-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : LocallyOfFiniteType f
inst_3 : IsCofiltered I
inst_4 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
this_1 : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun (i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀) ↦
      ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover,
    h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)) → I
hki' : (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)) → k j ⟶ A.i'
heq :
  ∀ (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := OpenCover.finiteSubcover A.𝒰D
h : Nonempty.{u + 1} ↥(D.obj A.i')
O : Finset I := {A.i'} ∪ Finset.image (fun (i : 𝒰Df.I₀) ↦ k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i')))) Finset.univ
o : 𝒰Df.I₀ := Nonempty.some ⋯
ho : k (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))) ∈ O
l : I
hl1 : {X : I} → X ∈ O → (l ⟶ X)
hl2 :
  ∀ {X_1 Y : I} (mX : X_1 ∈ O) (mY : Y ∈ O) {f_1 : X_1 ⟶ Y},
    Membership.mem (γ := Finset ((X : I) ×' (Y : I) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)))
        (Finset.image
          (fun (i : 𝒰Df.I₀) ↦
            PSigma.mk (β := fun (X : I) ↦ (Y : I) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
              (k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))))
              (PSigma.mk (β := fun (Y : I) ↦
                (_ : k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))) ∈ O) ×'
                  (_ : Y ∈ O) ×' (k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))) ⟶ Y))
                A.i'
                (PSigma.mk (β := fun (x : k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))) ∈ O) ↦
                  (_ : A.i' ∈ O) ×' (k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))) ⟶ A.i')) ⋯
                  (PSigma.mk (β := fun (x : A.i' ∈ O) ↦ k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))) ⟶ A.i') ⋯
                    (hki' (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))))))))
          Finset.univ)
        (PSigma.mk (β := fun (X : I) ↦ (Y : I) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X_1
          (PSigma.mk (β := fun (Y : I) ↦ (_ : X_1 ∈ O) ×' (_ : Y ∈ O) ×' (X_1 ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X_1 ∈ O) ↦ (_ : Y ∈ O) ×' (X_1 ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X_1 ⟶ Y) mY f_1)))) →
      hl1 mX ≫ f_1 = hl1 mY
this :
  ∀ (w v : 𝒰Df.I₀),
    hl1 ⋯ ≫ hki' (Cover.idx A.𝒰D (↑w : ↥(D.obj A.i'))) = hl1 ⋯ ≫ hki' (Cover.idx A.𝒰D (↑v : ↥(D.obj A.i')))
u : (Precoverage.ZeroHypercover.pullback₁ (D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))))) 𝒰Df).I₀
F : pullback (D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))))) (𝒰Df.f u) ⟶
  pullback (X := D.obj (k (Cover.idx A.𝒰D (↑u : ↥(D.obj A.i'))))) (Y :=
    PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D) (Cover.idx A.𝒰D (↑u : ↥(D.obj A.i'))))
    (D.map (hki' (Cover.idx A.𝒰D (↑u : ↥(D.obj A.i')))))
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D) (Cover.idx A.𝒰D (↑u : ↥(D.obj A.i')))) :=
  pullback.map (D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))))) (𝒰Df.f u)
    (D.map (hki' (Cover.idx A.𝒰D (↑u : ↥(D.obj A.i')))))
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D) (Cover.idx A.𝒰D (↑u : ↥(D.obj A.i'))))
    (D.map (hl1 ⋯)) (𝟙 (𝒰Df.X u)) (𝟙 (D.obj A.i')) ⋯ ⋯
hF :
  F ≫
      pullback.fst (D.map (hki' (Cover.idx A.𝒰D (↑u : ↥(D.obj A.i')))))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)
          (Cover.idx A.𝒰D (↑u : ↥(D.obj A.i')))) =
    pullback.fst (D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))))) (𝒰Df.f u) ≫ D.map (hl1 ⋯)
inr :
  ∀
    (heq :
      ∀ (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)),
        Eq (α :=
          pullback (D.map (hki' j)) (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D) j) ⟶ X)
          (pullback.fst (D.map (hki' j)) (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D) j) ≫
            D.map (hki' j) ≫ D.map A.hii' ≫ A.a)
          (pullback.fst (D.map (hki' j)) (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D) j) ≫
            D.map (hki' j) ≫ D.map A.hii' ≫ A.b)),
    Eq (α := pullback (D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))))) (𝒰Df.f u) ⟶ X)
      (pullback.fst (D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))))) (𝒰Df.f u) ≫
        D.map (hl1 ho) ≫ D.map (hki' (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i')))) ≫ D.map A.hii' ≫ a)
      (pullback.fst (D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))))) (𝒰Df.f u) ≫
        D.map (hl1 ho) ≫ D.map (hki' (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i')))) ≫ D.map A.hii' ≫ b)
⊢ (Precoverage.ZeroHypercover.pullback₁ (D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))))) 𝒰Df).f u ≫
      D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))) ≫ A.hii') ≫ a =
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))))) 𝒰Df).f u ≫
      D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))) ≫ A.hii') ≫ b

Tactic:
simp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
    PreZeroHypercover.pullback₁_X, PreZeroHypercover.pullback₁_f, Functor.map_comp, Category.assoc]
    at heq ⊢

Premises used: CategoryTheory.Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover, CategoryTheory.PreZeroHypercover.pullback₁_X, CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.PreZeroHypercover.pullback₁_f