-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma ideal_le_ker_glueDataObjι (U V : X.affineOpens) :
    I.ideal V ≤ RingHom.ker (U.1.ι.app V.1 ≫ (I.glueDataObjι U).app _).hom

Proof state:
case intro.intro.intro.a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↑↑(I.glueDataObj U).toPresheafedSpace
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((ConcreteCategory.hom (I.glueDataObjι U).base) p) ∈ X.basicOpen f
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
⊢ (ConcreteCategory.hom (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f)))
      ((ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE ⋯).op))
        ((CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V))) x)) =
    (ConcreteCategory.hom (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f)))
      ((ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE ⋯).op)) 0)

Tactic:
simp only [CommRingCat.forget_map, map_zero, ← RingHom.comp_apply,
  ← CommRingCat.hom_comp, Category.assoc]

Result:
case intro.intro.intro.a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↑↑(I.glueDataObj U).toPresheafedSpace
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((ConcreteCategory.hom (I.glueDataObjι U).base) p) ∈ X.basicOpen f
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
⊢ (CommRingCat.Hom.hom
        (Hom.app (↑U).ι ↑V ≫
          Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V) ≫
            (I.glueDataObj U).presheaf.map (homOfLE ⋯).op ≫
              Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f)))
      x =
    0

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ ∀ x_1 ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V)),
    ∃ V_1,
      ∃ (hV : V_1 ≤ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))),
        x_1 ∈ V_1 ∧
          (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE hV).op))
              ((CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V))) x) =
            (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE hV).op)) 0

Tactic:
intro p hp

Result:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↑↑(I.glueDataObj U).toPresheafedSpace
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
⊢ ∃ V_1,
    ∃ (hV : V_1 ≤ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))),
      p ∈ V_1 ∧
        (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE hV).op))
            ((CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V))) x) =
          (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE hV).op)) 0

Proof state:
case intro.intro.intro.a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↑↑(I.glueDataObj U).toPresheafedSpace
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((ConcreteCategory.hom (I.glueDataObjι U).base) p) ∈ X.basicOpen f
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
⊢ (CommRingCat.Hom.hom
        (Hom.appLE (I.glueDataObjι (X.affineBasicOpen f) ≫ X.homOfLE ⋯ ≫ (↑U).ι) (↑V)
          (I.glueDataObjMap ⋯ ⁻¹ᵁ I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f) ⋯))
      x =
    0

Tactic:
rw [Scheme.Hom.appLE]

Result:
case intro.intro.intro.a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↑↑(I.glueDataObj U).toPresheafedSpace
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((ConcreteCategory.hom (I.glueDataObjι U).base) p) ∈ X.basicOpen f
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
⊢ (CommRingCat.Hom.hom
        (Hom.app (I.glueDataObjι (X.affineBasicOpen f) ≫ X.homOfLE ⋯ ≫ (↑U).ι) ↑V ≫
          (I.glueDataObj (X.affineBasicOpen f)).presheaf.map (homOfLE ⋯).op))
      x =
    0

Proof state:
case h.e'_2.h.e'_6
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↑↑(I.glueDataObj U).toPresheafedSpace
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((ConcreteCategory.hom (I.glueDataObjι U).base) p) ∈ X.basicOpen f
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
H : (X.homOfLE ⋯ ≫ (↑U).ι) ⁻¹ᵁ ↑V = ⊤
⊢ x ∈
    Ideal.comap
      (CommRingCat.Hom.hom
        (X.presheaf.map
          ((homOfLE ⋯).op ≫ (homOfLE ⋯).op ≫ ((Hom.opensFunctor (X.basicOpen f).ι).map (eqToHom ⋯)).op ≫ eqToHom ⋯)))
      (I.ideal (X.affineBasicOpen f))

Tactic:
exact I.ideal_le_comap_ideal (U := X.affineBasicOpen f) (V := V)
  (hfg.trans_le (X.basicOpen_le g)) hx

Result:
no goals

Proof state:
case intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↑↑(I.glueDataObj U).toPresheafedSpace
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((ConcreteCategory.hom (I.glueDataObjι U).base) p) ∈ X.basicOpen f
⊢ (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE ⋯).op))
      ((CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V))) x) =
    (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE ⋯).op)) 0

Tactic:
have := Hom.isIso_app (I.glueDataObjMap (X.affineBasicOpen_le f))
  (I.glueDataObjι U ⁻¹ᵁ U.1.ι ⁻¹ᵁ X.basicOpen f) (by rw [opensRange_glueDataObjMap])

Result:
case intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↑↑(I.glueDataObj U).toPresheafedSpace
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((ConcreteCategory.hom (I.glueDataObjι U).base) p) ∈ X.basicOpen f
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
⊢ (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE ⋯).op))
      ((CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V))) x) =
    (ConcreteCategory.hom ((I.glueDataObj U).presheaf.map (homOfLE ⋯).op)) 0