awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
n : ℕ
simp_rw :
  HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n =
    HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ^ n
⊢ mk' S (x ^ n) (y ^ n) = mk' S x y ^ n

Tactic:
simp_rw [IsLocalization.mk'_eq_iff_eq_mul, SubmonoidClass.coe_pow, map_pow, ← mul_pow]

Premises used: map_pow, IsLocalization.mk'_eq_iff_eq_mul, SubmonoidClass.coe_pow, mul_pow
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
n : ℕ
⊢ HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n =
    HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ^ n

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
⊢ Surjective.{u_1 + 1, u_2 + 1} (β := S) fun (x : R × ↥M) ↦
    match (motive := R × ↥M → S) x with
    | (r, m) => mk' S r m

Tactic:
fun z ↦
  let ⟨r, hr⟩ := IsLocalization.surj _ z
  ⟨r, (eq_mk'_iff_mul_eq.2 hr).symm⟩

Premises used: Iff.mpr, IsLocalization.surj, Exists, IsLocalization.mk', IsLocalization.mk'_surjective.match_1, Exists.intro, IsLocalization.eq_mk'_iff_mul_eq, Eq.symm, _private.0.IsLocalization.mk'_surjective.match_2, Eq, Function.Surjective
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
⊢ ∃ (x : R) (y : ↥M), mk' S x y = z

Tactic:
let ⟨⟨r, m⟩, hz⟩ := mk'_surjective M z; ⟨r, m, hz⟩

Premises used: IsLocalization.mk'_surjective, Exists, _private.0.IsLocalization.exists_mk'_eq.match_1, IsLocalization.mk', Exists.intro, Eq
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
h : 0 ∈ M
⊢ Eq.{u_2 + 1} (α := S) 0 1

Tactic:
simpa using IsLocalization.map_units S ⟨0, h⟩

Premises used: Subtype.mk, IsLocalization.map_units, OfNat.ofNat
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ mk' S x₁ y₁ = mk' S x₂ y₂ ↔
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑y₂ : R) * x₁) : S)
      ((algebraMap R S : (a : R) → S) ((↑y₁ : R) * x₂) : S)

Tactic:
(toLocalizationMap M S).mk'_eq_iff_eq

Premises used: Submonoid.LocalizationMap.mk'_eq_iff_eq, IsLocalization.mk', IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ mk' S x₁ y₁ = mk' S x₂ y₂ ↔
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x₁ * (↑y₂ : R)) : S)
      ((algebraMap R S : (a : R) → S) (x₂ * (↑y₁ : R)) : S)

Tactic:
(toLocalizationMap M S).mk'_eq_iff_eq'

Premises used: Submonoid.LocalizationMap.mk'_eq_iff_eq', IsLocalization.mk', IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
a₁ b₁ : R
a₂ b₂ : ↥M
⊢ mk' S a₁ a₂ = mk' S b₁ b₂ ↔ ∃ (c : ↥M), (↑c : R) * ((↑b₂ : R) * a₁) = (↑c : R) * ((↑a₂ : R) * b₁)

Tactic:
(toLocalizationMap M S).eq

Premises used: Set.Mem, IsLocalization.mk', IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.eq
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
s : ↥M
⊢ mk' S x s = 0 ↔ ∃ (m : ↥M), (↑m : R) * x = 0

Tactic:
(toLocalizationMap M S).mk'_eq_zero_iff x s

Premises used: Set.Mem, IsLocalization.mk', IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.mk'_eq_zero_iff
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
s : ↥M
⊢ mk' S 0 s = 0

Tactic:
(toLocalizationMap M S).mk'_zero s

Premises used: Submonoid.LocalizationMap.mk'_zero, IsLocalization.mk', IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
y : ↥M
hxy : mk' S 0 y ≠ 0
⊢ False

Tactic:
hxy (IsLocalization.mk'_zero _)

Premises used: IsLocalization.mk'_zero
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
y : ↥M
hxy : mk' S 0 y ≠ 0
⊢ False

Tactic:
exact hxy (IsLocalization.mk'_zero _)

Premises used: IsLocalization.mk'_zero
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
hM : ∀ m ∈ M, IsRegular m
r : R
m : ↥M
⊢ ∀ (n : ↥M) (x y : R), (↑n : R) * x = (↑n : R) * y ↔ x = y

Tactic:
have (n : M) (x y : R) : n * x = n * y ↔ x = y := (hM _ n.2).1.eq_iff
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
hM : ∀ m ∈ M, IsRegular m
r : R
m : ↥M
this : ∀ (n : ↥M) (x y : R), (↑n : R) * x = (↑n : R) * y ↔ x = y
simp :
  (∀ (a a_1 : R) (b : a_1 ∈ M) (a_2 a_3 : R) (b : a_3 ∈ M), a_3 * (r * a) = a_1 * (r * a_2) → a_3 * a = a_1 * a_2) ↔
    ∀ ⦃a₁ a₂ : R⦄, r * a₁ = r * a₂ → a₁ = a₂
⊢ IsRegular (mk' S r m) ↔ IsRegular r

Tactic:
simp +contextual only [← isLeftRegular_iff_isRegular, IsLeftRegular, Function.Injective,
    (mk'_surjective M).forall, ← mk'_mul, Prod.forall, Subtype.forall, IsLocalization.eq,
    Submonoid.coe_mul, this, exists_const, mul_assoc]

Premises used: IsLocalization.mk'_surjective, Function.Surjective.forall, mul_assoc, isLeftRegular_iff_isRegular, Subtype.forall, IsLeftRegular, exists_const, Prod.forall, Function.Injective, IsLocalization.eq, Submonoid.coe_mul, IsLocalization.mk'_mul
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
hM : ∀ m ∈ M, IsRegular m
r : R
m : ↥M
this : ∀ (n : ↥M) (x y : R), (↑n : R) * x = (↑n : R) * y ↔ x = y
simp_rw :
  (∀ (a a_1 : R) (b : a_1 ∈ M) (a_2 a_3 : R) (b : a_3 ∈ M), r * (a_3 * a) = r * (a_1 * a_2) → a_3 * a = a_1 * a_2) ↔
    ∀ ⦃a₁ a₂ : R⦄, r * a₁ = r * a₂ → a₁ = a₂
⊢ (∀ (a a_1 : R) (b : a_1 ∈ M) (a_2 a_3 : R) (b : a_3 ∈ M), a_3 * (r * a) = a_1 * (r * a_2) → a_3 * a = a_1 * a_2) ↔
    ∀ ⦃a₁ a₂ : R⦄, r * a₁ = r * a₂ → a₁ = a₂

Tactic:
simp_rw [← mul_left_comm r]

Premises used: mul_left_comm
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
hM : ∀ m ∈ M, IsRegular m
r : R
m : ↥M
this : ∀ (n : ↥M) (x y : R), (↑n : R) * x = (↑n : R) * y ↔ x = y
h : ∀ (a a_1 : R) (b : a_1 ∈ M) (a_2 a_3 : R) (b : a_3 ∈ M), r * (a_3 * a) = r * (a_1 * a_2) → a_3 * a = a_1 * a_2
a b : R
⊢ r * a = r * b → a = b

Tactic:
simpa using h a 1 M.one_mem b 1 M.one_mem

Premises used: Submonoid.one_mem, OfNat.ofNat
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
hM : ∀ m ∈ M, IsRegular m
r : R
m : ↥M
this : ∀ (n : ↥M) (x y : R), (↑n : R) * x = (↑n : R) * y ↔ x = y
⊢ (∀ (a a_1 : R) (b : a_1 ∈ M) (a_2 a_3 : R) (b : a_3 ∈ M), r * (a_3 * a) = r * (a_1 * a_2) → a_3 * a = a_1 * a_2) ↔
    ∀ ⦃a₁ a₂ : R⦄, r * a₁ = r * a₂ → a₁ = a₂

Tactic:
exact ⟨fun h a b ↦ by simpa using h a 1 M.one_mem b 1 M.one_mem, fun h ha s hs b t ht ↦ @h _ _⟩
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : NoZeroDivisors R
⊢ NoZeroDivisors S

Tactic:
(toLocalizationMap M S).noZeroDivisors

Premises used: Submonoid.LocalizationMap.noZeroDivisors, IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
hx : x ≠ 0
h : (sec M x).1 = 0
rw : mk' S (sec M x).1 (sec M x).2 = 0
rw₁ : mk' S 0 (sec M x).2 = 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := S) 0 0
⊢ x = 0

Tactic:
rw [← mk'_sec (M := M) S x, h, mk'_zero]

Premises used: IsLocalization.mk'_sec, IsLocalization.mk'_zero
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
inst_5 : Algebra R P
inst_6 : IsLocalization M P
x y : R
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
    Eq.{u_3 + 1} (α := P) ((algebraMap R P : (a : R) → P) x : P) ((algebraMap R P : (a : R) → P) y : P)

Tactic:
(toLocalizationMap M S).eq_iff_eq (toLocalizationMap M P)

Premises used: IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.eq_iff_eq
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
inst_5 : Algebra R P
inst_6 : IsLocalization M P
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ mk' S x₁ y₁ = mk' S x₂ y₂ ↔ mk' P x₁ y₁ = mk' P x₂ y₂

Tactic:
(toLocalizationMap M S).mk'_eq_iff_mk'_eq (toLocalizationMap M P)

Premises used: Submonoid.LocalizationMap.mk'_eq_iff_mk'_eq, IsLocalization.mk', IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
a₁ b₁ : R
a₂ b₂ : ↥M
H : (↑a₂ : R) * b₁ = (↑b₂ : R) * a₁
⊢ mk' S a₁ a₂ = mk' S b₁ b₂

Tactic:
(toLocalizationMap M S).mk'_eq_of_eq H

Premises used: Submonoid.LocalizationMap.mk'_eq_of_eq, IsLocalization.mk', IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
a₁ b₁ : R
a₂ b₂ : ↥M
H : b₁ * (↑a₂ : R) = a₁ * (↑b₂ : R)
⊢ mk' S a₁ a₂ = mk' S b₁ b₂

Tactic:
(toLocalizationMap M S).mk'_eq_of_eq' H

Premises used: IsLocalization.mk', Submonoid.LocalizationMap.mk'_eq_of_eq', IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
a : R
b c : ↥M
⊢ mk' S (a * (↑c : R)) (b * c) = mk' S a b

Tactic:
(toLocalizationMap M S).mk'_cancel _ _ _

Premises used: Set.Mem, Submonoid.LocalizationMap.mk'_cancel, IsLocalization.mk', IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
hx : x ∈ M
⊢ mk' S x (Subtype.mk (p := fun (x : R) ↦ x ∈ M) x hx) = 1

Tactic:
(toLocalizationMap M S).mk'_self _ hx

Premises used: Set.Mem, Submonoid.LocalizationMap.mk'_self, IsLocalization.mk', IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : ↥M
⊢ mk' S (↑x : R) x = 1

Tactic:
(toLocalizationMap M S).mk'_self' _

Premises used: IsLocalization.mk', IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.mk'_self'
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : ↥M
⊢ mk' S (↑x : R) x = 1

Tactic:
mk'_self' _

Premises used: IsLocalization.mk'_self'
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : R
z : ↥M
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (mk' S y z) = mk' S (x * y) z

Tactic:
(toLocalizationMap M S).mul_mk'_eq_mk'_of_mul _ _ _

Premises used: Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul, IsLocalization.mk', IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
⊢ mk' S x y = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (mk' S 1 y)

Tactic:
((toLocalizationMap M S).mul_mk'_one_eq_mk' _ _).symm

Premises used: IsLocalization.mk', Submonoid.LocalizationMap.mul_mk'_one_eq_mk', IsLocalization.toLocalizationMap, Eq.symm
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
⊢ mk' S ((↑y : R) * x) y = (algebraMap R S : (a : R) → S) x

Tactic:
(toLocalizationMap M S).mk'_mul_cancel_left _ _

Premises used: Submonoid.LocalizationMap.mk'_mul_cancel_left, IsLocalization.mk', IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
⊢ mk' S (x * (↑y : R)) y = (algebraMap R S : (a : R) → S) x

Tactic:
(toLocalizationMap M S).mk'_mul_cancel_right _ _

Premises used: IsLocalization.mk', Submonoid.LocalizationMap.mk'_mul_cancel_right, IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : ↥M
rw : mk' S ((↑y : R) * (↑x : R)) (y * x) = 1
⊢ mk' S (↑x : R) y * mk' S (↑y : R) x = 1

Tactic:
rw [← mk'_mul, mul_comm]

Premises used: mul_comm, IsLocalization.mk'_mul
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : ↥M
⊢ mk' S ((↑y : R) * (↑x : R)) (y * x) = 1

Tactic:
mk'_self _ _

Premises used: IsLocalization.mk'_self
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : ↥M
⊢ mk' S ((↑y : R) * (↑x : R)) (y * x) = 1

Tactic:
exact mk'_self _ _

Premises used: IsLocalization.mk'_self
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
h : x ∈ M
⊢ mk' S x y * mk' S (↑y : R) (Subtype.mk (p := fun (x : R) ↦ x ∈ M) x h) = 1

Tactic:
mk'_mul_mk'_eq_one ⟨x, h⟩ _

Premises used: Subtype.mk, IsLocalization.mk'_mul_mk'_eq_one
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : R
m : ↥M
nth_rw : x • mk' S y m = mk' S (x * y) (1 * m)
⊢ x • mk' S y m = mk' S (x * y) m

Tactic:
nth_rw 2 [← one_mul m]

Premises used: one_mul
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : R
m : ↥M
rw : x • mk' S y m = mk' (M := M) S x 1 * mk' S y m
rw₁ : x • mk' S y m = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (mk' S y m)
rw₂ rw₃ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (mk' S y m) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (mk' S y m)
⊢ x • mk' S y m = mk' S (x * y) (1 * m)

Tactic:
rw [mk'_mul, mk'_one, Algebra.smul_def]

Premises used: IsLocalization.mk'_one, Algebra.smul_def, IsLocalization.mk'_mul
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
m : ↥M
rw : mk' S (x * 1) m = mk' S x m
rw₁ rw₂ : mk' S x m = mk' S x m
⊢ x • mk' S 1 m = mk' S x m

Tactic:
rw [smul_mk', mul_one]

Premises used: IsLocalization.smul_mk', mul_one
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
m : ↥M
r : R
rw : mk' S ((↑m : R) * r) m = (algebraMap R S : (a : R) → S) r
rw₁ rw₂ : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap R S : (a : R) → S) r : S)
⊢ (↑m : R) • mk' S r m = (algebraMap R S : (a : R) → S) r

Tactic:
rw [smul_mk', mk'_mul_cancel_left]

Premises used: IsLocalization.mk'_mul_cancel_left, IsLocalization.smul_mk'
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
s : ↥M
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) (mk' S 1 s) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
s : ↥M
⊢ HMul.hMul (β := S) (mk' S 1 s) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
j : S →+* P
y : ↥M
⊢ IsUnit.{u_3} (M := P) ((j.comp (algebraMap R S) : (a : R) → P) (↑y : R) : P)

Tactic:
(toLocalizationMap M S).isUnit_comp j.toMonoidHom _

Premises used: Submonoid.LocalizationMap.isUnit_comp, IsLocalization.toLocalizationMap, RingHom.toMonoidHom
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
x y : R
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
⊢ Eq.{u_3 + 1} (α := P) ((g : (a : R) → P) x : P) ((g : (a : R) → P) y : P)

Tactic:
Submonoid.LocalizationMap.eq_of_eq (toLocalizationMap M S) (g := g.toMonoidHom) hg h

Premises used: IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.eq_of_eq
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
rw :
  HAdd.hAdd (α := S) ((algebraMap R S : (a : R) → S) ((↑y₁ : R) * (↑(y₁ * y₂) : R) * x₂) : S)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((↑(y₁ * y₂) : R) * x₁) : S)
        ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S)) =
    HMul.hMul (β := S)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (x₁ * (↑y₂ : R) + x₂ * (↑y₁ : R)) : S)
        ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S))
      ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S)
⊢ HMul.hMul (β := S) (mk' S x₁ y₁ + mk' S x₂ y₂) ((algebraMap R S : (a : R) → S) (↑(y₁ * y₂) : R) : S) =
    (algebraMap R S : (a : R) → S) (x₁ * (↑y₂ : R) + x₂ * (↑y₁ : R))

Tactic:
rw [mul_comm (_ + _), mul_add, mul_mk'_eq_mk'_of_mul, mk'_add_eq_iff_add_mul_eq_mul,
          mul_comm (_ * _), ← mul_assoc, add_comm, ← map_mul, mul_mk'_eq_mk'_of_mul,
          mk'_add_eq_iff_add_mul_eq_mul]

Premises used: HMul.hMul, mul_assoc, IsLocalization.mk'_add_eq_iff_add_mul_eq_mul, add_comm, map_mul, HAdd.hAdd, mul_comm, mul_add, IsLocalization.mul_mk'_eq_mk'_of_mul
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
simp :
  HMul.hMul (β := S)
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S)
          (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S)
            ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S)))
        ((algebraMap R S : (a : R) → S) x₂ : S) +
      HMul.hMul (β := S)
        (HMul.hMul (β := S)
          (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S)
            ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S))
          ((algebraMap R S : (a : R) → S) x₁ : S))
        ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S) =
    HMul.hMul (β := S)
      (HMul.hMul (β := S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x₁ : S)
            ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S) +
          HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x₂ : S)
            ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S))
        ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S))
      ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S)
⊢ HAdd.hAdd (α := S) ((algebraMap R S : (a : R) → S) ((↑y₁ : R) * (↑(y₁ * y₂) : R) * x₂) : S)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((↑(y₁ * y₂) : R) * x₁) : S)
        ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S)) =
    HMul.hMul (β := S)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (x₁ * (↑y₂ : R) + x₂ * (↑y₁ : R)) : S)
        ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S))
      ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S)

Tactic:
simp only [map_add, Submonoid.coe_mul, map_mul]

Premises used: map_add, map_mul, Submonoid.coe_mul
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ HMul.hMul (β := S)
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S)
          (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S)
            ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S)))
        ((algebraMap R S : (a : R) → S) x₂ : S) +
      HMul.hMul (β := S)
        (HMul.hMul (β := S)
          (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S)
            ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S))
          ((algebraMap R S : (a : R) → S) x₁ : S))
        ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S) =
    HMul.hMul (β := S)
      (HMul.hMul (β := S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x₁ : S)
            ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S) +
          HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x₂ : S)
            ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S))
        ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S))
      ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S)

Tactic:
ring