awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
refine_1 :
  p =
    RingHom.ker (F := RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
      (@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ₚ)))
⊢ p =
    RingHom.ker (F := RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
      (algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) :
        RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
have refine_1₁ : p =
  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ₚ))))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
refine_1 :
  p =
    RingHom.ker (F := RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
      (@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ₚ))))
⊢ p =
    RingHom.ker (F := RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
      (algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) :
        RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
have refine_1₂ : p =
  under R
    (RingHom.ker (F := Rₚ →+* HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      (algebraMap 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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
refine_1 :
  p =
    RingHom.ker (F := RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
      (@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ₚ))))
⊢ p =
    RingHom.ker (F := RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
      (algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) :
        RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
have refine_1₃ : p =
  under R
    (RingHom.ker (F := Rₚ →+* HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      (Ideal.Quotient.mk (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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
refine_1 :
  p =
    RingHom.ker (F := RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
      (@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ₚ)))
⊢ p =
    RingHom.ker (F := RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
      (algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) :
        RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
have refine_1₄ : p = under 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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
refine_1 :
  p =
    RingHom.ker (F := RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
      (@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ₚ)
⊢ p =
    RingHom.ker (F := RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
      (algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) :
        RingHom.{u_7, u_8} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)))
have refine_1₅ : p = p
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]
-- 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 : HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal 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
have 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ₚ))
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x
-- 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ₚ
⊢ ∃ (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ₚ))
have 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ₚ))
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x
Cleared hypotheses: x
-- 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
⊢ ∃ (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ₚ))
have 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ₚ))
Tactic: obtain ⟨s', hs⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p s)⁻¹
-- 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)
⊢ ∃ (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ₚ))
have 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ₚ))
Tactic: simp only [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _),
      Ideal.Quotient.algebraMap_eq, RingHom.comp_apply]
-- 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)
⊢ ∃ (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ₚ))
have 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ₚ))
Tactic: use x * s'
-- 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)
⊢ 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ₚ))
have 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))
Tactic: rw [← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
-- 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)
⊢ ((algebraMap R Rₚ : (a : R) → Rₚ) (↑s : R) : Rₚ) ∉ maximalIdeal Rₚ
have rw : (↑s : R) ∉ p
Tactic: rw [← Ideal.mem_under, IsLocalization.AtPrime.under_maximalIdeal Rₚ p]