Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝⁴ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝³ : LocallyOfFiniteType f
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
inst✝ : ∀ (i : I), IsAffineHom (A.c.π.app i)
j : A.𝒰D.I₀
this✝² : IsAffine (A.𝒰D.X j)
this✝¹ : ∀ (i : Over A.i'), IsAffine ((Over.post D ⋙ Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).obj i)
this✝ : IsAffine ((Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).mapCone ((Over.conePost D A.i').obj A.c)).pt
this : LocallyOfFiniteType ((A.𝒰X j.fst.fst).f j.fst.snd ≫ Scheme.Cover.pullbackHom A.𝒰S f j.fst.fst)
H₁ :
  pullback.fst (D.map A.hii' ≫ pullback.lift A.a A.b ⋯)
        ((Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩) ≫
      D.map A.hii' ≫ A.a =
    pullback.snd (D.map A.hii' ≫ pullback.lift A.a A.b ⋯)
        ((Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩) ≫
      pullback.fst ((A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.snd f (A.𝒰S.f j.fst.fst))
          ((A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.snd f (A.𝒰S.f j.fst.fst)) ≫
        (A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.fst f (A.𝒰S.f j.fst.fst)
H₂ :
  pullback.fst (D.map A.hii' ≫ pullback.lift A.a A.b ⋯)
        ((Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩) ≫
      D.map A.hii' ≫ A.b =
    pullback.snd (D.map A.hii' ≫ pullback.lift A.a A.b ⋯)
        ((Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩) ≫
      pullback.snd ((A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.snd f (A.𝒰S.f j.fst.fst))
          ((A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.snd f (A.𝒰S.f j.fst.fst)) ≫
        (A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.fst f (A.𝒰S.f j.fst.fst)
H₃ :
  pullback.fst (A.c.π.app A.i') (A.𝒰D.f j) ≫ A.c.π.app A.i ≫ A.a =
    pullback.fst (A.c.π.app A.i') (A.𝒰D.f j) ≫ A.c.π.app A.i ≫ A.b
⊢ ((((Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).mapCone ((Over.conePost D A.i').obj A.c)).π.app
            (Over.mk (𝟙 A.i')) ≫
          pullback.snd ((Over.post D).obj (Over.mk (𝟙 A.i'))).hom (A.𝒰D.f j) ≫
            (A.𝒰D₀.X j.fst).affineCover.f j.snd ≫
              Scheme.Cover.pullbackHom (Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X) A.g
                  ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩ ≫
                pullback.fst
                  ((A.𝒰X ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.snd.1 ≫
                    Scheme.Cover.pullbackHom A.𝒰S f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst)
                  ((A.𝒰X ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.snd.2 ≫
                    Scheme.Cover.pullbackHom A.𝒰S f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst)) ≫
        (A.𝒰X j.fst.fst).f j.fst.snd) ≫
      pullback.fst f (A.𝒰S.f j.fst.fst) =
    ((((Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).mapCone ((Over.conePost D A.i').obj A.c)).π.app
            (Over.mk (𝟙 A.i')) ≫
          pullback.snd ((Over.post D).obj (Over.mk (𝟙 A.i'))).hom (A.𝒰D.f j) ≫
            (A.𝒰D₀.X j.fst).affineCover.f j.snd ≫
              Scheme.Cover.pullbackHom (Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X) A.g
                  ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩ ≫
                pullback.snd
                  ((A.𝒰X ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.snd.1 ≫
                    Scheme.Cover.pullbackHom A.𝒰S f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst)
                  ((A.𝒰X ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.snd.2 ≫
                    Scheme.Cover.pullbackHom A.𝒰S f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst)) ≫
        (A.𝒰X j.fst.fst).f j.fst.snd) ≫
      pullback.fst f (A.𝒰S.f j.fst.fst)

Tactic:
simp only [pullback.condition_assoc, 𝒰D, ← A.c.w A.hii', Category.assoc] at H₃

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝⁴ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝³ : LocallyOfFiniteType f
inst✝² : IsCofiltered I
inst✝¹ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
inst✝ : ∀ (i : I), IsAffineHom (A.c.π.app i)
j : A.𝒰D.I₀
this✝² : IsAffine (A.𝒰D.X j)
this✝¹ : ∀ (i : Over A.i'), IsAffine ((Over.post D ⋙ Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).obj i)
this✝ : IsAffine ((Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).mapCone ((Over.conePost D A.i').obj A.c)).pt
this : LocallyOfFiniteType ((A.𝒰X j.fst.fst).f j.fst.snd ≫ Scheme.Cover.pullbackHom A.𝒰S f j.fst.fst)
H₁ :
  pullback.fst (D.map A.hii' ≫ pullback.lift A.a A.b ⋯)
        ((Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩) ≫
      D.map A.hii' ≫ A.a =
    pullback.snd (D.map A.hii' ≫ pullback.lift A.a A.b ⋯)
        ((Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩) ≫
      pullback.fst ((A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.snd f (A.𝒰S.f j.fst.fst))
          ((A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.snd f (A.𝒰S.f j.fst.fst)) ≫
        (A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.fst f (A.𝒰S.f j.fst.fst)
H₂ :
  pullback.fst (D.map A.hii' ≫ pullback.lift A.a A.b ⋯)
        ((Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩) ≫
      D.map A.hii' ≫ A.b =
    pullback.snd (D.map A.hii' ≫ pullback.lift A.a A.b ⋯)
        ((Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩) ≫
      pullback.snd ((A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.snd f (A.𝒰S.f j.fst.fst))
          ((A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.snd f (A.𝒰S.f j.fst.fst)) ≫
        (A.𝒰X j.fst.fst).f j.fst.snd ≫ pullback.fst f (A.𝒰S.f j.fst.fst)
H₃ :
  pullback.snd (A.c.π.app A.i') ((Precoverage.ZeroHypercover.bind A.𝒰D₀ fun x ↦ (A.𝒰D₀.X x).affineCover).f j) ≫
      (Precoverage.ZeroHypercover.bind A.𝒰D₀ fun x ↦ (A.𝒰D₀.X x).affineCover).f j ≫ D.map A.hii' ≫ A.a =
    pullback.snd (A.c.π.app A.i') ((Precoverage.ZeroHypercover.bind A.𝒰D₀ fun x ↦ (A.𝒰D₀.X x).affineCover).f j) ≫
      (Precoverage.ZeroHypercover.bind A.𝒰D₀ fun x ↦ (A.𝒰D₀.X x).affineCover).f j ≫ D.map A.hii' ≫ A.b
⊢ ((((Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).mapCone ((Over.conePost D A.i').obj A.c)).π.app
            (Over.mk (𝟙 A.i')) ≫
          pullback.snd ((Over.post D).obj (Over.mk (𝟙 A.i'))).hom (A.𝒰D.f j) ≫
            (A.𝒰D₀.X j.fst).affineCover.f j.snd ≫
              Scheme.Cover.pullbackHom (Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X) A.g
                  ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩ ≫
                pullback.fst
                  ((A.𝒰X ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.snd.1 ≫
                    Scheme.Cover.pullbackHom A.𝒰S f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst)
                  ((A.𝒰X ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.snd.2 ≫
                    Scheme.Cover.pullbackHom A.𝒰S f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst)) ≫
        (A.𝒰X j.fst.fst).f j.fst.snd) ≫
      pullback.fst f (A.𝒰S.f j.fst.fst) =
    ((((Over.pullback (A.𝒰D.f j) ⋙ Over.forget (A.𝒰D.X j)).mapCone ((Over.conePost D A.i').obj A.c)).π.app
            (Over.mk (𝟙 A.i')) ≫
          pullback.snd ((Over.post D).obj (Over.mk (𝟙 A.i'))).hom (A.𝒰D.f j) ≫
            (A.𝒰D₀.X j.fst).affineCover.f j.snd ≫
              Scheme.Cover.pullbackHom (Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X) A.g
                  ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩ ≫
                pullback.snd
                  ((A.𝒰X ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.snd.1 ≫
                    Scheme.Cover.pullbackHom A.𝒰S f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst)
                  ((A.𝒰X ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst).f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.snd.2 ≫
                    Scheme.Cover.pullbackHom A.𝒰S f ⟨j.fst.fst, (j.fst.snd, j.fst.snd)⟩.fst)) ≫
        (A.𝒰X j.fst.fst).f j.fst.snd) ≫
      pullback.fst f (A.𝒰S.f j.fst.fst)