<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰✝ : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰✝.J), HasPullback (𝒰✝.map i ≫ f✝) g✝<VAR>s : PullbackCone f✝ g✝<VAR>𝒰 : Z.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>i : 𝒰.J<GOAL>pullback.map (pullback.snd f (𝒰.map i)) (pullback.snd g (𝒰.map i)) f g (pullback.fst f (𝒰.map i)) (pullback.fst g (𝒰.map i)) (𝒰.map i) ⋯ ⋯ = (pullbackSymmetry (pullback.snd f (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst)) (pullback.snd g (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst))).hom ≫ (limit.isoLimitCone { cone := PullbackCone.mk (pullback.snd (pullback.snd g (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst)) (pullback.snd f (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst))) (pullback.fst (pullback.snd g (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst)) (pullback.snd f (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst)) ≫ pullback.fst g (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst)) ⋯, isLimit := bigSquareIsPullback (pullback.fst (pullback.snd g (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst)) (pullback.snd f (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst))) (pullback.fst g (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst)) (pullback.snd f (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst)) (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst) (pullback.snd (pullback.snd g (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst)) (pullback.snd f (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst))) (pullback.snd g (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst)) g ⋯ ⋯ (PullbackCone.isLimitOfFlip (pullbackIsPullback g (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst))) (PullbackCone.isLimitOfFlip (pullbackIsPullback (pullback.snd g (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst)) (pullback.snd f (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst)))) }).inv ≫ pullback.map (pullback.snd f (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst) ≫ 𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst) g (pullback.fst f (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst) ≫ f) g (𝟙 (pullback f (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst))) (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫ pullback.map (pullback.fst f (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst) ≫ f) g f g (pullback.fst f (𝒰.map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i).fst)) (𝟙 Y) (𝟙 Z) ⋯ ⋯