-- 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:
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
⊢ I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f ≤ Hom.opensRange (I.glueDataObjMap ⋯)

Tactic:
rw [opensRange_glueDataObjMap]

Result:
no goals

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))
⊢ ∃ 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

Tactic:
obtain ⟨f, g, hfg, hf⟩ := exists_basicOpen_le_affine_inter U.2 V.2 ((I.glueDataObjι U).base p).1
    ⟨((I.glueDataObjι U).base p).2, hp⟩

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
⊢ ∃ 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
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
⊢ ∃ 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

Tactic:
refine ⟨(I.glueDataObjι U ⁻¹ᵁ U.1.ι ⁻¹ᵁ X.basicOpen f),
  fun x hx ↦ X.basicOpen_le g (hfg ▸ hx), hf, ?_⟩

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
⊢ (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

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
        (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

Tactic:
simp only [CommRingCat.hom_comp, RingHom.comp_apply]

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 ((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

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ x ∈ RingHom.ker (CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V)))

Tactic:
apply (I.glueDataObj U).IsSheaf.section_ext

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

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
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

Tactic:
apply ((ConcreteCategory.isIso_iff_bijective _).mp this).1

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))
⊢ (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)