awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
h :
  u • b.2 • a.1 = (↑u : R) • (↑b.2 : R) • a.1 ∧
    (↑u : R) * ((↑b.2 : R) * (↑a.2 : R)) = (↑u : R) * ((↑b.2 : R) * (↑a.2 : R))
⊢ (u * a.2) • b.1 = ((↑u : R) * (↑b.2 : R)) • a.1 ∧ (↑(u * a.2) : R) * (↑b.2 : R) = (↑u : R) * (↑b.2 : R) * (↑a.2 : R)

Tactic:
rw [mul_smul, ← hu, mul_smul, Submonoid.coe_mul, mul_assoc, mul_assoc, mul_comm (a.2 : R)]

Premises used: mul_assoc, mul_comm, Subtype.val, Prod.snd, SemigroupAction.mul_smul, Submonoid.coe_mul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ u • b.2 • a.1 = (↑u : R) • (↑b.2 : R) • a.1 ∧
    (↑u : R) * ((↑b.2 : R) * (↑a.2 : R)) = (↑u : R) * ((↑b.2 : R) * (↑a.2 : R))

Tactic:
simp [Submonoid.smul_def]

Premises used: Submonoid.smul_def
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : Prod.{v, u} M ↥S
m : M
s : ↥S
rw rw₁ : (m, s).2 • (m, s).1 = (m, s).2 • (m, s).1
⊢ HSMul.hSMul.{u, v, v} (α := ↥S) 1 ((m, s).2 • (m, s).1) = HSMul.hSMul.{u, v, v} (α := ↥S) 1 ((m, s).2 • (m, s).1)

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 x_2 : Prod.{v, u} M ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
h_1 : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
h_2 : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
h : (u1 * u2 * s2) • (m3, s3).2 • (m1, s1).1 = (u1 * u2 * s2) • (m1, s1).2 • (m3, s3).1
⊢ r S M (m1, s1) (m3, s3)

Tactic:
use u1 * u2 * s2
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 x_2 : Prod.{v, u} M ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
h : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
h_1 : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
⊢ Eq.{v + 1} (α := M) ((fun (x : M) ↦ (u2 * s3) • x) (u1 • (m1, s1).2 • (m2, s2).1))
    ((fun (x : M) ↦ (u2 * s3) • x) (u1 • (m2, s2).2 • (m1, s1).1))

Tactic:
have hu1' := congr_arg ((u2 * s3) • ·) hu1.symm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 x_2 : Prod.{v, u} M ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
h : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
h_1 : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
hu1' :
  Eq.{v + 1} (α := M) ((fun (x : M) ↦ (u2 * s3) • x) (u1 • (m1, s1).2 • (m2, s2).1))
    ((fun (x : M) ↦ (u2 * s3) • x) (u1 • (m2, s2).2 • (m1, s1).1))
⊢ Eq.{v + 1} (α := M) ((fun (x : M) ↦ (u1 * s1) • x) (u2 • (m2, s2).2 • (m3, s3).1))
    ((fun (x : M) ↦ (u1 * s1) • x) (u2 • (m3, s3).2 • (m2, s2).1))

Tactic:
have hu2' := congr_arg ((u1 * s1) • ·) hu2.symm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 x_2 : Prod.{v, u} M ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
h_1 : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
h_2 : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
hu1' :
  Eq.{v + 1} (α := M) ((fun (x : M) ↦ (u2 * s3) • x) (u1 • (m1, s1).2 • (m2, s2).1))
    ((fun (x : M) ↦ (u2 * s3) • x) (u1 • (m2, s2).2 • (m1, s1).1))
hu2' :
  Eq.{v + 1} (α := M) ((fun (x : M) ↦ (u1 * s1) • x) (u2 • (m2, s2).2 • (m3, s3).1))
    ((fun (x : M) ↦ (u1 * s1) • x) (u2 • (m3, s3).2 • (m2, s2).1))
h :
  ∀ (hu1' : (s1 * (s3 * (u1 * u2))) • m2 = (s2 * (s3 * (u1 * u2))) • m1)
    (hu2' : (s1 * (s2 * (u1 * u2))) • m3 = (s1 * (s3 * (u1 * u2))) • m2),
    (s2 * (s3 * (u1 * u2))) • m1 = (s1 * (s2 * (u1 * u2))) • m3
⊢ (u1 * u2 * s2) • (m3, s3).2 • (m1, s1).1 = (u1 * u2 * s2) • (m1, s1).2 • (m3, s3).1

Tactic:
simp only [← mul_smul, mul_comm, mul_left_comm] at hu1' hu2' ⊢

Premises used: mul_left_comm, mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 x_2 : Prod.{v, u} M ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
h_1 : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
h_2 : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
hu1' : (s1 * (s3 * (u1 * u2))) • m2 = (s2 * (s3 * (u1 * u2))) • m1
hu2' : (s1 * (s2 * (u1 * u2))) • m3 = (s1 * (s3 * (u1 * u2))) • m2
h : (s2 * (s3 * (u1 * u2))) • m1 = (s1 * (s3 * (u1 * u2))) • m2
h₁ h₂ : (s2 * (s3 * (u1 * u2))) • m1 = (s2 * (s3 * (u1 * u2))) • m1
⊢ (s2 * (s3 * (u1 * u2))) • m1 = (s1 * (s2 * (u1 * u2))) • m3

Tactic:
rw [hu2', hu1']
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_2
inst : CommSemiring R
S : Submonoid R
⊢ Localization (M := R) S = LocalizedModule S R

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_2
inst : CommSemiring R
S : Submonoid R
⊢ Localization (M := R) S = LocalizedModule S R

Tactic:
with_reducible rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
m m' : M
s s' : ↥S
rw : (∃ (u : ↥S) (v : R), u • m' = v • m ∧ (↑u : R) * (↑s' : R) = v * (↑s : R)) ↔ ∃ (u : ↥S), u • s' • m = u • s • m'
⊢ Eq (α := LocalizedModule S M) (mk m s) (mk m' s') ↔ ∃ (u : ↥S), u • s' • m = u • s • m'

Tactic:
rw [mk, mk, OreLocalization.oreDiv_eq_iff]

Premises used: OreLocalization.oreDiv_eq_iff, LocalizedModule.mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
m m' : M
s s' : ↥S
⊢ (∃ (u : ↥S) (v : R), u • m' = v • m ∧ (↑u : R) * (↑s' : R) = v * (↑s : R)) ↔ ∃ (u : ↥S), u • s' • m = u • s • m'

Tactic:
congr($(oreEqv_eq_r S M) ⟨m, s⟩ ⟨m', s'⟩)

Premises used: congrArg, id, Prod.mk, LocalizedModule.oreEqv_eq_r, iff_of_eq
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
m m' : M
s s' : ↥S
⊢ (∃ (u : ↥S) (v : R), u • m' = v • m ∧ (↑u : R) * (↑s' : R) = v * (↑s : R)) ↔ ∃ (u : ↥S), u • s' • m = u • s • m'

Tactic:
exact congr($(oreEqv_eq_r S M) ⟨m, s⟩ ⟨m', s'⟩)
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
β : LocalizedModule S M → Prop
h : ∀ (m : M) (s : ↥S), β (mk m s)
x : LocalizedModule S M
m : M
s : ↥S
⊢ β (Quot.mk (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) (m, s))

Tactic:
h m s

Premises used: Quotient.mk', OreLocalization.oreDiv
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
β : LocalizedModule S M → Prop
h : ∀ (m : M) (s : ↥S), β (mk m s)
x : LocalizedModule S M
m : M
s : ↥S
⊢ β (Quot.mk (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) (m, s))

Tactic:
exact h m s
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
β : LocalizedModule S M → LocalizedModule S M → Prop
h : ∀ (m m' : M) (s s' : ↥S), β (mk m s) (mk m' s')
x : LocalizedModule S M
m : M
s : ↥S
y : LocalizedModule S M
m' : M
s' : ↥S
⊢ β (Quot.mk (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) (m, s))
    (Quot.mk (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) (m', s'))

Tactic:
h m m' s s'

Premises used: Quotient.mk', OreLocalization.oreDiv
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
β : LocalizedModule S M → LocalizedModule S M → Prop
h : ∀ (m m' : M) (s s' : ↥S), β (mk m s) (mk m' s')
x : LocalizedModule S M
m : M
s : ↥S
y : LocalizedModule S M
m' : M
s' : ↥S
⊢ β (Quot.mk (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) (m, s))
    (Quot.mk (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) (m', s'))

Tactic:
exact h m m' s s'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
α : Type u_2
x : LocalizedModule S M
f : Prod.{v, u} M ↥S → α
wd : ∀ (p p' : Prod.{v, u} M ↥S), p ≈ p' → f p = f p'
⊢ ∀ (a b : Prod.{v, u} M ↥S), a ≈ b → f a = f b

Tactic:
simpa +instances only [r.setoid, ← oreEqv_eq_r S M] using wd

Premises used: LocalizedModule.r.setoid, LocalizedModule.oreEqv_eq_r
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_2
f : Prod.{v, u} M ↥S → α
wd : ∀ (p p' : Prod.{v, u} M ↥S), p ≈ p' → f p = f p'
m : M
s : ↥S
⊢ ⟦(m, s)⟧.liftOn f wd = f (m, s)

Tactic:
Quotient.liftOn_mk f wd ⟨m, s⟩

Premises used: Prod.mk, Quotient.liftOn_mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_2
f : Prod.{v, u} M ↥S → α
wd : ∀ (p p' : Prod.{v, u} M ↥S), p ≈ p' → f p = f p'
m : M
s : ↥S
⊢ liftOn (mk m s) f wd = f (m, s)

Tactic:
convert! Quotient.liftOn_mk f wd ⟨m, s⟩

Premises used: Prod.mk, Quotient.liftOn_mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
α : Type u_2
x y : LocalizedModule S M
f : Prod.{v, u} M ↥S → Prod.{v, u} M ↥S → α
wd : ∀ (p q p' q' : Prod.{v, u} M ↥S), p ≈ p' → q ≈ q' → f p q = f p' q'
⊢ ∀ (a₁ b₁ a₂ b₂ : Prod.{v, u} M ↥S), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂

Tactic:
simpa +instances only [r.setoid, ← oreEqv_eq_r S M] using wd

Premises used: LocalizedModule.r.setoid, LocalizedModule.oreEqv_eq_r
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_2
f : Prod.{v, u} M ↥S → Prod.{v, u} M ↥S → α
wd : ∀ (p q p' q' : Prod.{v, u} M ↥S), p ≈ p' → q ≈ q' → f p q = f p' q'
m m' : M
s s' : ↥S
⊢ ⟦(m, s)⟧.liftOn₂ ⟦(m', s')⟧ f wd = f (m, s) (m', s')

Tactic:
Quotient.liftOn₂_mk f wd _ _

Premises used: Quotient.liftOn₂_mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_2
f : Prod.{v, u} M ↥S → Prod.{v, u} M ↥S → α
wd : ∀ (p q p' q' : Prod.{v, u} M ↥S), p ≈ p' → q ≈ q' → f p q = f p' q'
m m' : M
s s' : ↥S
⊢ liftOn₂ (mk m s) (mk m' s') f wd = f (m, s) (m', s')

Tactic:
convert! Quotient.liftOn₂_mk f wd _ _

Premises used: Quotient.liftOn₂_mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : 0 ∈ S
⊢ Subsingleton (LocalizedModule S M)

Tactic:
⟨fun a b ↦ ?_⟩

Premises used: Subsingleton.intro
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : 0 ∈ S
refine : ∀ (a b : LocalizedModule S M), a = b
⊢ Subsingleton (LocalizedModule S M)

Tactic:
refine ⟨fun a b ↦ ?_⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : 0 ∈ S
a b : LocalizedModule S M
h₁ : ∀ (m m' : M) (s s' : ↥S), Eq (α := LocalizedModule S M) (mk m s) (mk m' s')
⊢ a = b

Tactic:
induction a, b using LocalizedModule.induction_on₂
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : 0 ∈ S
m m' : M
s s' : ↥S
⊢ Subtype.mk (p := fun (x : R) ↦ x ∈ S) 0 h • s' • m = Subtype.mk (p := fun (x : R) ↦ x ∈ S) 0 h • s • m'

Tactic:
simp only [Submonoid.mk_smul, zero_smul]

Premises used: Submonoid.mk_smul, zero_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : 0 ∈ S
m m' : M
s s' : ↥S
⊢ Eq (α := LocalizedModule S M) (mk m s) (mk m' s')

Tactic:
exact mk_eq.mpr ⟨⟨0, h⟩, by simp only [Submonoid.mk_smul, zero_smul]⟩

Premises used: Iff.mpr, LocalizedModule.mk_eq, Subtype.mk, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
⊢ Eq (α := LocalizedModule S M) (mk 0 s) 0

Tactic:
simp [mk]

Premises used: LocalizedModule.mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
m1 m2 : M
s1 s2 : ↥S
⊢ HAdd.hAdd (α := LocalizedModule S M) (mk m1 s1) (mk m2 s2) = mk (s2 • m1 + s1 • m2) (s1 * s2)

Tactic:
simp [mk, OreLocalization.oreDiv_add_oreDiv, mul_comm s1 s2, Submonoid.smul_def]

Premises used: OreLocalization.oreDiv_add_oreDiv, LocalizedModule.mk, Submonoid.smul_def, mul_comm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
m : M
s : ↥S
⊢ Eq (α := LocalizedModule S M) (mk (-m) s) (-mk m s)

Tactic:
simp [mk]

Premises used: LocalizedModule.mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S_1 : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : u₁ • (b₁, t₁).2 • (a₁, s₁).1 = u₁ • (a₁, s₁).2 • (b₁, t₁).1
u₂ : ↥S
e₂ : u₂ • (b₂, t₂).2 • (a₂, s₂).1 = u₂ • (a₂, s₂).2 • (b₂, t₂).1
simp : Eq (α := LocalizedModule S A) (mk (a₁ * a₂) (s₁ * s₂)) (mk (b₁ * b₂) (t₁ * t₂))
⊢ Eq (α := LocalizedModule S A)
    ((fun (x₁ x₂ : Prod.{u_2, u} A ↥S) ↦ (mk (x₁.1 * x₂.1) (x₂.2 * x₁.2) : LocalizedModule S A)) (a₁, s₁) (a₂, s₂))
    ((fun (x₁ x₂ : Prod.{u_2, u} A ↥S) ↦ (mk (x₁.1 * x₂.1) (x₂.2 * x₁.2) : LocalizedModule S A)) (b₁, t₁) (b₂, t₂))

Tactic:
simp only [mul_comm s₂ s₁, mul_comm t₂ t₁]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S_1 : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : u₁ • (b₁, t₁).2 • (a₁, s₁).1 = u₁ • (a₁, s₁).2 • (b₁, t₁).1
u₂ : ↥S
e₂ : u₂ • (b₂, t₂).2 • (a₂, s₂).1 = u₂ • (a₂, s₂).2 • (b₂, t₂).1
rw : ∃ (u : ↥S), u • (t₁ * t₂) • (a₁ * a₂) = u • (s₁ * s₂) • (b₁ * b₂)
⊢ Eq (α := LocalizedModule S A) (mk (a₁ * a₂) (s₁ * s₂)) (mk (b₁ * b₂) (t₁ * t₂))

Tactic:
rw [mk_eq]

Premises used: LocalizedModule.mk_eq
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S_1 : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : u₁ • (b₁, t₁).2 • (a₁, s₁).1 = u₁ • (a₁, s₁).2 • (b₁, t₁).1
u₂ : ↥S
e₂ : u₂ • (b₂, t₂).2 • (a₂, s₂).1 = u₂ • (a₂, s₂).2 • (b₂, t₂).1
h : (u₁ * u₂) • (t₁ * t₂) • (a₁ * a₂) = (u₁ * u₂) • (s₁ * s₂) • (b₁ * b₂)
⊢ ∃ (u : ↥S), u • (t₁ * t₂) • (a₁ * a₂) = u • (s₁ * s₂) • (b₁ * b₂)

Tactic:
use u₁ * u₂
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S_1 : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : u₁ • (b₁, t₁).2 • (a₁, s₁).1 = u₁ • (a₁, s₁).2 • (b₁, t₁).1
u₂ : ↥S
e₂ : u₂ • (b₂, t₂).2 • (a₂, s₂).1 = u₂ • (a₂, s₂).2 • (b₂, t₂).1
h :
  ((↑u₁ : R) * (↑u₂ : R)) • ((↑t₁ : R) * (↑t₂ : R)) • (a₁ * a₂) =
    ((↑u₁ : R) * (↑u₂ : R)) • ((↑s₁ : R) * (↑s₂ : R)) • (b₁ * b₂)
⊢ (u₁ * u₂) • (t₁ * t₂) • (a₁ * a₂) = (u₁ * u₂) • (s₁ * s₂) • (b₁ * b₂)

Tactic:
dsimp [Submonoid.smul_def] at *

Premises used: Submonoid.smul_def
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S_1 : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : (↑u₁ : R) • (↑t₁ : R) • a₁ = (↑u₁ : R) • (↑s₁ : R) • b₁
u₂ : ↥S
e₂ : (↑u₂ : R) • (↑t₂ : R) • a₂ = (↑u₂ : R) • (↑s₂ : R) • b₂
⊢ ((↑u₁ : R) * (↑u₂ : R)) • ((↑t₁ : R) * (↑t₂ : R)) • (a₁ * a₂) =
    ((↑u₁ : R) * (↑u₂ : R)) • ((↑s₁ : R) * (↑s₂ : R)) • (b₁ * b₂)

Tactic:
simp only [mul_smul_mul_comm, e₁, e₂]

Premises used: mul_smul_mul_comm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S_1 : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
a : LocalizedModule S A
a₁ : A
s₁ : ↥S
b : LocalizedModule S A
a₂ : A
s₂ : ↥S
c : LocalizedModule S A
a₃ : A
s₃ : ↥S
apply :
  ∃ (u : ↥S),
    u •
        (((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).2 * (a₁, s₁).2) •
          (((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).1 * (a₃, s₃).1) =
      u •
        ((a₃, s₃).2 * ((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).2) •
          ((a₁, s₁).1 * ((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).1)
⊢ HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁))
        (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₂, s₂)) *
      Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃) =
    Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁) *
      HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₂, s₂))
        (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃))

Tactic:
apply mk_eq.mpr _

Premises used: Iff.mpr, LocalizedModule.mk_eq
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S_1 : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
a : LocalizedModule S A
a₁ : A
s₁ : ↥S
b : LocalizedModule S A
a₂ : A
s₂ : ↥S
c : LocalizedModule S A
a₃ : A
s₃ : ↥S
h :
  HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1
      ((((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).2 * (a₁, s₁).2) •
        (((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).1 * (a₃, s₃).1)) =
    HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1
      (((a₃, s₃).2 * ((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).2) •
        ((a₁, s₁).1 * ((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).1))
⊢ ∃ (u : ↥S),
    u •
        (((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).2 * (a₁, s₁).2) •
          (((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).1 * (a₃, s₃).1) =
      u •
        ((a₃, s₃).2 * ((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).2) •
          ((a₁, s₁).1 * ((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).1)

Tactic:
use 1
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S_1 : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
a : LocalizedModule S A
a₁ : A
s₁ : ↥S
b : LocalizedModule S A
a₂ : A
s₂ : ↥S
c : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1
      ((((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).2 * (a₁, s₁).2) •
        (((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).1 * (a₃, s₃).1)) =
    HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1
      (((a₃, s₃).2 * ((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).2) •
        ((a₁, s₁).1 * ((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).1))

Tactic:
simp only [one_mul, smul_smul, ← mul_assoc, mul_right_comm]

Premises used: mul_assoc, smul_smul, mul_right_comm, one_mul