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ₚ_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β :
  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:
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β :
  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, ?_, ?_⟩
-- 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ₚ_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β :
  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 : Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α : R ⧸ p) (0 : R ⧸ p)
⊢ α * β - 1 ∈ p

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
          map_mul, hβ, mul_inv_cancel₀, sub_self]

Premises used: map_sub, mul_inv_cancel₀, sub_self, Ideal.Quotient.eq_zero_iff_mem, map_mul, map_one
-- 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ₚ_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β :
  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 : ¬Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α : R ⧸ p) (0 : R ⧸ p)
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : α ∉ p
⊢ Ne (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α : R ⧸ p) (0 : R ⧸ p)

Tactic:
rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]

Premises used: Ne, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ_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β :
  Eq (α := R ⧸ p) ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) β : R ⧸ p)
    (((Ideal.Quotient.mk p : (a : R) → R ⧸ p) α)⁻¹ : R ⧸ p)
refine_2 refine_2₁ : α * β = α * β
⊢ α * β = 1 + (α * β - 1)

Tactic:
rw [add_sub_cancel]

Premises used: add_sub_cancel
-- 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ₚ_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₁ :
  Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))
    (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) (mk' Sₚ x s))
⊢ Eq.{u_9 + 1} (α :=
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    (((algebraMap S
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
            RingHom.{u_6, u_9} S
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))) :
          (a : S) → Sₚ ⧸ pSₚ)
        (β • x) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    ((Ideal.Quotient.mk (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)) : (a : Sₚ) → Sₚ ⧸ pSₚ)
        (mk' Sₚ x s) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))

Tactic:
rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ pSₚ), Ideal.Quotient.algebraMap_eq,
      RingHom.comp_apply, ← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]

Premises used: map_sub, sub_eq_zero, Ideal.Quotient.algebraMap_eq, Ideal.Quotient.eq_zero_iff_mem, RingHom.comp_apply
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ_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₁ :
  ∃ (x_1 : ↥(Ideal.map (F := R →+* S) (algebraMap R S) p) × ↥(algebraMapSubmonoid S p.primeCompl)),
    HMul.hMul (β := Sₚ) (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) (mk' Sₚ x s))
        ((algebraMap S Sₚ : (a : S) → Sₚ) (↑x_1.2 : S) : Sₚ) =
      (algebraMap S Sₚ : (a : S) → Sₚ) (↑x_1.1 : S)
⊢ Membership.mem (γ := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))
    (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) (mk' Sₚ x s))

Tactic:
rw [h, IsLocalization.mem_map_algebraMap_iff
      (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]

Premises used: Ideal.primeCompl, Algebra.algebraMapSubmonoid, IsLocalization.mem_map_algebraMap_iff
-- 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ₚ_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₁ : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (γ • x)
h₂ :
  HMul.hMul (β := Sₚ) (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) (mk' Sₚ x s))
      ((algebraMap S Sₚ : (a : S) → Sₚ)
          (↑(Subtype.mk (p := fun (x : S) ↦
                    Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) x) (γ • x) ⋯,
                  s).2 :
            S) :
        Sₚ) =
    (algebraMap S Sₚ : (a : S) → Sₚ)
      (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) x)
                (γ • x) ⋯,
              s).1 :
        S)
⊢ ∃ (x_1 : ↥(Ideal.map (F := R →+* S) (algebraMap R S) p) × ↥(algebraMapSubmonoid S p.primeCompl)),
    HMul.hMul (β := Sₚ) (HSub.hSub (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) (β • x) : Sₚ) (mk' Sₚ x s))
        ((algebraMap S Sₚ : (a : S) → Sₚ) (↑x_1.2 : S) : Sₚ) =
      (algebraMap S Sₚ : (a : S) → Sₚ) (↑x_1.1 : S)

Tactic:
refine ⟨⟨⟨γ • x, ?_⟩, s⟩, ?_⟩
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ_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₁ :
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) γ : S) x)
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (γ • x)

Tactic:
rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- 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ₚ_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₁ :
  Membership.mem.{u_6, u_6} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
    ((algebraMap R S : (a : R) → S) γ : S)
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) γ : S) x)

Tactic:
apply Ideal.mul_mem_right

Premises used: Ideal.mul_mem_right
-- 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ₚ_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 + γ
⊢ Membership.mem.{u_6, u_6} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
    ((algebraMap R S : (a : R) → S) γ : S)

Tactic:
Ideal.mem_map_of_mem _ hγ

Premises used: Ideal.mem_map_of_mem, Set.Mem
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
p_1 : Ideal R_1
inst_4 : p_1.IsPrime
Rₚ_1 : Type u_4
inst_5 : CommSemiring Rₚ_1
inst_6 : Algebra R_1 Rₚ_1
inst_7 : IsLocalization.AtPrime Rₚ_1 p_1
inst_8 : IsLocalRing Rₚ_1
Sₚ_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 + γ
⊢ Membership.mem.{u_6, u_6} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
    ((algebraMap R S : (a : R) → S) γ : S)

Tactic:
exact Ideal.mem_map_of_mem _ hγ

Premises used: Ideal.mem_map_of_mem