awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
n : ℕ
⊢ Eq (α := AlgHom.{u_7, u_7, u_8} R R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
    (AlgHom.comp
      (AlgHom.comp
        (AlgHom.comp (Quotient.liftₐ (p ^ n) (ofId R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) ⋯)
          (Quotient.liftₐ (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
            (liftAlgHom (R := R) (M := p.primeCompl) (f := Quotient.mkₐ R (p ^ n)) ⋯) ⋯))
        (Quotient.mkₐ R (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)))
      (algHom R R Rₚ))
    (AlgHom.comp
      (AlgHom.comp (AlgHom.id R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
        (Quotient.mkₐ R (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)))
      (algHom R R Rₚ))

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
n : ℕ
⊢ Eq (α := Rₚ →ₐ[R] Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
    (AlgHom.comp
      (AlgHom.comp (Quotient.liftₐ (p ^ n) (ofId R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) ⋯)
        (Quotient.liftₐ (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
          (liftAlgHom (R := R) (M := p.primeCompl) (f := Quotient.mkₐ R (p ^ n)) ⋯) ⋯))
      (Quotient.mkₐ R (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)))
    (AlgHom.comp (AlgHom.id R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n))
      (Quotient.mkₐ R (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)))

Tactic:
exact IsLocalization.algHom_ext (W := p.primeCompl) (A := R) (by ext)

Premises used: IsLocalization.algHom_ext, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
n : ℕ
refine_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)) ⋯) ⋯)
        (Quotient.liftₐ (p ^ n) (ofId R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) ⋯))
      (Quotient.mkₐ R (p ^ n)))
    (AlgHom.comp (AlgHom.id R (R ⧸ p ^ n)) (Quotient.mkₐ R (p ^ 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))

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

Premises used: AlgHom.cancel_right, Ideal.Quotient.mkₐ_surjective
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ : Type u_5
inst_9 : CommSemiring Sₚ
inst_10 : Algebra S_1 Sₚ
inst_11 : IsLocalization (algebraMapSubmonoid S_1 p_1.primeCompl) Sₚ
inst_12 : Algebra Rₚ_1 Sₚ
P : Ideal S_1
S : Type u_6
R : Type u_7
inst_13 : CommRing R
p : Ideal R
inst_14 : p.IsMaximal
Rₚ : Type u_8
inst_15 : CommRing Rₚ
inst_16 : Algebra R Rₚ
inst_17 : IsLocalization.AtPrime Rₚ p
inst_18 : IsLocalRing Rₚ
n : ℕ
⊢ 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)) ⋯) ⋯)
        (Quotient.liftₐ (p ^ n) (ofId R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) ⋯))
      (Quotient.mkₐ R (p ^ n)))
    (AlgHom.comp (AlgHom.id R (R ⧸ p ^ n)) (Quotient.mkₐ R (p ^ n)))

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Rₚ : Type u_8
inst_2 : CommRing Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
n : ℕ
x : R
⊢ Eq.{u_8 + 1} (α := Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
    (((equivQuotMaximalIdealPow p Rₚ n :
            AlgEquiv.{u_7, u_7, u_8} R (R ⧸ p ^ n) (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)) :
          (a : R ⧸ p ^ n) → Rₚ ⧸ maximalIdeal Rₚ ^ n)
        ((Ideal.Quotient.mk (p ^ n) : (a : R) → R ⧸ p ^ n) x) :
      Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ ^ n)
        ((algebraMap R Rₚ : (a : R) → Rₚ) x) :
      Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R : Type u_7
inst : CommRing R
p : Ideal R
inst_1 : p.IsMaximal
Rₚ : Type u_8
inst_2 : CommRing Rₚ
inst_3 : Algebra R Rₚ
inst_4 : IsLocalization.AtPrime Rₚ p
inst_5 : IsLocalRing Rₚ
n : ℕ
x : R
s : ↥p.primeCompl
⊢ HMul.hMul (α := R ⧸ p ^ n) (β := R ⧸ p ^ n)
      (((AlgEquiv.symm (equivQuotMaximalIdealPow p Rₚ n) :
              AlgEquiv.{u_7, u_8, u_7} R (Rₚ ⧸ HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n) (R ⧸ p ^ n)) :
            (a : Rₚ ⧸ maximalIdeal Rₚ ^ n) → R ⧸ p ^ n)
          ((Ideal.Quotient.mk (HPow.hPow (α := Ideal Rₚ) (maximalIdeal Rₚ) n) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ ^ n)
            (mk' Rₚ x s)) :
        R ⧸ p ^ n)
      ((Ideal.Quotient.mk (p ^ n) : (a : R) → R ⧸ p ^ n) (↑s : R) : R ⧸ p ^ n) =
    (Ideal.Quotient.mk (p ^ n) : (a : R) → R ⧸ p ^ n) x

Tactic:
simp [equivQuotMaximalIdealPow, lift_mk', IsUnit.liftRight_apply, mul_assoc]

Premises used: IsUnit.liftRight_apply, mul_assoc, IsLocalization.lift_mk', IsLocalization.AtPrime.equivQuotMaximalIdealPow
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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ₚ
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)))
⊢ 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)

Tactic:
rw [IsScalarTower.algebraMap_eq R S Sₚ, ← Ideal.map_map, eq_comm]

Premises used: eq_comm, Ideal.map_map, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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ₚ
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)
⊢ 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:
apply Ideal.le_comap_map.antisymm

Premises used: LE.le.antisymm, Ideal.le_comap_map
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
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)
⊢ ∃ α ∉ 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
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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)
⊢ ∃ (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

Premises used: map_mul, Ideal.primeCompl, Algebra.algebraMapSubmonoid, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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)
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)
⊢ ∃ α ∉ p, Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)

Tactic:
obtain ⟨c, hc⟩ := hy
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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)
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)
⊢ ∃ α ∉ p, Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)

Tactic:
obtain ⟨α, hα, e⟩ := (c * s).prop

Premises used: HMul.hMul, Subtype.prop
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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)

Tactic:
⟨α, hα, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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)
refine : Membership.mem (γ := Ideal 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)

Tactic:
refine ⟨α, hα, ?_⟩
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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)
rw : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) ((↑c : S) * (↑(y, s).1 : S))
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (α • x)

Tactic:
rw [Algebra.smul_def, e, Submonoid.coe_mul, mul_assoc, mul_comm _ x, hc]

Premises used: mul_assoc, mul_comm, Algebra.smul_def, Submonoid.coe_mul
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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) ((↑c : S) * (↑(y, s).1 : S))

Tactic:
Ideal.mul_mem_left _ _ y.prop

Premises used: Subtype.prop, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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) ((↑c : S) * (↑(y, s).1 : S))

Tactic:
exact Ideal.mul_mem_left _ _ y.prop

Premises used: Subtype.prop, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
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
⊢ 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
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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)
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 + γ
⊢ ∃ (β : R), ∃ γ ∈ p, β * α = 1 + γ

Tactic:
obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹

Premises used: Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, Inv.inv, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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 + γ

Tactic:
⟨β, β * α - 1, ?_, ?_⟩

Premises used: HMul.hMul, HSub.hSub, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
refine_2 : β * α = 1 + (β * α - 1)
⊢ ∃ (β : R), ∃ γ ∈ p, β * α = 1 + γ

Tactic:
refine ⟨β, β * α - 1, ?_, ?_⟩