-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma Hom.range_subset_ker_support (f : X.Hom Y) :
    Set.range f.base ⊆ f.ker.support

Proof state:
X Y : Scheme
f : X.Hom Y
⊢ Set.range ⇑(ConcreteCategory.hom f.base) ⊆ f.ker.support

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case intro
X Y : Scheme
f : X.Hom Y
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom f.base) x ∈ f.ker.support

Proof state:
case intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X.Hom Y
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
⊢ (ConcreteCategory.hom f.base) x ∈ Y.zeroLocus ↑(f.ker.ideal ⟨U, hU⟩)

Tactic:
simp only [Scheme.mem_zeroLocus_iff, SetLike.mem_coe]

Result:
case intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X.Hom Y
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
⊢ ∀ f_1 ∈ f.ker.ideal ⟨U, hU⟩, (ConcreteCategory.hom f.base) x ∉ Y.basicOpen f_1

Proof state:
case intro
X Y : Scheme
f : X.Hom Y
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom f.base) x ∈ f.ker.support

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
  (isBasis_affine_open Y).exists_subset_of_mem_open (Set.mem_univ (f.base x)) isOpen_univ

Result:
case intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X.Hom Y
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
⊢ (ConcreteCategory.hom f.base) x ∈ f.ker.support

Proof state:
case intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X.Hom Y
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
⊢ ∀ f_1 ∈ f.ker.ideal ⟨U, hU⟩, (ConcreteCategory.hom f.base) x ∉ Y.basicOpen f_1

Tactic:
intro s hs hxs

Result:
case intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X.Hom Y
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
s : ↑Γ(Y, U)
hs : s ∈ f.ker.ideal ⟨U, hU⟩
hxs : (ConcreteCategory.hom f.base) x ∈ Y.basicOpen s
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X.Hom Y
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
⊢ (ConcreteCategory.hom f.base) x ∈ f.ker.support

Tactic:
refine ((support_inter f.ker ⟨U, hU⟩).ge ⟨?_, hxU⟩).1

Result:
case intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X.Hom Y
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
⊢ (ConcreteCategory.hom f.base) x ∈ Y.zeroLocus ↑(f.ker.ideal ⟨U, hU⟩)

Proof state:
case intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X.Hom Y
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
s : ↑Γ(Y, U)
hs : s ∈ f.ker.ideal ⟨U, hU⟩
hxs : (ConcreteCategory.hom f.base) x ∈ Y.basicOpen s
this : x ∈ f ⁻¹ᵁ Y.basicOpen s
⊢ False

Tactic:
rwa [Scheme.preimage_basicOpen, RingHom.mem_ker.mp (ideal_ofIdeals_le _ _ hs),
  Scheme.basicOpen_zero] at this

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X.Hom Y
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
s : ↑Γ(Y, U)
hs : s ∈ f.ker.ideal ⟨U, hU⟩
hxs : (ConcreteCategory.hom f.base) x ∈ Y.basicOpen s
⊢ False

Tactic:
have : x ∈ f ⁻¹ᵁ Y.basicOpen s := hxs

Result:
case intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X.Hom Y
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
s : ↑Γ(Y, U)
hs : s ∈ f.ker.ideal ⟨U, hU⟩
hxs : (ConcreteCategory.hom f.base) x ∈ Y.basicOpen s
this : x ∈ f ⁻¹ᵁ Y.basicOpen s
⊢ False