-- 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.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 : (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ f.app (Y.basicOpen s))) x = 0
⊢ ((CommRingCat.Hom.hom (f.app ↑U)) x |_ f ⁻¹ᵁ Y.basicOpen s) ⋯ = 0

Tactic:
rwa [f.naturality] at hx

Result:
no goals

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

Tactic:
refine (IsLocalization.mk'_mem_map_algebraMap_iff _ _ _ _ _).mpr ?_

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)
⊢ ∃ s_1 ∈ Submonoid.powers s, s_1 * x ∈ (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) U

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

Tactic:
exact congr($(ofIdeals_ideal I).ideal U)

Result:
no goals

Proof state:
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 (f.app ↑U))
      (RingHom.ker
        (CommRingCat.Hom.hom (X.presheaf.map ((TopologicalSpace.Opens.map f.base).map (homOfLE ⋯).op.unop).op)))

Tactic:
exact Ideal.ker_le_comap _ hx

Result:
no goals

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 : (CommRingCat.Hom.hom (f.app (Y.basicOpen s))) (IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨s ^ n, ⋯⟩) = 0
⊢ (CommRingCat.Hom.hom (f.app (Y.basicOpen s))) ((algebraMap ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen s)) x) = 0

Tactic:
rw [← IsLocalization.mk'_spec' (M := .powers s), map_mul, hx, mul_zero]

Result:
no goals

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

Tactic:
simp_rw [RingHom.comap_ker, ← CommRingCat.hom_comp, Scheme.affineBasicOpen_coe, f.naturality,
  CommRingCat.hom_comp, ← RingHom.comap_ker]

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 (f.app ↑U))
      (RingHom.ker
        (CommRingCat.Hom.hom (X.presheaf.map ((TopologicalSpace.Opens.map f.base).map (homOfLE ⋯).op.unop).op)))

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 (f.app (Y.basicOpen s))) ((algebraMap ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen s)) x) = 0

Tactic:
simp only [Scheme.affineBasicOpen_coe, RingHom.mem_ker] at hx

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 : (CommRingCat.Hom.hom (f.app (Y.basicOpen s))) (IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨s ^ n, ⋯⟩) = 0
⊢ (CommRingCat.Hom.hom (f.app (Y.basicOpen s))) ((algebraMap ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen s)) x) = 0

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)
⊢ ∃ V, ∃ (hV : V = X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)), ((CommRingCat.Hom.hom (f.app ↑U)) x |_ V) ⋯ = 0

Tactic:
refine ⟨f ⁻¹ᵁ Y.basicOpen s, by simp, ?_⟩

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

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

Tactic:
intro U s

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

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 =
    (CommRingCat.Hom.hom (f.app (Y.basicOpen s))) ((algebraMap ↑Γ(Y, ↑U) ↑Γ(Y, Y.basicOpen s)) x)

Tactic:
simp [-NatTrans.naturality, RingHom.algebraMap_toAlgebra]

Result:
no goals

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)
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
⊢ (fun x => s ^ x) n * x ∈ (fun U => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))) U

Tactic:
simpa using hn

Result:
no goals