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ₚ_1 : Type u_5
inst_9 : CommSemiring Sₚ_1
inst_10 : Algebra S_1 Sₚ_1
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ_1
inst_12 : Algebra Rₚ_1 Sₚ_1
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ₚ
Sₚ : Type u_9
inst_19 : CommRing S
inst_20 : Algebra R S
inst_21 : CommRing Sₚ
inst_22 : Algebra S Sₚ
inst_23 : Algebra R Sₚ
inst_24 : Algebra Rₚ Sₚ
inst_25 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_26 : IsScalarTower R S Sₚ
inst_27 : IsScalarTower R Rₚ Sₚ
h :
  Eq.{u_9 + 1} (α := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))
    (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p))
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S : (a : R) → S) α = (↑s : S)
β γ : R
hγ : γ ∈ p
hβ : α * β = 1 + γ
h₁ :
  HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) (mk' Sₚ x s)) =
    (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
h₂ :
  HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) -
      HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) (mk' Sₚ x s) =
    (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
h₃ :
  HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) -
      mk' Sₚ ((↑s : S) * x) s =
    (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
h₄ :
  HSub.hSub (β := Sₚ)
      (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ))
      ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ) =
    (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
⊢ HMul.hMul (β := Sₚ) (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) (mk' Sₚ x s))
      ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) =
    (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
have h₅ : HSub.hSub (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) ((↑s : S) * β • x) : Sₚ)
    ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ) =
  (algebraMap S Sₚ : (a : S) → Sₚ) (γ • x)
Tactic: rw [mul_comm, mul_sub, IsLocalization.mul_mk'_eq_mk'_of_mul,
      IsLocalization.mk'_mul_cancel_left, ← map_mul, ← e, ← Algebra.smul_def, smul_smul,
      hβ, ← map_sub, add_smul, one_smul, add_comm x, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
I p : Ideal R
inst_3 : p.IsPrime
inst_4 : IsLocalization.AtPrime S p
hle : ¬I ≤ p
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤
have hle₁ : ¬(↑I : Set R) ⊆ (↑p.primeCompl : Set R)ᶜ
Tactic: apply IsLocalization.map_eq_top_of_not_subset p.primeCompl
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
Rₚ : Type u_3
inst : CommRing Rₚ
inst_1 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_2 : CommRing Sₚ
inst_3 : Algebra Rₚ Sₚ
Q : Ideal Sₚ
inst_4 : Q.IsMaximal
inst_5 : Algebra.IsIntegral Rₚ Sₚ
⊢ Membership.mem (γ := Set (Ideal Sₚ)) (primesOver (maximalIdeal Rₚ) Sₚ) Q
have refine : Q.LiesOver (maximalIdeal Rₚ)
Tactic: refine ⟨inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
Rₚ : Type u_3
inst : CommRing Rₚ
inst_1 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_2 : CommRing Sₚ
inst_3 : Algebra Rₚ Sₚ
Q : Ideal Sₚ
inst_4 : Q.IsMaximal
inst_5 : Algebra.IsIntegral Rₚ Sₚ
⊢ Q.LiesOver (maximalIdeal Rₚ)
have rw : IsMaximal (under Rₚ Q)
Tactic: rw [liesOver_iff, ← eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
T : Type u_5
inst_8 : CommRing T
inst_9 : Algebra R T
inst_10 : Algebra Rₚ T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : IsScalarTower R Rₚ T
Q : Ideal T
inst_14 : Q.LiesOver (maximalIdeal Rₚ)
⊢ Q.LiesOver p
have this : LiesOver (maximalIdeal Rₚ) p
Tactic: have : (maximalIdeal Rₚ).LiesOver p := liesOver_maximalIdeal Rₚ p _
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
T : Type u_5
inst_8 : CommRing T
inst_9 : Algebra R T
inst_10 : Algebra Rₚ T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : IsScalarTower R Rₚ T
Q : Ideal T
inst_14 : Q.LiesOver (maximalIdeal Rₚ)
⊢ LiesOver (comap (F := S →+* T) (algebraMap S T) Q) p
have this : Q.LiesOver p
Tactic: have : Q.LiesOver p := by
    have : (maximalIdeal Rₚ).LiesOver p := liesOver_maximalIdeal Rₚ p _
    exact LiesOver.trans Q (IsLocalRing.maximalIdeal Rₚ) p
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : P.IsPrime
⊢ LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) (maximalIdeal Rₚ)
have rw : Eq (α := Ideal Rₚ) (under.{u_3, u_4} Rₚ (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
  (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) (under R P))
Tactic: rw [liesOver_iff, eq_comm, ← map_eq_maximalIdeal p, over_def P p]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
⊢ ∃ (a : S),
    (algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
          (a : S) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        a =
      x
have obtain : ∀ (x : Sₚ),
  ∃ (a : S),
    Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
            (a : S) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          a :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          x :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : Sₚ
⊢ ∃ (a : S),
    Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
            (a : S) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          a :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          x :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
have obtain : ∀ (x : S) (s : ↥(algebraMapSubmonoid S p.primeCompl)),
  ∃ (a : S),
    Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
            (a : S) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          a :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (mk' Sₚ x s) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq (algebraMapSubmonoid S p.primeCompl) x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
⊢ ∃ (a : S),
    Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
            (a : S) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          a :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (mk' Sₚ x s) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
have obtain : ∀ (s' : S)
  (hs :
    Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
      (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)),
  ∃ (a : S),
    Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
            (a : S) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          a :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (mk' Sₚ x s) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
Tactic: obtain ⟨s', hs⟩ := Ideal.Quotient.mk_surjective (I := P) (Ideal.Quotient.mk P s)⁻¹
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
⊢ ∃ (a : S),
    Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((algebraMap S (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
            (a : S) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          a :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (mk' Sₚ x s) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
have simp : ∃ (a : S),
  Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) : (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        ((algebraMap S Sₚ : (a : S) → Sₚ) a) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) : (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        (mk' Sₚ x s) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
Tactic: simp only [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ _), Quotient.algebraMap_eq, RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
⊢ ∃ (a : S),
    Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          ((algebraMap S Sₚ : (a : S) → Sₚ) a) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
      ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) :
            (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          (mk' Sₚ x s) :
        HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
have h : Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
  ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) : (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
      ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s')) :
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
  ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) : (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
      (mk' Sₚ x s) :
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
Tactic: use x * s'
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
⊢ Eq.{u_4 + 1} (α := HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) : (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s')) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
    ((Ideal.Quotient.mk (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) : (a : Sₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        (mk' Sₚ x s) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
have h : Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
  (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s))
Tactic: rw [← sub_eq_zero, ← map_sub, Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s))
have h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
Tactic: have h₀ : (P.map (algebraMap S Sₚ)).IsPrime := isPrime_map_of_liesOver S p Sₚ P
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s))
have h₁ : (↑s : S) ∉ P
Tactic: have h₁ : s.1 ∉ P := (Set.disjoint_left.mp <| disjoint_primeCompl_of_liesOver P p) s.prop
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
⊢ ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
have rwa : (↑s : S) ∉ comap (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
Tactic: rwa [← mem_comap, comap_map_eq_self_of_isMaximal _ h₀.ne_top]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s))
have h₂ : ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
Tactic: have h₂ : algebraMap S Sₚ s ∉ Ideal.map (algebraMap S Sₚ) P := by
    rwa [← mem_comap, comap_map_eq_self_of_isMaximal _ h₀.ne_top]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
h₂ : ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s))
have h : Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
  (HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
    (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s)))
Tactic: refine (h₀.mem_or_mem ?_).resolve_left h₂
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Sₚ : Type u_4
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_7 : P.IsMaximal
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
s' : S
hs :
  Eq (α := S ⧸ P) ((Ideal.Quotient.mk P : (a : S) → S ⧸ P) s' : S ⧸ P)
    (((Ideal.Quotient.mk P : (a : S) → S ⧸ P) (↑s : S))⁻¹ : S ⧸ P)
h₀ : IsPrime.{u_4} (α := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
h₁ : (↑s : S) ∉ P
h₂ : ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) ∉ Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
    (HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) (mk' Sₚ x s)))
have h : Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)
  (HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ)
      ((algebraMap S Sₚ : (a : S) → Sₚ) (x * s') : Sₚ) -
    HMul.hMul (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (↑s : S) : Sₚ) (mk' Sₚ x s))
Tactic: rw [mul_sub, mul_mk'_eq_mk'_of_mul, mk'_mul_cancel_left, ← map_mul, ← map_sub, ← mem_comap,
    comap_map_eq_self_of_isMaximal _ IsPrime.ne_top', ← Ideal.Quotient.eq, map_mul, map_mul, hs,
    mul_comm, inv_mul_cancel_right₀ (Quotient.eq_zero_iff_mem.not.mpr h₁)]