-- 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 : ∀ (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
⊢ ∀ (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')))

Tactic:
have (w v : 𝒰Df.I₀) :
      hl1 (by simp [O]) ≫ hki' (A.𝒰D.idx w.1) = hl1 (by simp [O]) ≫ hki' (A.𝒰D.idx v.1) := by
    trans hl1 (show A.i' ∈ O by simp [O])
    · exact hl2 _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))
    · exact .symm <| hl2 _ _ (Finset.mem_image_of_mem _ (by simp))