-- 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))
H : (X.homOfLE ⋯ ≫ (↑U).ι) ⁻¹ᵁ ↑V = ⊤
⊢ (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

Tactic:
simp only [Scheme.comp_app, Scheme.Opens.ι_app, Scheme.homOfLE_app, ← Functor.map_comp,
  Scheme.app_eq _ H, Scheme.Opens.toScheme_presheaf_map, ← Functor.map_comp_assoc, 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))
H : (X.homOfLE ⋯ ≫ (↑U).ι) ⁻¹ᵁ ↑V = ⊤
⊢ (CommRingCat.Hom.hom
        (X.presheaf.map
            ((homOfLE ⋯).op ≫ (homOfLE ⋯).op ≫ ((Hom.opensFunctor (X.basicOpen f).ι).map (eqToHom ⋯).op.unop).op) ≫
          Hom.app (I.glueDataObjι (X.affineBasicOpen f)) ⊤ ≫
            (I.glueDataObj (X.affineBasicOpen f)).presheaf.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op)))
      x =
    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))
H : (X.homOfLE ⋯ ≫ (↑U).ι) ⁻¹ᵁ ↑V = ⊤
⊢ (CommRingCat.Hom.hom ((I.glueDataObj (X.affineBasicOpen f)).presheaf.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op)))
      ((CommRingCat.Hom.hom (Hom.app (I.glueDataObjι (X.affineBasicOpen f)) ⊤))
        ((CommRingCat.Hom.hom
            (X.presheaf.map
              ((homOfLE ⋯).op ≫ (homOfLE ⋯).op ≫ ((Hom.opensFunctor (X.basicOpen f).ι).map (eqToHom ⋯).op.unop).op)))
          x)) =
    0

Tactic:
convert RingHom.map_zero _ using 2

Result:
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 = ⊤
⊢ (CommRingCat.Hom.hom (Hom.app (I.glueDataObjι (X.affineBasicOpen f)) ⊤))
      ((CommRingCat.Hom.hom
          (X.presheaf.map
            ((homOfLE ⋯).op ≫ (homOfLE ⋯).op ≫ ((Hom.opensFunctor (X.basicOpen f).ι).map (eqToHom ⋯).op.unop).op)))
        x) =
    0

Proof state:
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))
⊢ ⊤ ≤ (X.basicOpen f).ι ⁻¹ᵁ ↑V

Tactic:
exact fun x _ ↦ (hfg.trans_le (X.basicOpen_le g)) x.2

Result:
no goals

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.app (I.glueDataObjι (X.affineBasicOpen f) ≫ X.homOfLE ⋯ ≫ (↑U).ι) ↑V ≫
          (I.glueDataObj (X.affineBasicOpen f)).presheaf.map (homOfLE ⋯).op))
      x =
    0

Tactic:
have H : (X.homOfLE (X.basicOpen_le f) ≫ U.1.ι) ⁻¹ᵁ V.1 = ⊤ := by
  simp only [Scheme.homOfLE_ι, ← top_le_iff]
  exact fun x _ ↦ (hfg.trans_le (X.basicOpen_le g)) x.2

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))
H : (X.homOfLE ⋯ ≫ (↑U).ι) ⁻¹ᵁ ↑V = ⊤
⊢ (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.unop).op) ≫
          (↑(X.affineBasicOpen f)).topIso.hom))
      (I.ideal (X.affineBasicOpen f))

Tactic:
simp only [Scheme.affineBasicOpen_coe, homOfLE_leOfHom, Scheme.comp_coeBase,
  TopologicalSpace.Opens.map_comp_obj, eqToHom_op, eqToHom_unop, ← Functor.map_comp,
  Scheme.Opens.topIso_hom, Category.assoc, ← CommRingCat.hom_comp]

Result:
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))