-- Mathlib/AlgebraicGeometry/SpreadingOut.lean
protected
lemma Scheme.IsGermInjective.Spec
    (H : ∀ I : Ideal R, I.IsPrime →
      ∃ f : R, f ∉ I ∧ ∀ (x y : R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0) :
    (Spec R).IsGermInjective

Proof state:
case intro.intro
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ ∃ U, ∃ (hx : p ∈ U), IsAffineOpen U ∧ Function.Injective ⇑(ConcreteCategory.hom ((Spec R).presheaf.germ U p hx))

Tactic:
refine ⟨PrimeSpectrum.basicOpen f, hf, ?_, ?_⟩

Result:
case intro.intro.refine_1
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ IsAffineOpen (PrimeSpectrum.basicOpen f)

case intro.intro.refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ Function.Injective ⇑(ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))

Proof state:
case intro.intro.refine_2.intro.intro
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
      (IsLocalization.mk' (↑((Spec.structureSheaf ↑R).val.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s) =
    0
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).val.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0

Tactic:
rw [← RingHom.mem_ker, IsLocalization.mk'_eq_mul_mk'_one, Ideal.mul_unit_mem_iff_mem,
  RingHom.mem_ker, RingHom.algebraMap_toAlgebra] at hx

Result:
case intro.intro.refine_2.intro.intro
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
      ((CommRingCat.Hom.hom (StructureSheaf.toOpen (↑R) (Opposite.unop (Opposite.op (PrimeSpectrum.basicOpen f))))) x) =
    0
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).val.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0

case intro.intro.refine_2.intro.intro.hy
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (algebraMap ↑R ↑((Spec.structureSheaf ↑R).val.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x *
      IsLocalization.mk' (↑((Spec.structureSheaf ↑R).val.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) 1 s ∈
    RingHom.ker (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
⊢ IsUnit (IsLocalization.mk' (↑((Spec.structureSheaf ↑R).val.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) 1 s)

Proof state:
case intro.intro.refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ ∀ (x : ↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f)))),
    (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf)) x = 0 → x = 0

Tactic:
intro x hx

Result:
case intro.intro.refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f)))
hx : (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf)) x = 0
⊢ x = 0

Proof state:
case intro.intro.refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ Function.Injective ⇑(ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))

Tactic:
rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]

Result:
case intro.intro.refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ ∀ (x : ↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f)))),
    (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf)) x = 0 → x = 0

Proof state:
case intro.intro.refine_2.intro.intro.intro.mk.intro
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx : (ConcreteCategory.hom (StructureSheaf.toStalk (↑R) p)) x = 0
y : ↑R
hy : y ∈ p.asIdeal.primeCompl
hy' : ↑⟨y, hy⟩ * x = 0
n : ℕ
hn : f ^ n * x = 0
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).val.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0

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

Result:
case intro.intro.refine_2.intro.intro.intro.mk.intro
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx : (ConcreteCategory.hom (StructureSheaf.toStalk (↑R) p)) x = 0
y : ↑R
hy : y ∈ p.asIdeal.primeCompl
hy' : ↑⟨y, hy⟩ * x = 0
n : ℕ
hn : f ^ n * x = 0
⊢ ∃ m, ↑m * x = 0

Proof state:
case intro.intro.refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f)))
hx : (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf)) x = 0
⊢ x = 0

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective
  (S := ((Spec.structureSheaf R).val.obj (.op <| PrimeSpectrum.basicOpen f))) (.powers f) x

Result:
case intro.intro.refine_2.intro.intro
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↑↑(Spec R).toPresheafedSpace
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
      (IsLocalization.mk' (↑((Spec.structureSheaf ↑R).val.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s) =
    0
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).val.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0