awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
h₂ : ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
h :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) (mk' Sₚ x s))
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s)))
have h₃ : Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
  (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
    mk' Sₚ ((↑s : S) * x) s)
Tactic: rw [mul_sub, mul_mk'_eq_mk'_of_mul, mk'_mul_cancel_left, ← map_mul, ← map_sub, ← mem_comap,
    comap_map_eq_self_of_isMaximal _ IsPrime.ne_top', ← Ideal.Quotient.eq, map_mul, map_mul, hs,
    mul_comm, inv_mul_cancel_right₀ (Quotient.eq_zero_iff_mem.not.mpr h₁)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
h₂ : ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
h :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) (mk' Sₚ x s))
h₃ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      mk' Sₚ ((↑s : S) * x) s)
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s)))
have h₄ : Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
  (HSub.hSub (β := Sₚ)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ))
    ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
Tactic: rw [mul_sub, mul_mk'_eq_mk'_of_mul, mk'_mul_cancel_left, ← map_mul, ← map_sub, ← mem_comap,
    comap_map_eq_self_of_isMaximal _ IsPrime.ne_top', ← Ideal.Quotient.eq, map_mul, map_mul, hs,
    mul_comm, inv_mul_cancel_right₀ (Quotient.eq_zero_iff_mem.not.mpr h₁)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
h₂ : ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
h :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) (mk' Sₚ x s))
h₃ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      mk' Sₚ ((↑s : S) * x) s)
h₄ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (β := Sₚ)
      (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ))
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s)))
have h₅ : Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
  (HSub.hSub (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * (x * s')) : Sₚ)
    ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
Tactic: rw [mul_sub, mul_mk'_eq_mk'_of_mul, mk'_mul_cancel_left, ← map_mul, ← map_sub, ← mem_comap,
    comap_map_eq_self_of_isMaximal _ IsPrime.ne_top', ← Ideal.Quotient.eq, map_mul, map_mul, hs,
    mul_comm, inv_mul_cancel_right₀ (Quotient.eq_zero_iff_mem.not.mpr h₁)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
h₂ : ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
h :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) (mk' Sₚ x s))
h₃ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      mk' Sₚ ((↑s : S) * x) s)
h₄ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (β := Sₚ)
      (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ))
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
h₅ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * (x * s')) : Sₚ)
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s)))
have h₆ : Membership.mem.{u_4, u_4} (α := Sₚ) (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
  ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * (x * s') - x) : Sₚ)
Tactic: rw [mul_sub, mul_mk'_eq_mk'_of_mul, mk'_mul_cancel_left, ← map_mul, ← map_sub, ← mem_comap,
    comap_map_eq_self_of_isMaximal _ IsPrime.ne_top', ← Ideal.Quotient.eq, map_mul, map_mul, hs,
    mul_comm, inv_mul_cancel_right₀ (Quotient.eq_zero_iff_mem.not.mpr h₁)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
h₂ : ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
h :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) (mk' Sₚ x s))
h₃ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      mk' Sₚ ((↑s : S) * x) s)
h₄ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (β := Sₚ)
      (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ))
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
h₅ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * (x * s')) : Sₚ)
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
h₆ :
  Membership.mem.{u_4, u_4} (α := Sₚ) (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * (x * s') - x) : Sₚ)
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s)))
have h₇ : Membership.mem (γ := Ideal S) (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
  ((↑s : S) * (x * s') - x)
Tactic: rw [mul_sub, mul_mk'_eq_mk'_of_mul, mk'_mul_cancel_left, ← map_mul, ← map_sub, ← mem_comap,
    comap_map_eq_self_of_isMaximal _ IsPrime.ne_top', ← Ideal.Quotient.eq, map_mul, map_mul, hs,
    mul_comm, inv_mul_cancel_right₀ (Quotient.eq_zero_iff_mem.not.mpr h₁)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
h₂ : ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
h :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) (mk' Sₚ x s))
h₃ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      mk' Sₚ ((↑s : S) * x) s)
h₄ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (β := Sₚ)
      (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ))
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
h₅ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * (x * s')) : Sₚ)
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
h₆ :
  Membership.mem.{u_4, u_4} (α := Sₚ) (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * (x * s') - x) : Sₚ)
h₇ :
  Membership.mem (γ := Ideal S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) ((↑s : S) * (x * s') - x)
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s)))
have h₈ : (↑s : S) * (x * s') - x ∈ P
Tactic: rw [mul_sub, mul_mk'_eq_mk'_of_mul, mk'_mul_cancel_left, ← map_mul, ← map_sub, ← mem_comap,
    comap_map_eq_self_of_isMaximal _ IsPrime.ne_top', ← Ideal.Quotient.eq, map_mul, map_mul, hs,
    mul_comm, inv_mul_cancel_right₀ (Quotient.eq_zero_iff_mem.not.mpr h₁)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
h₂ : ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
h :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) (mk' Sₚ x s))
h₃ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      mk' Sₚ ((↑s : S) * x) s)
h₄ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (β := Sₚ)
      (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ))
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
h₅ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * (x * s')) : Sₚ)
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
h₆ :
  Membership.mem.{u_4, u_4} (α := Sₚ) (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * (x * s') - x) : Sₚ)
h₇ :
  Membership.mem (γ := Ideal S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) ((↑s : S) * (x * s') - x)
h₈ : (↑s : S) * (x * s') - x ∈ P
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s)))
have h₉ : Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) ((↑s : S) * (x * s')) : S ⧸ P)
  ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x : S ⧸ P)
Tactic: rw [mul_sub, mul_mk'_eq_mk'_of_mul, mk'_mul_cancel_left, ← map_mul, ← map_sub, ← mem_comap,
    comap_map_eq_self_of_isMaximal _ IsPrime.ne_top', ← Ideal.Quotient.eq, map_mul, map_mul, hs,
    mul_comm, inv_mul_cancel_right₀ (Quotient.eq_zero_iff_mem.not.mpr h₁)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
h₂ : ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
h :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) (mk' Sₚ x s))
h₃ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
      mk' Sₚ ((↑s : S) * x) s)
h₄ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (β := Sₚ)
      (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ))
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
h₅ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * (x * s')) : Sₚ)
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ))
h₆ :
  Membership.mem.{u_4, u_4} (α := Sₚ) (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * (x * s') - x) : Sₚ)
h₇ :
  Membership.mem (γ := Ideal S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) ((↑s : S) * (x * s') - x)
h₈ : (↑s : S) * (x * s') - x ∈ P
h₉ :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) ((↑s : S) * (x * s')) : S ⧸ P)
    ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) x : S ⧸ P)
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s)))
have h₁₀ : HMul.hMul (α := S ⧸ P) (β := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S) : S ⧸ P)
    ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (x * s') : S ⧸ P) =
  (Ideal.Quotient.mk P : (a : S) → S ⧸ P) x
Tactic: rw [mul_sub, mul_mk'_eq_mk'_of_mul, mk'_mul_cancel_left, ← map_mul, ← map_sub, ← mem_comap,
    comap_map_eq_self_of_isMaximal _ IsPrime.ne_top', ← Ideal.Quotient.eq, map_mul, map_mul, hs,
    mul_comm, inv_mul_cancel_right₀ (Quotient.eq_zero_iff_mem.not.mpr h₁)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : P.IsMaximal
⊢ P =
    RingHom.ker (F :=
      RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
      (algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
        RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
have rw : P =
  RingHom.ker (F :=
    RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (algebraMap Sₚ (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
        (algebraMap S Sₚ) :
      RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
Tactic: rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ _), ← RingHom.comap_ker, Quotient.algebraMap_eq,
        mk_ker, comap_map_eq_self_of_isMaximal _ (isPrime_map_of_liesOver S p Sₚ P).ne_top]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : P.IsMaximal
rw :
  P =
    RingHom.ker (F :=
      RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
          (algebraMap Sₚ (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
          (algebraMap S Sₚ) :
        RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
⊢ P =
    RingHom.ker (F :=
      RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
      (algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
        RingHom.{u_2, u_4} S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)))
have rw₁ : P =
  comap (F := S →+* Sₚ) (algebraMap S Sₚ : S →+* Sₚ)
    (RingHom.ker (F := Sₚ →+* HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      (algebraMap Sₚ (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))))
Tactic: rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ _), ← RingHom.comap_ker, Quotient.algebraMap_eq,
        mk_ker, comap_map_eq_self_of_isMaximal _ (isPrime_map_of_liesOver S p Sₚ P).ne_top]