<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : Z.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>x : (i : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft (𝒰.pullbackCover f) f g).J) × ((fun i => let Xᵢ := CategoryTheory.Limits.pullback f (𝒰.map i); let Yᵢ := CategoryTheory.Limits.pullback g (𝒰.map i); let W := CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) (CategoryTheory.Limits.pullback.snd f (𝒰.map i)); let_fun this := CategoryTheory.Limits.bigSquareIsPullback (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) (CategoryTheory.Limits.pullback.snd f (𝒰.map i))) (CategoryTheory.Limits.pullback.fst g (𝒰.map i)) (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) (𝒰.map i) (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) (CategoryTheory.Limits.pullback.snd f (𝒰.map i))) (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) g ⋯ ⋯ (CategoryTheory.Limits.PullbackCone.isLimitOfFlip (CategoryTheory.Limits.pullbackIsPullback g (𝒰.map i))) (CategoryTheory.Limits.PullbackCone.isLimitOfFlip (CategoryTheory.Limits.pullbackIsPullback (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) (CategoryTheory.Limits.pullback.snd f (𝒰.map i)))); AlgebraicGeometry.Scheme.openCoverOfIsIso ((CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) (CategoryTheory.Limits.pullback.snd g (𝒰.map i))).hom ≫ (CategoryTheory.Limits.limit.isoLimitCone { cone := CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) (CategoryTheory.Limits.pullback.snd f (𝒰.map i))) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) ≫ CategoryTheory.Limits.pullback.fst g (𝒰.map i)) ⋯, isLimit := this }).inv ≫ CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.snd f (𝒰.map i) ≫ 𝒰.map i) g ((𝒰.pullbackCover f).map i ≫ f) g (𝟙 (CategoryTheory.Limits.pullback f (𝒰.map i))) (𝟙 Y) (𝟙 Z) ⋯ ⋯)) i).J<GOAL>(AlgebraicGeometry.Scheme.Pullback.openCoverOfBase' 𝒰 f g).map x = (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst))).hom ≫ (CategoryTheory.Limits.limit.isoLimitCone { cone := CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst))) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst)) ≫ CategoryTheory.Limits.pullback.fst g (𝒰.map x.fst)) ⋯, isLimit := CategoryTheory.Limits.bigSquareIsPullback (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst))) (CategoryTheory.Limits.pullback.fst g (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst)) (𝒰.map x.fst) (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst))) (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst)) g ⋯ ⋯ (CategoryTheory.Limits.PullbackCone.isLimitOfFlip (CategoryTheory.Limits.pullbackIsPullback g (𝒰.map x.fst))) (CategoryTheory.Limits.PullbackCone.isLimitOfFlip (CategoryTheory.Limits.pullbackIsPullback (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst)))) }).inv ≫ CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst) ≫ 𝒰.map x.fst) g (CategoryTheory.Limits.pullback.fst f (𝒰.map x.fst) ≫ f) g (𝟙 (CategoryTheory.Limits.pullback f (𝒰.map x.fst))) (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫ CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.fst f (𝒰.map x.fst) ≫ f) g f g (CategoryTheory.Limits.pullback.fst f (𝒰.map x.fst)) (𝟙 Y) (𝟙 Z) ⋯ ⋯