-- 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
U : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
s : (↑Γ(D.obj i, U) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
          (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
this : CompactSpace.{u} ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
obtain :
  ∀ (j : Over i) (f : j ⟶ Over.mk (𝟙 i))
    (hf :
      Eq (α := (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop ((opensDiagram D i U).map f)) :
              (a : (↑Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤) : Type u)) →
                (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X := Γ(D.obj i, U)) (Y := Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤))
                    ((D.obj i).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
                  (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u))
                s :
              (↑Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u)) :
          (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
        (0 : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))),
    ∃ (j : I) (f : j ⟶ i),
      Eq (α := (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.app (D.map f) U) :
              (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
            s :
          (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
        (0 : (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
⊢ ∃ (j : I) (f : j ⟶ i),
    Eq (α := (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.app (D.map f) U) :
            (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
          s :
        (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))
      (0 : (↑Γ(D.obj j, D.map f ⁻¹ᵁ U) : Type u))

Tactic:
obtain ⟨j, f, hf⟩ := exists_appTop_map_eq_zero_of_isLimit _ _
    (isLimitOpensCone D c hc i U) (i := .mk (𝟙 i))
    ((D.obj i).presheaf.map (homOfLE (show (D.map (𝟙 _) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U by simp)).op s) (by
      rw [← map_zero (c.pt.presheaf.map (homOfLE
        (show (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ c.π.app i ⁻¹ᵁ U by simp)).op).hom, ← hs]
      dsimp [Scheme.Opens.toScheme_presheaf_obj]
      rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply]
      congr! 2
      simp [Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE])

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, AlgebraicGeometry.isLimitOpensCone, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.exists_appTop_map_eq_zero_of_isLimit, DFunLike.coe, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace