awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
h : (∃ m ∈ p.primeCompl, m * x ∈ p ^ n) ↔ x ∈ p ^ n
⊢ Membership.mem (γ := Ideal R) (under R (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) x ↔ x ∈ p ^ n

Tactic:
rw [mem_comap, ← map_eq_maximalIdeal p Rₚ, ← Ideal.map_pow,
    algebraMap_mem_map_algebraMap_iff p.primeCompl Rₚ]

Premises used: IsLocalization.algebraMap_mem_map_algebraMap_iff, IsLocalization.AtPrime.map_eq_maximalIdeal, Ideal.primeCompl, Ideal.mem_comap, Ideal.map_pow
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
h : x ∈ p ^ n
⊢ 1 ∈ p.primeCompl

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
h : x ∈ p ^ n
⊢ 1 * x ∈ p ^ n

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
h : (∃ m ∈ p.primeCompl, m * x ∈ p ^ n) → ∀ (m : R) (hm : m ∈ p.primeCompl) (h : m * x ∈ p ^ n), x ∈ p ^ n
⊢ (∃ m ∈ p.primeCompl, m * x ∈ p ^ n) ↔ x ∈ p ^ n

Tactic:
refine ⟨fun ⟨m, hm, h⟩ ↦ ?_, fun h ↦ ⟨1, by simp, by simp [h]⟩⟩
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
h_1 : ∃ m ∈ p.primeCompl, m * x ∈ p ^ n
m : R
hm : m ∈ p.primeCompl
h : m * x ∈ p ^ n
⊢ x ∈ p ^ n

Tactic:
(IsMaximal.mul_mem_pow _ h).resolve_left (mem_primeCompl_iff.mp hm)

Premises used: Or.resolve_left, Ideal.mem_primeCompl_iff, Ideal.IsMaximal.mul_mem_pow, Iff.mp
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
h_1 : ∃ m ∈ p.primeCompl, m * x ∈ p ^ n
m : R
hm : m ∈ p.primeCompl
h : m * x ∈ p ^ n
⊢ x ∈ p ^ n

Tactic:
exact (IsMaximal.mul_mem_pow _ h).resolve_left (mem_primeCompl_iff.mp hm)

Premises used: Or.resolve_left, Ideal.mem_primeCompl_iff, Ideal.IsMaximal.mul_mem_pow, Iff.mp
-- 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ₚ
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ₚ)))
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ₚ)
⊢ RingEquiv.{u_7, u_8} (R ⧸ p) (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))

Tactic:
refine (Ideal.quotEquivOfEq ?_).trans
    (RingHom.quotientKerEquivOfSurjective (f := algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) ?_)

Premises used: Ideal.quotEquivOfEq, RingHom.quotientKerEquivOfSurjective, RingEquiv.trans
-- 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ₚ
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ₚ)))
refine_1₁ :
  p =
    comap (F := R →+* Rₚ) (algebraMap R Rₚ : R →+* Rₚ)
      (RingHom.ker (F := Rₚ →+* HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
        (algebraMap Rₚ (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))))
refine_1₂ :
  p =
    under R
      (RingHom.ker (F := Rₚ →+* HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
        (algebraMap Rₚ (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))))
refine_1₃ :
  p =
    under R
      (RingHom.ker (F := Rₚ →+* HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
        (Ideal.Quotient.mk (maximalIdeal Rₚ)))
refine_1₄ : p = under R (maximalIdeal Rₚ)
refine_1₅ refine_1₆ : p = p
⊢ 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:
rw [IsScalarTower.algebraMap_eq R Rₚ, ← RingHom.comap_ker, ← under_def,
      Ideal.Quotient.algebraMap_eq, Ideal.mk_ker, IsLocalization.AtPrime.under_maximalIdeal Rₚ p]

Premises used: Ideal.Quotient.algebraMap_eq, RingHom.comap_ker, Ideal.under_def, IsLocalization.AtPrime.isLocalRing, IsScalarTower.algebraMap_eq, Ideal.mk_ker, 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 : HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)
refine_2 :
  ∀ (x : Rₚ),
    ∃ (a : R),
      Eq.{u_8 + 1} (α := 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ₚ)
            a :
          HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
        ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) x :
          HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ))
⊢ ∃ (a : 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ₚ)
        a =
      x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- 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ₚ
refine_2 :
  ∀ (x : R) (s : ↥p.primeCompl),
    ∃ (a : R),
      Eq.{u_8 + 1} (α := 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ₚ)
            a :
          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ₚ))
⊢ ∃ (a : R),
    Eq.{u_8 + 1} (α := 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ₚ)
          a :
        HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) x :
        HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ))

Tactic:
obtain ⟨x, s, 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ₚ
x : R
s : ↥p.primeCompl
refine_2 :
  ∀ (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)),
    ∃ (a : R),
      Eq.{u_8 + 1} (α := 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ₚ)
            a :
          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ₚ))
⊢ ∃ (a : R),
    Eq.{u_8 + 1} (α := 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ₚ)
          a :
        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ₚ))

Tactic:
obtain ⟨s', hs⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p s)⁻¹

Premises used: Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, Inv.inv, Subtype.val, DFunLike.coe
-- 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)
refine_2 :
  ∃ (a : R),
    Eq.{u_8 + 1} (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) ((algebraMap R Rₚ : (a : R) → Rₚ) a) :
        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ₚ))
⊢ ∃ (a : R),
    Eq.{u_8 + 1} (α := 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ₚ)
          a :
        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ₚ))

Tactic:
simp only [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _),
      Ideal.Quotient.algebraMap_eq, RingHom.comp_apply]

Premises used: Ideal.Quotient.algebraMap_eq, HasQuotient.Quotient, IsScalarTower.algebraMap_eq, RingHom.comp_apply
-- 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)
h :
  Eq.{u_8 + 1} (α := 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 * s')) :
      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ₚ))
⊢ ∃ (a : R),
    Eq.{u_8 + 1} (α := HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) ((algebraMap R Rₚ : (a : R) → Rₚ) a) :
        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ₚ))

Tactic:
use x * s'
-- 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)
h :
  Membership.mem (γ := Ideal Rₚ) (maximalIdeal Rₚ : Ideal Rₚ)
    (HSub.hSub (α := Rₚ) ((algebraMap R Rₚ : (a : R) → Rₚ) (x * s') : Rₚ) (mk' Rₚ x s))
⊢ Eq.{u_8 + 1} (α := 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 * s')) :
      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ₚ))

Tactic:
rw [← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]

Premises used: map_sub, sub_eq_zero, 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)
rw : (↑s : R) ∉ p
⊢ ((algebraMap R Rₚ : (a : R) → Rₚ) (↑s : R) : Rₚ) ∉ maximalIdeal Rₚ

Tactic:
rw [← Ideal.mem_under, IsLocalization.AtPrime.under_maximalIdeal Rₚ p]

Premises used: Ideal.mem_under, IsLocalization.AtPrime.isLocalRing, 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)
⊢ (↑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)
⊢ (↑s : R) ∉ p

Tactic:
exact s.prop

Premises used: Subtype.prop
-- 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)
⊢ ((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