-- 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)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this : CompactSpace.{u} ↥c.pt
i : (x : ↥c.pt) → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), Membership.mem (α := ↥(D.obj (i x))) (U x) ((c.π.app (i x)) x : ↥(D.obj (i x)))
t : (x : ↥c.pt) → (↑Γ(D.obj (i x), U x) : Type u)
ht :
  ∀ (x : ↥c.pt),
    Eq (α := (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x)) (Scheme.Hom.app (c.π.app (i x)) (U x)) :
            (a : (↑Γ(D.obj (i x), U x) : Type u)) → (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
          (t x) :
        (↑Γ(c.pt, c.π.app (i x) ⁻¹ᵁ U x) : Type u))
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) s (c.π.app (i x) ⁻¹ᵁ U x) ⋯ :
        ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
          (c.pt.presheaf.obj (Opposite.op (c.π.app (i x) ⁻¹ᵁ U x))))
x y : ↥c.pt
j : I
fjx : j ⟶ i x
fjy : j ⟶ i y
k : I
fkj : k ⟶ j
H : D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y ≤ D.map fkj ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)
hk :
  Eq (α := (↑Γ(D.obj k, D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) ((D.obj k).presheaf.map (homOfLE H).op) :
          (a : (↑Γ(D.obj k, D.map fkj ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) : Type u)) →
            (↑Γ(D.obj k, D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(D.obj j, D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y))
                (Scheme.Hom.app (D.map fkj) (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) :
              (a : (↑Γ(D.obj j, D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y) : Type u)) →
                (↑Γ(D.obj k, D.map fkj ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) : Type u))
            (HSub.hSub (α :=
              ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
                ((D.obj j).presheaf.obj (Opposite.op (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y))))
              (β :=
              ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
                ((D.obj j).presheaf.obj (Opposite.op (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y))))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (X := (D.obj j).presheaf.obj (Opposite.op (D.map fjx ⁻¹ᵁ U x))) (Y :=
                      (D.obj j).presheaf.obj (Opposite.op (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)))
                      ((D.obj j).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
                    (a : (↑((D.obj j).presheaf.obj (Opposite.op (D.map fjx ⁻¹ᵁ U x))) : Type u)) →
                      (↑((D.obj j).presheaf.obj (Opposite.op (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y))) : Type u))
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (X := Γ(D.obj (i x), U x)) (Scheme.Hom.app (D.map fjx) (U x)) :
                        (a : (↑Γ(D.obj (i x), U x) : Type u)) → (↑Γ(D.obj j, D.map fjx ⁻¹ᵁ U x) : Type u))
                      (t x) :
                    (↑Γ(D.obj j, D.map fjx ⁻¹ᵁ U x) : Type u)) :
                (↑((D.obj j).presheaf.obj (Opposite.op (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y))) : Type u))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (X := (D.obj j).presheaf.obj (Opposite.op (D.map fjy ⁻¹ᵁ U y))) (Y :=
                      (D.obj j).presheaf.obj (Opposite.op (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)))
                      ((D.obj j).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
                    (a : (↑((D.obj j).presheaf.obj (Opposite.op (D.map fjy ⁻¹ᵁ U y))) : Type u)) →
                      (↑((D.obj j).presheaf.obj (Opposite.op (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y))) : Type u))
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (X := Γ(D.obj (i y), U y)) (Scheme.Hom.app (D.map fjy) (U y)) :
                        (a : (↑Γ(D.obj (i y), U y) : Type u)) → (↑Γ(D.obj j, D.map fjy ⁻¹ᵁ U y) : Type u))
                      (t y) :
                    (↑Γ(D.obj j, D.map fjy ⁻¹ᵁ U y) : Type u)) :
                (↑((D.obj j).presheaf.obj (Opposite.op (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y))) : Type u))) :
          (↑Γ(D.obj k, D.map fkj ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) : Type u)) :
      (↑Γ(D.obj k, D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) ((D.obj k).presheaf.map (homOfLE H).op) :
          (a : (↑Γ(D.obj k, D.map fkj ⁻¹ᵁ (D.map fjx ⁻¹ᵁ U x ⊓ D.map fjy ⁻¹ᵁ U y)) : Type u)) →
            (↑Γ(D.obj k, D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y) : Type u))
        0 :
      (↑Γ(D.obj k, D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y) : Type u))
⊢ Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      ((D.obj k).presheaf.obj (Opposite.op (D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y))))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := (D.obj k).presheaf.obj (Opposite.op (D.map (fkj ≫ fjx) ⁻¹ᵁ U x))) (Y :=
            (D.obj k).presheaf.obj (Opposite.op (D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y)))
            ((D.obj k).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑((D.obj k).presheaf.obj (Opposite.op (D.map (fkj ≫ fjx) ⁻¹ᵁ U x))) : Type u)) →
            (↑((D.obj k).presheaf.obj (Opposite.op (D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(D.obj (i x), U x)) (Scheme.Hom.app (D.map (fkj ≫ fjx)) (U x)) :
              (a : (↑Γ(D.obj (i x), U x) : Type u)) → (↑Γ(D.obj k, D.map (fkj ≫ fjx) ⁻¹ᵁ U x) : Type u))
            (t x) :
          (↑Γ(D.obj k, D.map (fkj ≫ fjx) ⁻¹ᵁ U x) : Type u)) :
      (↑((D.obj k).presheaf.obj (Opposite.op (D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := (D.obj k).presheaf.obj (Opposite.op (D.map (fkj ≫ fjy) ⁻¹ᵁ U y))) (Y :=
            (D.obj k).presheaf.obj (Opposite.op (D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y)))
            ((D.obj k).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑((D.obj k).presheaf.obj (Opposite.op (D.map (fkj ≫ fjy) ⁻¹ᵁ U y))) : Type u)) →
            (↑((D.obj k).presheaf.obj (Opposite.op (D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(D.obj (i y), U y)) (Scheme.Hom.app (D.map (fkj ≫ fjy)) (U y)) :
              (a : (↑Γ(D.obj (i y), U y) : Type u)) → (↑Γ(D.obj k, D.map (fkj ≫ fjy) ⁻¹ᵁ U y) : Type u))
            (t y) :
          (↑Γ(D.obj k, D.map (fkj ≫ fjy) ⁻¹ᵁ U y) : Type u)) :
      (↑((D.obj k).presheaf.obj (Opposite.op (D.map (fkj ≫ fjx) ⁻¹ᵁ U x ⊓ D.map (fkj ≫ fjy) ⁻¹ᵁ U y))) : Type u))

Tactic:
simpa [sub_eq_zero, ← ConcreteCategory.comp_apply, -Scheme.Hom.comp_appLE,
      Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_comp_appLE] using hk

Premises used: CategoryTheory.ConcreteCategory.comp_apply, sub_eq_zero, AlgebraicGeometry.Scheme.Hom.comp_appLE, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE