awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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))

Tactic:
((inferInstance : (maximalIdeal Rₚ).IsPrime).mem_or_mem ?_).resolve_left this

Premises used: Set.Mem, inferInstance, Or.resolve_left, Ideal.IsPrime.mem_or_mem
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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ₚ
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)))
⊢ Membership.mem (γ := Ideal Rₚ) (maximalIdeal Rₚ : Ideal 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

Premises used: inferInstance, Or.resolve_left, Ideal.IsPrime.mem_or_mem
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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ₚ
h : Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R) : R ⧸ p) (0 : R ⧸ p)
⊢ 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:
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]

Premises used: map_sub, mul_inv_cancel₀, mul_sub, sub_self, IsLocalization.mk'_mul_cancel_left, mul_left_comm, Ideal.Quotient.eq_zero_iff_mem, map_mul, Ideal.mem_under, IsLocalization.AtPrime.isLocalRing, mul_one, IsLocalization.mul_mk'_eq_mk'_of_mul, IsLocalization.AtPrime.under_maximalIdeal
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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ₚ
h : (↑s : R) ∉ p
⊢ Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R) : R ⧸ p) (0 : R ⧸ p)

Tactic:
rw [Ne, Ideal.Quotient.eq_zero_iff_mem]

Premises used: Ne, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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ₚ
⊢ (↑s : R) ∉ p

Tactic:
s.prop

Premises used: Set.Mem, setOf, Subtype.prop, Not
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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ₚ
⊢ (↑s : R) ∉ p

Tactic:
exact s.prop

Premises used: Subtype.prop
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
⊢ Eq (α := 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) x) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) ((algebraMap R Rₚ : (a : R) → Rₚ) x) :
      HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
⊢ Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R) : R ⧸ p) (0 : R ⧸ p)

Tactic:
simpa [ne_eq, Ideal.Quotient.eq_zero_iff_mem] using Ideal.mem_primeCompl_iff.mp s.prop

Premises used: ne_eq, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_primeCompl_iff, Subtype.prop, Iff.mp
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
⊢ 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
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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)
rwa rwa₁ rwa₂ rwa₃ : Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) (↑s : R) : R ⧸ p) (0 : R ⧸ p)
⊢ 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:
rwa [RingEquiv.map_ne_zero_iff]

Premises used: RingEquiv.map_ne_zero_iff
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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)
⊢ 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]
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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))
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)) ⋯) ⋯)
      (Quotient.liftₐ (p ^ n) (ofId R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) ⋯))
    (AlgHom.id R (R ⧸ p ^ n))
⊢ AlgEquiv.{u_7, u_7, u_8} R (R ⧸ p ^ n) (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)

Tactic:
refine AlgEquiv.ofAlgHom (Ideal.Quotient.liftₐ _ (Algebra.ofId _ _) ?_) ?_ ?_ ?_

Premises used: Ideal.Quotient.liftₐ, AlgEquiv.ofAlgHom
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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)
refine_1₃ : p ^ n ≤ under R (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
refine_1₄ refine_1₅ : p ^ n ≤ p ^ 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))

Tactic:
rw [← Quotient.mk_comp_algebraMap, ← RingHom.comap_ker, mk_ker, ← under_def,
      under_maximalIdeal_pow p]

Premises used: RingHom.comap_ker, Ideal.under_def, IsLocalization.AtPrime.under_maximalIdeal_pow, Ideal.mk_ker, Ideal.Quotient.mk_comp_algebraMap
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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_2 :
  ∀ (x : Rₚ) (hx : x ∈ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n),
    Eq.{u_7 + 1} (α := R ⧸ p ^ n)
      ((liftAlgHom (R := R) (M := p.primeCompl) (f := Quotient.mkₐ R (p ^ n)) ⋯ : (a : Rₚ) → R ⧸ p ^ n) x : R ⧸ p ^ n)
      (0 : R ⧸ p ^ n)
⊢ AlgHom.{u_7, u_8, u_7} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n) (R ⧸ p ^ n)

Tactic:
refine Ideal.Quotient.liftₐ _
      (IsLocalization.liftAlgHom (f := Ideal.Quotient.mkₐ R (p ^ n)) fun (u : p.primeCompl) ↦
        Ideal.Quotient.isUnit_mk_pow_of_notMem _ <| mem_primeCompl_iff.mp u.prop) fun x hx ↦ ?_

Premises used: Ideal.Quotient.liftₐ
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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 : ℕ
x : Rₚ
hx : x ∈ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n
refine_2 :
  ∀ (a : R) (b : ↥p.primeCompl) (hx : mk' Rₚ a b ∈ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n),
    Eq.{u_7 + 1} (α := R ⧸ p ^ n)
      ((liftAlgHom (R := R) (M := p.primeCompl) (f := Quotient.mkₐ R (p ^ n)) ⋯ : (a : Rₚ) → R ⧸ p ^ n) (mk' Rₚ a b) :
        R ⧸ p ^ n)
      (0 : R ⧸ p ^ n)
⊢ Eq.{u_7 + 1} (α := R ⧸ p ^ n)
    ((liftAlgHom (R := R) (M := p.primeCompl) (f := Quotient.mkₐ R (p ^ n)) ⋯ : (a : Rₚ) → R ⧸ p ^ n) x : R ⧸ p ^ n)
    (0 : R ⧸ p ^ n)

Tactic:
obtain ⟨a, b, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x

Premises used: Ideal.primeCompl, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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 : ℕ
a : R
b : ↥p.primeCompl
hx : mk' Rₚ a b ∈ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n
⊢ a ∈ p ^ n

Tactic:
rw [IsLocalization.mk'_mem_iff, ← Ideal.mem_under, under_maximalIdeal_pow p] at hx

Premises used: IsLocalization.mk'_mem_iff, Ideal.mem_under, IsLocalization.AtPrime.under_maximalIdeal_pow
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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 : ℕ
a : R
b : ↥p.primeCompl
hx : a ∈ p ^ n
⊢ Eq.{u_7 + 1} (α := R ⧸ p ^ n)
    ((liftAlgHom (R := R) (M := p.primeCompl) (f := Quotient.mkₐ R (p ^ n)) ⋯ : (a : Rₚ) → R ⧸ p ^ n) (mk' Rₚ a b) :
      R ⧸ p ^ n)
    (0 : R ⧸ p ^ n)

Tactic:
simpa [lift_mk', Quotient.eq_zero_iff_mem] using hx

Premises used: IsLocalization.lift_mk', Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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_3 :
  Eq (α := Rₚ →ₐ[R] Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
    (AlgHom.comp
      (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)) ⋯) ⋯))
      (Quotient.mkₐ R (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)))
    (AlgHom.comp (AlgHom.id R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
      (Quotient.mkₐ R (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)))
⊢ 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))

Tactic:
rw [← AlgHom.cancel_right (Ideal.Quotient.mkₐ_surjective _ _)]

Premises used: AlgHom.cancel_right, Ideal.Quotient.mkₐ_surjective