Re: Formalizing topos-theoretic arguments in Lean