-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
@[simp]
lemma Hom.ker_apply (f : X.Hom Y) [QuasiCompact f] (U : Y.affineOpens) :
    f.ker.ideal U = RingHom.ker (f.app U).hom

Proof state:
case refine_1.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
x : ↑Γ(Y, Y.basicOpen s)
hx : x ∈ (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) (Y.affineBasicOpen s)
⊢ x ∈
    Ideal.map (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) U)

Tactic:
have := U.2.isLocalization_basicOpen s

Result:
case refine_1.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
x : ↑Γ(Y, Y.basicOpen s)
hx : x ∈ (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) (Y.affineBasicOpen s)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
⊢ x ∈
    Ideal.map (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) U)

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this✝ : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x => s ^ x) n, ⋯⟩ ∈
    (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) (Y.affineBasicOpen s)
this :
  ∃ V, ∃ (hV : V = X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)), ((CommRingCat.Hom.hom (f.app ↑U)) x |_ V) ⋯ = 0
⊢ ∃ s_1 ∈ Submonoid.powers s, s_1 * x ∈ (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) U

Tactic:
obtain ⟨_, rfl, H⟩ := this

Result:
case intro.intro
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x => s ^ x) n, ⋯⟩ ∈
    (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) (Y.affineBasicOpen s)
H : ((CommRingCat.Hom.hom (f.app ↑U)) x |_ X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)) ⋯ = 0
⊢ ∃ s_1 ∈ Submonoid.powers s, s_1 * x ∈ (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) U

Proof state:
case refine_1.a.intro.intro.mk.intro
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x => s ^ x) n, ⋯⟩ ∈
    (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) (Y.affineBasicOpen s)
⊢ ∃ s_1 ∈ Submonoid.powers s, s_1 * x ∈ (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) U

Tactic:
suffices ∃ (V : X.Opens) (hV : V = X.basicOpen ((f.app U).hom s)),
    letI := hV.trans_le (X.basicOpen_le _); ((f.app U).hom x |_ V) = 0 by
  obtain ⟨_, rfl, H⟩ := this
  obtain ⟨n, hn⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact
    X (U := f ⁻¹ᵁ U) (QuasiCompact.isCompact_preimage (f := f) _ U.1.2 U.2.isCompact)
    (f.app U x) (f.app U s) H
  exact ⟨_, ⟨n, rfl⟩, by simpa using hn⟩

Result:
case refine_1.a.intro.intro.mk.intro
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x => s ^ x) n, ⋯⟩ ∈
    (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) (Y.affineBasicOpen s)
⊢ ∃ V, ∃ (hV : V = X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)), ((CommRingCat.Hom.hom (f.app ↑U)) x |_ V) ⋯ = 0

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x => s ^ x) n, ⋯⟩ ∈
    (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) (Y.affineBasicOpen s)
⊢ (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ f.app (Y.basicOpen s))) x = 0

Tactic:
trans (f.app (Y.basicOpen s)).hom (algebraMap Γ(Y, U) _ x)

Result:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x => s ^ x) n, ⋯⟩ ∈
    (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) (Y.affineBasicOpen s)
⊢ (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ f.app (Y.basicOpen s))) x =
    (CommRingCat.Hom.hom (f.app (Y.basicOpen s))) ((algebraMap ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen s)) x)

X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x => s ^ x) n, ⋯⟩ ∈
    (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) (Y.affineBasicOpen s)
⊢ (CommRingCat.Hom.hom (f.app (Y.basicOpen s))) ((algebraMap ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen s)) x) = 0

Proof state:
case intro.intro.intro
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n✝ : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x => s ^ x) n✝, ⋯⟩ ∈
    (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) (Y.affineBasicOpen s)
H : ((CommRingCat.Hom.hom (f.app ↑U)) x |_ X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)) ⋯ = 0
n : ℕ
hn : (ConcreteCategory.hom (f.app ↑U)) s ^ n * (ConcreteCategory.hom (f.app ↑U)) x = 0
⊢ ∃ s_1 ∈ Submonoid.powers s, s_1 * x ∈ (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) U

Tactic:
exact ⟨_, ⟨n, rfl⟩, by simpa using hn⟩

Result:
no goals

Proof state:
case refine_1.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) U) ≤
    (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) (Y.affineBasicOpen s)

Tactic:
refine Ideal.map_le_iff_le_comap.mpr fun x hx ↦ ?_

Result:
case refine_1.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s x : ↑Γ(Y, ↑U)
hx : x ∈ (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) U
⊢ x ∈
    Ideal.comap (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) (Y.affineBasicOpen s))

Proof state:
case refine_1.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
⊢ (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) (Y.affineBasicOpen s) ≤
    Ideal.map (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) U)

Tactic:
intro x hx

Result:
case refine_1.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
x : ↑Γ(Y, Y.basicOpen s)
hx : x ∈ (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) (Y.affineBasicOpen s)
⊢ x ∈
    Ideal.map (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) U)