-- 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
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:
apply le_antisymm

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

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)

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : ↑Y.affineOpens
⊢ f.ker.ideal U = RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

Tactic:
let I : IdealSheafData Y := ⟨fun U ↦ RingHom.ker (f.app U).hom, ?_⟩

Result:
case refine_2
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : ↑Y.affineOpens
I : Y.IdealSheafData :=
  { ideal := fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U)), map_ideal_basicOpen := ?refine_1 }
⊢ f.ker.ideal U = RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

case refine_1
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : ↑Y.affineOpens
⊢ ∀ (U : ↑Y.affineOpens) (f_1 : ↑Γ(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 f_1)

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

Tactic:
obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective (.powers s) x

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)
⊢ IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x => s ^ x) n, ⋯⟩ ∈
    Ideal.map (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) U)

Proof state:
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

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

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

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)
⊢ f ⁻¹ᵁ Y.basicOpen s = X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)

Tactic:
simp

Result:
no goals