-- 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))
x : ↥(D.obj i)
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : x ∈ (↑U : Set ↥(D.obj i))
this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i U).obj j)
h :
  Eq (α := (↑Γ((↑(c.π.app i ⁻¹ᵁ U) : Scheme), ⊤) : Type u))
    (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(D.obj i, ⊤)) (Y := Γ((↑(c.π.app i ⁻¹ᵁ U) : Scheme), ⊤))
              (Scheme.Hom.appLE (c.π.app i) ⊤ ((c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤) ⋯ :
                Γ(D.obj i, ⊤) ⟶ Γ(c.pt, (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤)) :
            (↑Γ(D.obj i, ⊤) : Type u) →+* (↑Γ((↑(c.π.app i ⁻¹ᵁ U) : Scheme), ⊤) : Type u)) :
          (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ((↑(c.π.app i ⁻¹ᵁ U) : Scheme), ⊤) : Type u))
        s :
      (↑Γ((↑(c.π.app i ⁻¹ᵁ U) : Scheme), ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(D.obj i, ⊤)) (Y := c.pt.presheaf.obj (Opposite.op (⋯.functor.obj ⊤)))
            (Scheme.Hom.appLE (c.π.app i) ⊤ (⋯.functor.obj ⊤) ⋯) :
          (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑(c.pt.presheaf.obj (Opposite.op (⋯.functor.obj ⊤))) : Type u))
        s :
      (↑(c.pt.presheaf.obj (Opposite.op (⋯.functor.obj ⊤))) : Type u))
⊢ Eq (α := (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj (Over.mk (𝟙 i)), ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤))
            (Scheme.Hom.appTop ((opensCone D c i U).π.app (Over.mk (𝟙 i)))) :
          (a : (↑Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤) : Type u)) →
            (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj (Over.mk (𝟙 i)), ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ((Over.forget i ⋙ D).obj (Over.mk (𝟙 i)), ⊤))
                (Scheme.Hom.appTop ((opensDiagramι D i U).app (Over.mk (𝟙 i)))) :
              (a : (↑Γ((Over.forget i ⋙ D).obj (Over.mk (𝟙 i)), ⊤) : Type u)) →
                (↑Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤) : Type u))
            s :
          (↑Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤) : Type u)) :
      (↑Γ(((Functor.const (Over i)).obj (opensCone D c i U).pt).obj (Over.mk (𝟙 i)), ⊤) : Type u))
    ((CommRingCat.Hom.hom (c.pt.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(c.pt.presheaf.obj (Opposite.op ⊤)) : Type u)) →
            (↑(c.pt.presheaf.obj (Opposite.op (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))))) : 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)) :
      (↑(c.pt.presheaf.obj (Opposite.op (⋯.functor.obj (Opposite.unop (Opposite.op ⊤))))) : Type u))

Tactic:
simp [Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE, ← ConcreteCategory.comp_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.Hom.resLE_appLE