Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
        (𝒰.f i) ⋯ ⋯ ≫
      pullback.fst f g =
    ((pullbackSymmetry
            (pullback.snd f
              (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))
            (pullback.snd g
              (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))).hom ≫
        (limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv ≫
          pullback.map
              (pullback.snd f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
                𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst)
              g
              (pullback.fst f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
                f)
              g
              (𝟙
                (pullback f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst)))
              (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫
            pullback.map
              (pullback.fst f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
                f)
              g f g
              (pullback.fst f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))
              (𝟙 Y) (𝟙 Z) ⋯ ⋯) ≫
      pullback.fst f g

pp: case h₁
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
        (𝒰.f i) ⋯ ⋯ ≫
      pullback.snd f g =
    ((pullbackSymmetry
            (pullback.snd f
              (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))
            (pullback.snd g
              (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))).hom ≫
        (limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv ≫
          pullback.map
              (pullback.snd f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
                𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst)
              g
              (pullback.fst f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
                f)
              g
              (𝟙
                (pullback f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst)))
              (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫
            pullback.map
              (pullback.fst f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
                f)
              g f g
              (pullback.fst f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))
              (𝟙 Y) (𝟙 Z) ⋯ ⋯) ≫
      pullback.snd f g

Tactic:
<;>

Goal state after:
case h₀
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
        (𝒰.f i) ⋯ ⋯ ≫
      pullback.fst f g =
    ((pullbackSymmetry
            (pullback.snd f
              (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))
            (pullback.snd g
              (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))).hom ≫
        (limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv ≫
          pullback.map
              (pullback.snd f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
                𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst)
              g
              (pullback.fst f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
                f)
              g
              (𝟙
                (pullback f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst)))
              (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫
            pullback.map
              (pullback.fst f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
                f)
              g f g
              (pullback.fst f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))
              (𝟙 Y) (𝟙 Z) ⋯ ⋯) ≫
      pullback.fst f g

case h₁
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
        (𝒰.f i) ⋯ ⋯ ≫
      pullback.snd f g =
    ((pullbackSymmetry
            (pullback.snd f
              (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))
            (pullback.snd g
              (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))).hom ≫
        (limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv ≫
          pullback.map
              (pullback.snd f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
                𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst)
              g
              (pullback.fst f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
                f)
              g
              (𝟙
                (pullback f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst)))
              (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫
            pullback.map
              (pullback.fst f
                  (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
                f)
              g f g
              (pullback.fst f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))
              (𝟙 Y) (𝟙 Z) ⋯ ⋯) ≫
      pullback.snd f g