-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst_3 : CompactSpace.{u} ↥(D.obj i)
s : (↑Γ(D.obj i, ⊤) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (c.π.app i)) :
          (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
U : (x : ↥(D.obj i)) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : (x : ↥(D.obj i)) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H :
  ∀ (x : ↥(D.obj i)),
    Eq (α := (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(D.obj i, U x)) (Scheme.Hom.app (D.map (f x)) (U x)) :
            (a : (↑Γ(D.obj i, U x) : Type u)) → (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
          (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) s (U x) ⋯ :
            ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
              ((D.obj i).presheaf.obj (Opposite.op (U x)))) :
        (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
      (0 : (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
t : Finset ↥(D.obj i)
ht : Eq.{u + 1} (α := Set ↥(D.obj i)) (⋃ x ∈ t, (↑(U x) : Set ↥(D.obj i))) ⊤
k : I
fk : {X : I} → X ∈ insert i (Finset.image j t) → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ insert i (Finset.image j t)) (mY : Y ∈ insert i (Finset.image j t)) {f_1 : X ⟶ Y},
    Membership.mem (γ :=
        Finset
          ((X : I) ×'
            (Y : I) ×' (_ : X ∈ insert i (Finset.image j t)) ×' (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y)))
        (Finset.image
          (fun (x : ↥t) ↦
            PSigma.mk (β := fun (X : I) ↦
              (Y : I) ×' (_ : X ∈ insert i (Finset.image j t)) ×' (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y))
              (j (↑x : ↥(D.obj i)))
              (PSigma.mk (β := fun (Y : I) ↦
                (_ : j (↑x : ↥(D.obj i)) ∈ insert i (Finset.image j t)) ×'
                  (_ : Y ∈ insert i (Finset.image j t)) ×' (j (↑x : ↥(D.obj i)) ⟶ Y))
                i
                (PSigma.mk (β := fun (x_1 : j (↑x : ↥(D.obj i)) ∈ insert i (Finset.image j t)) ↦
                  (_ : i ∈ insert i (Finset.image j t)) ×' (j (↑x : ↥(D.obj i)) ⟶ i)) ⋯
                  (PSigma.mk (β := fun (x_1 : i ∈ insert i (Finset.image j t)) ↦ j (↑x : ↥(D.obj i)) ⟶ i) ⋯
                    (f (↑x : ↥(D.obj i)))))))
          t.attach)
        (PSigma.mk (β := fun (X : I) ↦
          (Y : I) ×' (_ : X ∈ insert i (Finset.image j t)) ×' (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : I) ↦
            (_ : X ∈ insert i (Finset.image j t)) ×' (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ insert i (Finset.image j t)) ↦
              (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ insert i (Finset.image j t)) ↦ X ⟶ Y) mY f_1)))) →
      fk mX ≫ f_1 = fk mY
x : ↥(D.obj k)
l : ↥(D.obj i)
hl : l ∈ t
hlU : Membership.mem (α := ↥(D.obj i)) (↑(U l) : Set ↥(D.obj i)) ((D.map (fk ⋯)) x : ↥(D.obj i))
h₁ : fk ⋯ = fk ⋯ ≫ f l
h₂ : D.map (fk ⋯) ⁻¹ᵁ U l ≤ D.map (fk ⋯) ⁻¹ᵁ D.map (f l) ⁻¹ᵁ U l
⊢ Eq (α := (↑Γ(D.obj k, D.map (fk ⋯) ⁻¹ᵁ U l) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE (D.map (fk ⋯)) (D.map (f l) ⁻¹ᵁ U l) (D.map (fk ⋯) ⁻¹ᵁ U l) h₂) :
          (a : (↑Γ(D.obj (j l), D.map (f l) ⁻¹ᵁ U l) : Type u)) → (↑Γ(D.obj k, D.map (fk ⋯) ⁻¹ᵁ U l) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(D.obj i, U l)) (Scheme.Hom.app (D.map (f l)) (U l)) :
              (a : (↑Γ(D.obj i, U l) : Type u)) → (↑Γ(D.obj (j l), D.map (f l) ⁻¹ᵁ U l) : Type u))
            (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) s (U l) ⋯ :
              ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
                ((D.obj i).presheaf.obj (Opposite.op (U l)))) :
          (↑Γ(D.obj (j l), D.map (f l) ⁻¹ᵁ U l) : Type u)) :
      (↑Γ(D.obj k, D.map (fk ⋯) ⁻¹ᵁ U l) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE (D.map (fk ⋯)) (D.map (f l) ⁻¹ᵁ U l) (D.map (fk ⋯) ⁻¹ᵁ U l) h₂) :
          (a : (↑Γ(D.obj (j l), D.map (f l) ⁻¹ᵁ U l) : Type u)) → (↑Γ(D.obj k, D.map (fk ⋯) ⁻¹ᵁ U l) : Type u))
        0 :
      (↑Γ(D.obj k, D.map (fk ⋯) ⁻¹ᵁ U l) : Type u))

Tactic:
congr((D.map (fk _)).appLE _ _ h₂ $(H l))

Premises used: Finset.mem_insert_self, congrArg, CategoryTheory.ConcreteCategory.hom, id, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.appLE, CategoryTheory.Functor.map, Finset.mem_insert_of_mem, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, Finset.mem_image_of_mem, DFunLike.coe, Finset.image, CategoryTheory.Functor.obj