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ₚ
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)
⊢ p ^ n ≤
    RingHom.ker (F := RingHom.{u_7, u_8} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
      (algebraMap R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
have refine_1₄ : p ^ n ≤ p ^ n
Tactic: rw [← Quotient.mk_comp_algebraMap, ← RingHom.comap_ker, mk_ker, ← under_def,
      under_maximalIdeal_pow p]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
n : ℕ
⊢ AlgHom.{u_7, u_8, u_7} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n) (R ⧸ p ^ n)
have 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)) sorry : (a : Rₚ) → R ⧸ p ^ n) x : R ⧸ p ^ n)
    (0 : 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 ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
n : ℕ
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)
have 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)) sorry : (a : Rₚ) → R ⧸ p ^ n) (mk' Rₚ a b) :
      R ⧸ p ^ n)
    (0 : R ⧸ p ^ n)
Tactic: obtain ⟨a, b, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
n : ℕ
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)
have hx₁ : a ∈ p ^ n
Tactic: rw [IsLocalization.mk'_mem_iff, ← Ideal.mem_under, under_maximalIdeal_pow p] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
n : ℕ
⊢ 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))
have 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)) sorry)
      (Quotient.liftₐ (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
        (liftAlgHom (R := R) (M := p.primeCompl) (f := Quotient.mkₐ R (p ^ n)) sorry) sorry))
    (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)))
Tactic: rw [← AlgHom.cancel_right (Ideal.Quotient.mkₐ_surjective _ _)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
n : ℕ
⊢ 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))
have refine_4 : Eq (α := R →ₐ[R] R ⧸ p ^ n)
  (AlgHom.comp
    (AlgHom.comp
      (Quotient.liftₐ (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
        (liftAlgHom (R := R) (M := p.primeCompl) (f := Quotient.mkₐ R (p ^ n)) sorry) sorry)
      (Quotient.liftₐ (p ^ n) (ofId R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) sorry))
    (Quotient.mkₐ R (p ^ n)))
  (AlgHom.comp (AlgHom.id R (R ⧸ p ^ n)) (Quotient.mkₐ R (p ^ n)))
Tactic: rw [← AlgHom.cancel_right (Ideal.Quotient.mkₐ_surjective _ _)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
⊢ Eq (α := Ideal S) (under.{u_6, u_9} S (B := Sₚ) (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p))
    (Ideal.map (F := R →+* S) (algebraMap R S) p)
have rw : Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
  (under.{u_6, u_9} S (B := Sₚ)
    (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
Tactic: rw [IsScalarTower.algebraMap_eq R S Sₚ, ← Ideal.map_map, eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
⊢ Eq (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
    (under.{u_6, u_9} S (B := Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
have apply : LE.le (α := Ideal S)
  (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
    (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
  (Ideal.map (F := R →+* S) (algebraMap R S) p)
Tactic: apply Ideal.le_comap_map.antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
⊢ ∃ α ∉ p, Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
have have : ∀ (y : ↥(Ideal.map (F := R →+* S) (algebraMap R S) p)) (s : ↥(algebraMapSubmonoid S p.primeCompl))
  (hy :
    HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ)
        ((algebraMap S Sₚ : (a : S) → Sₚ) (↑(y, s).2 : S) : Sₚ) =
      (algebraMap S Sₚ : (a : S) → Sₚ) (↑(y, s).1 : S)),
  ∃ α ∉ p, Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
Tactic: have ⟨⟨y, s⟩, hy⟩ := (IsLocalization.mem_map_algebraMap_iff
      (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ).mp hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
y : ↥(Ideal.map (F := R →+* S) (algebraMap R S) p)
s : ↥(algebraMapSubmonoid S p.primeCompl)
hy :
  HMul.hMul (α := Sₚ) (β := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) x : Sₚ)
      ((algebraMap S Sₚ : (a : S) → Sₚ) (↑(y, s).2 : S) : Sₚ) =
    (algebraMap S Sₚ : (a : S) → Sₚ) (↑(y, s).1 : S)
⊢ ∃ α ∉ p, Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
have hy₁ : ∃ (c : ↥(algebraMapSubmonoid S p.primeCompl)), (↑c : S) * (x * (↑(y, s).2 : S)) = (↑c : S) * (↑(y, s).1 : S)
Tactic: rw [← map_mul,
      IsLocalization.eq_iff_exists (Algebra.algebraMapSubmonoid S p.primeCompl)] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
y : ↥(Ideal.map (F := R →+* S) (algebraMap R S) p)
s : ↥(algebraMapSubmonoid S p.primeCompl)
hy : ∃ (c : ↥(algebraMapSubmonoid S p.primeCompl)), (↑c : S) * (x * (↑(y, s).2 : S)) = (↑c : S) * (↑(y, s).1 : S)
⊢ ∃ α ∉ p, Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
have obtain : ∀ (c : ↥(algebraMapSubmonoid S p.primeCompl)) (hc : (↑c : S) * (x * (↑(y, s).2 : S)) = (↑c : S) * (↑(y, s).1 : S)),
  ∃ α ∉ p, Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
Tactic: obtain ⟨c, hc⟩ := hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
y : ↥(Ideal.map (F := R →+* S) (algebraMap R S) p)
s c : ↥(algebraMapSubmonoid S p.primeCompl)
hc : (↑c : S) * (x * (↑(y, s).2 : S)) = (↑c : S) * (↑(y, s).1 : S)
⊢ ∃ α ∉ p, Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
have obtain : ∀ (α : R) (hα : α ∈ (↑p.primeCompl : Set R)) (e : (algebraMap R S : (a : R) → S) α = (↑(c * s) : S)),
  ∃ α ∉ p, Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
Tactic: obtain ⟨α, hα, e⟩ := (c * s).prop
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
y : ↥(Ideal.map (F := R →+* S) (algebraMap R S) p)
s c : ↥(algebraMapSubmonoid S p.primeCompl)
hc : (↑c : S) * (x * (↑(y, s).2 : S)) = (↑c : S) * (↑(y, s).1 : S)
α : R
hα : α ∈ (↑p.primeCompl : Set R)
e : (algebraMap R S : (a : R) → S) α = (↑(c * s) : S)
⊢ ∃ α ∉ p, Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
have refine : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
Tactic: refine ⟨α, hα, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
y : ↥(Ideal.map (F := R →+* S) (algebraMap R S) p)
s c : ↥(algebraMapSubmonoid S p.primeCompl)
hc : (↑c : S) * (x * (↑(y, s).2 : S)) = (↑c : S) * (↑(y, s).1 : S)
α : R
hα : α ∈ (↑p.primeCompl : Set R)
e : (algebraMap R S : (a : R) → S) α = (↑(c * s) : S)
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
have rw : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) ((↑c : S) * (↑(y, s).1 : S))
Tactic: rw [Algebra.smul_def, e, Submonoid.coe_mul, mul_assoc, mul_comm _ x, hc]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) p) x
have obtain : ∀ (α : R) (hα : α ∉ p) (hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)),
  Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) p) x
Tactic: obtain ⟨α, hα, hαx⟩ : ∃ α ∉ p, α • x ∈ pS := by
    have ⟨⟨y, s⟩, hy⟩ := (IsLocalization.mem_map_algebraMap_iff
      (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ).mp hx
    rw [← map_mul,
      IsLocalization.eq_iff_exists (Algebra.algebraMapSubmonoid S p.primeCompl)] at hy
    obtain ⟨c, hc⟩ := hy
    obtain ⟨α, hα, e⟩ := (c * s).prop
    refine ⟨α, hα, ?_⟩
    rw [Algebra.smul_def, e, Submonoid.coe_mul, mul_assoc, mul_comm _ x, hc]
    exact Ideal.mul_mem_left _ _ y.prop
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
⊢ ∃ (β : R), ∃ γ ∈ p, β * α = 1 + γ
have obtain : ∀ (β : R)
  (hβ :
    Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) β : R ⧸ p)
      (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α)⁻¹ : R ⧸ p)),
  ∃ (β : R), ∃ γ ∈ p, β * α = 1 + γ
Tactic: obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β : R
hβ :
  Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) β : R ⧸ p)
    (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α)⁻¹ : R ⧸ p)
⊢ ∃ (β : R), ∃ γ ∈ p, β * α = 1 + γ
have refine_1 : β * α - 1 ∈ p
Tactic: refine ⟨β, β * α - 1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β : R
hβ :
  Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) β : R ⧸ p)
    (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α)⁻¹ : R ⧸ p)
refine_1 : β * α - 1 ∈ p
⊢ ∃ (β : R), ∃ γ ∈ p, β * α = 1 + γ
have refine_2 : β * α = 1 + (β * α - 1)
Tactic: refine ⟨β, β * α - 1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β : R
hβ :
  Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) β : R ⧸ p)
    (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α)⁻¹ : R ⧸ p)
⊢ β * α - 1 ∈ p
have refine_1 : Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α : R ⧸ p) (0 : R ⧸ p)
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
        map_mul, hβ, inv_mul_cancel₀, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
S : Type u_6
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Sₚ : Type u_9
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : CommRing Sₚ
inst_5 : Algebra S Sₚ
inst_6 : Algebra R Sₚ
inst_7 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_8 : IsScalarTower R S Sₚ
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (comap (F := S →+* Sₚ) (algebraMap S Sₚ)
      (Ideal.map (R := S) (F := S →+* Sₚ) (algebraMap S Sₚ) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    x
α : R
hα : α ∉ p
hαx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)
β : R
hβ :
  Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) β : R ⧸ p)
    (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α)⁻¹ : R ⧸ p)
⊢ Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α : R ⧸ p) (0 : R ⧸ p)
have refine_1 : ¬Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α : R ⧸ p) (0 : R ⧸ p)
Tactic: rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]