awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
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ₚ
x : R
s : ↥p.primeCompl
s' : R
hs :
  Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) s' : R ⧸ p)
    (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R))⁻¹ : R ⧸ p)
⊢ Membership.mem (γ := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ)
    (HSub.hSub (α := Rₚ) ((algebraMap R Rₚ : (a : R) → Rₚ) (x * s') : Rₚ) (mk' Rₚ x s))
have this : ((algebraMap R Rₚ : (a : R) → Rₚ) (↑s : R) : Rₚ) ∉ maximalIdeal Rₚ
Tactic: have : algebraMap R Rₚ s ∉ maximalIdeal Rₚ := by
      rw [← Ideal.mem_under, IsLocalization.AtPrime.under_maximalIdeal Rₚ p]
      exact s.prop
-- 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ₚ
x : R
s : ↥p.primeCompl
s' : R
hs :
  Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) s' : R ⧸ p)
    (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R))⁻¹ : R ⧸ p)
this : ((algebraMap R Rₚ : (a : R) → Rₚ) (↑s : R) : Rₚ) ∉ maximalIdeal Rₚ
⊢ Membership.mem (γ := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ)
    (HSub.hSub (α := Rₚ) ((algebraMap R Rₚ : (a : R) → Rₚ) (x * s') : Rₚ) (mk' Rₚ x s))
have h : Membership.mem (γ := Ideal Rₚ) (maximalIdeal Rₚ)
  (HMul.hMul (α := Rₚ) ((algebraMap R Rₚ : (a : R) → Rₚ) (↑s : R) : Rₚ)
    (HSub.hSub (α := Rₚ) ((algebraMap R Rₚ : (a : R) → Rₚ) (x * s') : Rₚ) (mk' Rₚ x s)))
Tactic: refine ((inferInstance : (maximalIdeal Rₚ).IsPrime).mem_or_mem ?_).resolve_left this
-- 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ₚ
x : R
s : ↥p.primeCompl
s' : R
hs :
  Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) s' : R ⧸ p)
    (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R))⁻¹ : R ⧸ p)
this : ((algebraMap R Rₚ : (a : R) → Rₚ) (↑s : R) : Rₚ) ∉ maximalIdeal Rₚ
⊢ Membership.mem (γ := Ideal Rₚ) (maximalIdeal Rₚ)
    (HMul.hMul (α := Rₚ) ((algebraMap R Rₚ : (a : R) → Rₚ) (↑s : R) : Rₚ)
      (HSub.hSub (α := Rₚ) ((algebraMap R Rₚ : (a : R) → Rₚ) (x * s') : Rₚ) (mk' Rₚ x s)))
have h : Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R) : R ⧸ p) (0 : R ⧸ p)
Tactic: rw [mul_sub, IsLocalization.mul_mk'_eq_mk'_of_mul, IsLocalization.mk'_mul_cancel_left,
      ← map_mul, ← map_sub, ← Ideal.mem_under, under_maximalIdeal Rₚ p,
      mul_left_comm, ← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_mul, map_mul, hs,
      mul_inv_cancel₀, mul_one, sub_self]
-- 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ₚ
x : R
s : ↥p.primeCompl
s' : R
hs :
  Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) s' : R ⧸ p)
    (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R))⁻¹ : R ⧸ p)
this : ((algebraMap R Rₚ : (a : R) → Rₚ) (↑s : R) : Rₚ) ∉ maximalIdeal Rₚ
⊢ Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R) : R ⧸ p) (0 : R ⧸ p)
have h : (↑s : R) ∉ p
Tactic: rw [Ne, Ideal.Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
Goal:
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Rₚ : Type u_8
inst_2 : CommRing Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
⊢ ((RingEquiv.symm (equivQuotMaximalIdeal p Rₚ) :
          RingEquiv.{u_8, u_7} (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (R ⧸ p)) :
        (a : Rₚ ⧸ maximalIdeal Rₚ) → R ⧸ p)
      ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) (mk' Rₚ x s)) =
    HMul.hMul (α := R ⧸ p) (β := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) x : R ⧸ p)
      (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R))⁻¹ : R ⧸ p)
have h₁ : Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R) : R ⧸ p) (0 : R ⧸ p)
Tactic: have h₁ : Ideal.Quotient.mk p ↑s ≠ 0 := by
    simpa [ne_eq, Ideal.Quotient.eq_zero_iff_mem] using Ideal.mem_primeCompl_iff.mp s.prop
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
Goal:
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Rₚ : Type u_8
inst_2 : CommRing Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
h₁ : Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R) : R ⧸ p) (0 : R ⧸ p)
⊢ ((RingEquiv.symm (equivQuotMaximalIdeal p Rₚ) :
          RingEquiv.{u_8, u_7} (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (R ⧸ p)) :
        (a : Rₚ ⧸ maximalIdeal Rₚ) → R ⧸ p)
      ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) (mk' Rₚ x s)) =
    HMul.hMul (α := R ⧸ p) (β := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) x : R ⧸ p)
      (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R))⁻¹ : R ⧸ p)
have h₂ : Ne.{u_8 + 1} (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
  (((equivQuotMaximalIdeal p Rₚ :
          RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
        (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
      ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R)) :
    HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
  (0 : HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
Tactic: have h₂ : equivQuotMaximalIdeal p Rₚ (Ideal.Quotient.mk p ↑s) ≠ 0 := by
    rwa [RingEquiv.map_ne_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Rₚ : Type u_8
inst_2 : CommRing Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
h₁ : Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R) : R ⧸ p) (0 : R ⧸ p)
h₂ :
  Ne.{u_8 + 1} (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    (((equivQuotMaximalIdeal p Rₚ :
            RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
          (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
        ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R)) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    (0 : HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
⊢ ((RingEquiv.symm (equivQuotMaximalIdeal p Rₚ) :
          RingEquiv.{u_8, u_7} (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (R ⧸ p)) :
        (a : Rₚ ⧸ maximalIdeal Rₚ) → R ⧸ p)
      ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) (mk' Rₚ x s)) =
    HMul.hMul (α := R ⧸ p) (β := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) x : R ⧸ p)
      (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R))⁻¹ : R ⧸ p)
have rw : Eq (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
  ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) (mk' Rₚ x s) :
    HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ))
  (((equivQuotMaximalIdeal p Rₚ :
          RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
        (a : R ⧸ p) → Rₚ ⧸ maximalIdeal Rₚ)
      (HMul.hMul (α := R ⧸ p) (β := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) x : R ⧸ p)
        (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R))⁻¹ : R ⧸ p)) :
    HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
Tactic: rw [RingEquiv.symm_apply_eq, ← mul_left_inj' h₂, map_mul, mul_assoc, ← map_mul,
    inv_mul_cancel₀ h₁, map_one, mul_one, equivQuotMaximalIdeal_apply_mk, ← map_mul,
    mk'_spec, Ideal.Quotient.mk_algebraMap, equivQuotMaximalIdeal_apply_mk,
    Ideal.Quotient.mk_algebraMap]
-- 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ₚ
n : ℕ
⊢ AlgEquiv.{u_7, u_7, u_8} R (R ⧸ p ^ n) (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
have refine_1 : ∀ a ∈ p ^ n,
  Eq.{u_8 + 1} (α := Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
    ((ofId R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n) : (a : R) → Rₚ ⧸ maximalIdeal Rₚ ^ n) a :
      Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
    (0 : Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
Tactic: refine AlgEquiv.ofAlgHom (Ideal.Quotient.liftₐ _ (Algebra.ofId _ _) ?_) ?_ ?_ ?_
-- 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ₚ
n : ℕ
refine_1 :
  ∀ a ∈ p ^ n,
    Eq.{u_8 + 1} (α := Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
      ((ofId R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n) : (a : R) → Rₚ ⧸ maximalIdeal Rₚ ^ n) a :
        Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
      (0 : Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
⊢ AlgEquiv.{u_7, u_7, u_8} R (R ⧸ p ^ n) (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
have refine_2 : AlgHom.{u_7, u_8, u_7} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n) (R ⧸ p ^ n)
Tactic: refine AlgEquiv.ofAlgHom (Ideal.Quotient.liftₐ _ (Algebra.ofId _ _) ?_) ?_ ?_ ?_
-- 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ₚ
n : ℕ
refine_1 :
  ∀ a ∈ p ^ n,
    Eq.{u_8 + 1} (α := Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
      ((ofId R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n) : (a : R) → Rₚ ⧸ maximalIdeal Rₚ ^ n) a :
        Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
      (0 : Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
refine_2 : AlgHom.{u_7, u_8, u_7} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n) (R ⧸ p ^ n)
⊢ AlgEquiv.{u_7, u_7, u_8} R (R ⧸ p ^ n) (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
have refine_3 : Eq (α := Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n →ₐ[R] Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
  (AlgHom.comp (Quotient.liftₐ (p ^ n) (ofId R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) sorry)
    (Quotient.liftₐ (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
      (liftAlgHom (R := R) (M := p.primeCompl) (f := Quotient.mkₐ R (p ^ n)) sorry) sorry))
  (AlgHom.id R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
Tactic: refine AlgEquiv.ofAlgHom (Ideal.Quotient.liftₐ _ (Algebra.ofId _ _) ?_) ?_ ?_ ?_
-- 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ₚ
n : ℕ
refine_1 :
  ∀ a ∈ p ^ n,
    Eq.{u_8 + 1} (α := Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
      ((ofId R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n) : (a : R) → Rₚ ⧸ maximalIdeal Rₚ ^ n) a :
        Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
      (0 : Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
refine_2 : AlgHom.{u_7, u_8, u_7} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n) (R ⧸ p ^ n)
refine_3 :
  Eq (α := Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n →ₐ[R] Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
    (AlgHom.comp (Quotient.liftₐ (p ^ n) (ofId R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) ⋯)
      (Quotient.liftₐ (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
        (liftAlgHom (R := R) (M := p.primeCompl) (f := Quotient.mkₐ R (p ^ n)) ⋯) ⋯))
    (AlgHom.id R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
⊢ AlgEquiv.{u_7, u_7, u_8} R (R ⧸ p ^ n) (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
have refine_4 : Eq (α := R ⧸ p ^ n →ₐ[R] R ⧸ p ^ n)
  (AlgHom.comp
    (Quotient.liftₐ (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
      (liftAlgHom (R := R) (M := p.primeCompl) (f := Quotient.mkₐ R (p ^ n)) sorry) sorry)
    (Quotient.liftₐ (p ^ n) (ofId R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) sorry))
  (AlgHom.id R (R ⧸ p ^ n))
Tactic: refine AlgEquiv.ofAlgHom (Ideal.Quotient.liftₐ _ (Algebra.ofId _ _) ?_) ?_ ?_ ?_
-- 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ₚ
n : ℕ
⊢ p ^ n ≤
    RingHom.ker (F := RingHom.{u_7, u_8} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
      (algebraMap R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
have refine_1 : p ^ n ≤
  RingHom.ker (F := RingHom.{u_7, u_8} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
    (RingHom.comp (Ideal.Quotient.mk (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) (algebraMap R Rₚ))
Tactic: rw [← Quotient.mk_comp_algebraMap, ← RingHom.comap_ker, mk_ker, ← under_def,
      under_maximalIdeal_pow p]
-- 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ₚ
n : ℕ
refine_1 :
  p ^ n ≤
    RingHom.ker (F := RingHom.{u_7, u_8} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
      (RingHom.comp (Ideal.Quotient.mk (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) (algebraMap R Rₚ))
⊢ p ^ n ≤
    RingHom.ker (F := RingHom.{u_7, u_8} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
      (algebraMap R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
have refine_1₁ : p ^ n ≤
  comap (F := R →+* Rₚ) (algebraMap R Rₚ)
    (RingHom.ker (F := Rₚ →+* Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
      (Ideal.Quotient.mk (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)))
Tactic: rw [← Quotient.mk_comp_algebraMap, ← RingHom.comap_ker, mk_ker, ← under_def,
      under_maximalIdeal_pow p]
-- 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ₚ
n : ℕ
refine_1 :
  p ^ n ≤
    RingHom.ker (F := RingHom.{u_7, u_8} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
      (RingHom.comp (Ideal.Quotient.mk (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) (algebraMap R Rₚ))
refine_1₁ :
  p ^ n ≤
    comap (F := R →+* Rₚ) (algebraMap R Rₚ)
      (RingHom.ker (F := Rₚ →+* Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
        (Ideal.Quotient.mk (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)))
⊢ p ^ n ≤
    RingHom.ker (F := RingHom.{u_7, u_8} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
      (algebraMap R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
have refine_1₂ : p ^ n ≤ comap (F := R →+* Rₚ) (algebraMap R Rₚ) (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
Tactic: rw [← Quotient.mk_comp_algebraMap, ← RingHom.comap_ker, mk_ker, ← under_def,
      under_maximalIdeal_pow p]
-- 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ₚ
n : ℕ
refine_1 :
  p ^ n ≤
    RingHom.ker (F := RingHom.{u_7, u_8} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
      (RingHom.comp (Ideal.Quotient.mk (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) (algebraMap R Rₚ))
refine_1₁ :
  p ^ n ≤
    comap (F := R →+* Rₚ) (algebraMap R Rₚ)
      (RingHom.ker (F := Rₚ →+* Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
        (Ideal.Quotient.mk (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)))
refine_1₂ : p ^ n ≤ comap (F := R →+* Rₚ) (algebraMap R Rₚ) (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
⊢ p ^ n ≤
    RingHom.ker (F := RingHom.{u_7, u_8} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
      (algebraMap R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
have refine_1₃ : p ^ n ≤ under R (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
Tactic: rw [← Quotient.mk_comp_algebraMap, ← RingHom.comap_ker, mk_ker, ← under_def,
      under_maximalIdeal_pow p]