awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
⊢ Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)
have right : ∀ (y z : S), z ∉ P → ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)
Tactic: suffices ∀ y, ∀ z ∉ P, ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y) by
      simpa [(IsLocalization.mk'_surjective p.primeCompl).exists,
        (IsLocalization.mk'_surjective P.primeCompl).forall, P.over_def p,
        Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq, -map_mul,
        IsLocalization.eq_iff_exists P.primeCompl, Function.Surjective] using this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
y z : S
hzP : z ∉ P
⊢ ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)
have right : ∀ (a : S) (ha : a * y ∈ s) (haP : a ∈ (↑P.primeCompl : Set S)) (has : a ∈ (↑s.toSubmonoid : Set S)),
  ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)
Tactic: obtain ⟨a, ⟨haP, has⟩, ha⟩ := H.ge (Set.mem_univ y)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
y z : S
hzP : z ∉ P
a : S
ha : a * y ∈ s
haP : a ∈ (↑P.primeCompl : Set S)
has : a ∈ (↑s.toSubmonoid : Set S)
⊢ ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)
have right : ∀ (b : S) (hb : b * z ∈ s) (hbP : b ∈ (↑P.primeCompl : Set S)) (hbs : b ∈ (↑s.toSubmonoid : Set S)),
  ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)
Tactic: obtain ⟨b, ⟨hbP, hbs⟩, hb⟩ := H.ge (Set.mem_univ z)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
q : Ideal R
inst_1 : q.IsPrime
S : Type u_4
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : IsLocalization.AtPrime S q
p : Ideal R
inst_5 : p.IsPrime
hpq : p ≤ q
⊢ IsPrime.{u_4} (α := S) (map (F := R →+* S) (algebraMap R S) p)
have disj : Disjoint (↑q.primeCompl : Set R) (↑p : Set R)
Tactic: have disj : Disjoint (q.primeCompl : Set R) p := by
    simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left, hpq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
q : Ideal R
inst_1 : q.IsPrime
S : Type u_4
inst_2 : CommSemiring S
inst_3 : Algebra R S
inst_4 : IsLocalization.AtPrime S q
p : Ideal R
inst_5 : p.IsPrime
hpq : p ≤ q
⊢ under.{u_1, u_4} R (B := S) (map (F := R →+* S) (algebraMap R S) p) = p
have disj : Disjoint (↑q.primeCompl : Set R) (↑p : Set R)
Tactic: have disj : Disjoint (q.primeCompl : Set R) p := by
    simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left, hpq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
inst_11 : IsLocalization M R'
inst_12 : IsLocalization T S'
p : Ideal R
P : Ideal S
inst_13 : P.IsPrime
inst_14 : P.LiesOver p
disj : Disjoint (↑T : Set S) (↑P : Set S)
h :
  Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under R (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
⊢ Eq (α := Ideal R') (Ideal.map (F := R →+* R') (algebraMap R R') p)
    (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))
have rw : Eq (α := Ideal R')
  (Ideal.map (F := R →+* R') (algebraMap R R')
    (under R (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
  (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))
Tactic: rw [← h, IsLocalization.map_under (M := M)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
inst_11 : IsLocalization M R'
inst_12 : IsLocalization T S'
p : Ideal R
P : Ideal S
inst_13 : P.IsPrime
inst_14 : P.LiesOver p
disj : Disjoint (↑T : Set S) (↑P : Set S)
h :
  Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under R (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
rw :
  Eq (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under R (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
    (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))
⊢ Eq (α := Ideal R') (Ideal.map (F := R →+* R') (algebraMap R R') p)
    (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))
have rw₁ : Eq (α := Ideal R') (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))
  (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))
Tactic: rw [← h, IsLocalization.map_under (M := M)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
inst_11 : IsLocalization M R'
inst_12 : IsLocalization T S'
p : Ideal R
P : Ideal S
inst_13 : P.IsPrime
inst_14 : P.LiesOver p
disj : Disjoint (↑T : Set S) (↑P : Set S)
⊢ LiesOver.{u_5, u_6} (A := R') (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P)
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
have suffices : Eq.{u_5 + 1} (α := Ideal R')
  (Ideal.map (F := R →+* R') (algebraMap R R')
    (under R (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
  (Ideal.map (F := R →+* R') (algebraMap R R') p)
Tactic: suffices h : Ideal.map (algebraMap R R') (under R (under R' (P.map (algebraMap S S')))) =
      Ideal.map (algebraMap R R') p from ⟨by rw [← h, IsLocalization.map_under (M := M)]⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
inst_11 : IsLocalization M R'
inst_12 : IsLocalization T S'
p : Ideal R
P : Ideal S
inst_13 : P.IsPrime
inst_14 : P.LiesOver p
disj : Disjoint (↑T : Set S) (↑P : Set S)
⊢ Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under R (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
have rw : Eq.{u_5 + 1} (α := Ideal R')
  (Ideal.map (F := R →+* R') (algebraMap R R')
    (under.{u_1, u_6} R (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P)))
  (Ideal.map (F := R →+* R') (algebraMap R R') p)
Tactic: rw [under_under, ← under_under (B := S), under_map_of_isPrime_disjoint _ _ ‹_› disj,
    LiesOver.over (P := P) (p := p)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
inst_11 : IsLocalization M R'
inst_12 : IsLocalization T S'
p : Ideal R
P : Ideal S
inst_13 : P.IsPrime
inst_14 : P.LiesOver p
disj : Disjoint (↑T : Set S) (↑P : Set S)
rw :
  Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under.{u_1, u_6} R (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P)))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
⊢ Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under R (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
have rw₁ : Eq.{u_5 + 1} (α := Ideal R')
  (Ideal.map (F := R →+* R') (algebraMap R R')
    (under R (under.{u_4, u_6} S (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
  (Ideal.map (F := R →+* R') (algebraMap R R') p)
Tactic: rw [under_under, ← under_under (B := S), under_map_of_isPrime_disjoint _ _ ‹_› disj,
    LiesOver.over (P := P) (p := p)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
inst_11 : IsLocalization M R'
inst_12 : IsLocalization T S'
p : Ideal R
P : Ideal S
inst_13 : P.IsPrime
inst_14 : P.LiesOver p
disj : Disjoint (↑T : Set S) (↑P : Set S)
rw :
  Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under.{u_1, u_6} R (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P)))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
rw₁ :
  Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under R (under.{u_4, u_6} S (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
⊢ Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under R (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
have rw₂ : Eq.{u_5 + 1} (α := Ideal R') (Ideal.map (F := R →+* R') (algebraMap R R') (under R P))
  (Ideal.map (F := R →+* R') (algebraMap R R') p)
Tactic: rw [under_under, ← under_under (B := S), under_map_of_isPrime_disjoint _ _ ‹_› disj,
    LiesOver.over (P := P) (p := p)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
inst_11 : IsLocalization M R'
inst_12 : IsLocalization T S'
p : Ideal R
P : Ideal S
inst_13 : P.IsPrime
inst_14 : P.LiesOver p
disj : Disjoint (↑T : Set S) (↑P : Set S)
rw :
  Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under.{u_1, u_6} R (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P)))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
rw₁ :
  Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under R (under.{u_4, u_6} S (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
rw₂ :
  Eq.{u_5 + 1} (α := Ideal R') (Ideal.map (F := R →+* R') (algebraMap R R') (under R P))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
⊢ Eq.{u_5 + 1} (α := Ideal R')
    (Ideal.map (F := R →+* R') (algebraMap R R')
      (under R (under.{u_5, u_6} R' (B := S') (Ideal.map (F := S →+* S') (algebraMap S S') P))))
    (Ideal.map (F := R →+* R') (algebraMap R R') p)
have rw₃ : Eq.{u_5 + 1} (α := Ideal R') (Ideal.map (F := R →+* R') (algebraMap R R') (under R P))
  (Ideal.map (F := R →+* R') (algebraMap R R') (under R P))
Tactic: rw [under_under, ← under_under (B := S), under_map_of_isPrime_disjoint _ _ ‹_› disj,
    LiesOver.over (P := P) (p := p)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
inst_4 : IsMaximal (under R J)
⊢ J.IsMaximal
have obtain : ∀ (m : Ideal S) (maxm : m.IsMaximal) (hm : J ≤ m), J.IsMaximal
Tactic: obtain ⟨m, maxm, hm⟩ := exists_le_maximal J <| by
    rintro rfl
    exact Ideal.IsMaximal.ne_top ‹_› (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
inst_4 : IsMaximal (under R J)
m : Ideal S
maxm : m.IsMaximal
hm : J ≤ m
⊢ J.IsMaximal
have hm₁ : LE.le (α := Ideal R) (under R J) (under R m)
Tactic: replace hm : under R J ≤ under R m := comap_mono hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
inst_4 : IsMaximal (under R J)
m : Ideal S
maxm : m.IsMaximal
hm : LE.le (α := Ideal R) (under R J) (under R m)
⊢ J.IsMaximal
have rwa : IsMaximal.{u_4} (α := S) (map (F := R →+* S) (algebraMap R S) (under R J))
Tactic: rwa [← IsLocalization.map_under M S J, IsMaximal.eq_of_le ‹_› (IsPrime.under R m).ne_top hm,
    IsLocalization.map_under M S m]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
inst_4 : IsMaximal (under R J)
m : Ideal S
maxm : m.IsMaximal
hm : LE.le (α := Ideal R) (under R J) (under R m)
rwa : IsMaximal.{u_4} (α := S) (map (F := R →+* S) (algebraMap R S) (under R J))
⊢ J.IsMaximal
have rwa₁ : IsMaximal.{u_4} (α := S) (map (F := R →+* S) (algebraMap R S) (under R m))
Tactic: rwa [← IsLocalization.map_under M S J, IsMaximal.eq_of_le ‹_› (IsPrime.under R m).ne_top hm,
    IsLocalization.map_under M S m]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
inst_1 : p.IsPrime
Rₚ : Type u_4
inst_2 : CommSemiring Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
⊢ Eq (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p) (maximalIdeal Rₚ)
have h : Eq (α := Ideal Rₚ) (maximalIdeal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) (under R (maximalIdeal Rₚ)))
Tactic: convert! congr_arg (Ideal.map (algebraMap R Rₚ)) (under_maximalIdeal Rₚ p).symm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
inst_1 : p.IsPrime
Rₚ : Type u_4
inst_2 : CommSemiring Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
⊢ Eq (α := Ideal Rₚ) (maximalIdeal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) (under R (maximalIdeal Rₚ)))
have h : Eq (α := Ideal Rₚ) (maximalIdeal Rₚ) (maximalIdeal Rₚ)
Tactic: rw [map_under p.primeCompl]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P_1 : Type u_3
inst_3 : CommSemiring P_1
p : Ideal R
inst_4 : p.IsPrime
Rₚ : Type u_4
inst_5 : CommSemiring Rₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization.AtPrime Rₚ p
inst_8 : IsLocalRing Rₚ
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_12 : Algebra Rₚ Sₚ
P : Ideal S
⊢ IsMaximal.{u_4} (α := Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p)
have rw : IsMaximal (maximalIdeal Rₚ)
Tactic: rw [map_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
inst_1 : p.IsPrime
Rₚ : Type u_4
inst_2 : CommSemiring Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
inst_6 : p.IsMaximal
n : ℕ
⊢ under R (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n) = p ^ n
have h : ∀ (x : R), Membership.mem (γ := Ideal R) (under R (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) x ↔ x ∈ p ^ n
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
inst_1 : p.IsPrime
Rₚ : Type u_4
inst_2 : CommSemiring Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
inst_6 : p.IsMaximal
n : ℕ
x : R
⊢ Membership.mem (γ := Ideal R) (under R (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) x ↔ x ∈ p ^ n
have h : (∃ m ∈ p.primeCompl, m * x ∈ p ^ n) ↔ x ∈ p ^ n
Tactic: rw [mem_comap, ← map_eq_maximalIdeal p Rₚ, ← Ideal.map_pow,
    algebraMap_mem_map_algebraMap_iff p.primeCompl Rₚ]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
inst_1 : p.IsPrime
Rₚ : Type u_4
inst_2 : CommSemiring Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
inst_6 : p.IsMaximal
n : ℕ
x : R
⊢ (∃ m ∈ p.primeCompl, m * x ∈ p ^ n) ↔ x ∈ p ^ n
have h : (∃ m ∈ p.primeCompl, m * x ∈ p ^ n) → ∀ (m : R) (hm : m ∈ p.primeCompl) (h : m * x ∈ p ^ n), x ∈ p ^ n
Tactic: refine ⟨fun ⟨m, hm, h⟩ ↦ ?_, fun h ↦ ⟨1, by simp, by simp [h]⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
⊢ RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
have refine_1 : p =
  RingHom.ker (F := RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
    (algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) :
      RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
Tactic: refine (Ideal.quotEquivOfEq ?_).trans
    (RingHom.quotientKerEquivOfSurjective (f := algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
refine_1 :
  p =
    RingHom.ker (F := RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
      (algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) :
        RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
⊢ RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
have refine_2 : Function.Surjective.{u_7 + 1, u_8 + 1} (α := R) (β := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
  (⇑(algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) :
        RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
    (a : R) → Rₚ ⧸ maximalIdeal Rₚ)
Tactic: refine (Ideal.quotEquivOfEq ?_).trans
    (RingHom.quotientKerEquivOfSurjective (f := algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
⊢ p =
    RingHom.ker (F := RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
      (algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) :
        RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
have refine_1 : p =
  RingHom.ker (F := RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (algebraMap Rₚ (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) (algebraMap R Rₚ) :
      RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
Tactic: rw [IsScalarTower.algebraMap_eq R Rₚ, ← RingHom.comap_ker, ← under_def,
      Ideal.Quotient.algebraMap_eq, Ideal.mk_ker, IsLocalization.AtPrime.under_maximalIdeal Rₚ p]