awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
mk :
  ∀ (a : LocalizedModule S A) (a₁ : A) (s₁ : ↥S) (b : LocalizedModule S A) (a₂ : A) (s₂ : ↥S) (c : LocalizedModule S A)
    (a₃ : A) (s₃ : ↥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₂)) *
        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₃))
rintro :
  ∀ (a : LocalizedModule S A) (a₁ : A) (s₁ : ↥S) (b : LocalizedModule S A) (a₂ : A) (s₂ : ↥S) (c : LocalizedModule S A)
    (a₃ : A) (s₃ : ↥S),
    ∃ (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)
h :
  ∀ (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))
⊢ ∀ (a b c : LocalizedModule S A), a * b * c = a * (b * c)

Tactic:
with_unfolding_all
      rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨a₃, s₃⟩
      apply mk_eq.mpr _
      use 1
      simp only [one_mul, smul_smul, ← mul_assoc, mul_right_comm]

Premises used: Iff.mpr, LocalizedModule.mk_eq, mul_assoc, smul_smul, mul_right_comm, one_mul
-- 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_1 : LocalizedModule S A
a : A
s : ↥S
⊢ HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 (s • ((1, 1).1 * (a, s).1)) =
    HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 (((a, s).2 * (1, 1).2) • a)

Tactic:
simp only [one_mul, mul_one, one_smul]

Premises used: one_smul, mul_one, one_mul
-- 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_1 : LocalizedModule S A
a : A
s : ↥S
⊢ HMul.hMul (α := LocalizedModule S A) 1 (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:
exact mk_eq.mpr ⟨1, by simp only [one_mul, mul_one, one_smul]⟩

Premises used: Iff.mpr, LocalizedModule.mk_eq, Exists.intro, OfNat.ofNat
-- 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_1 : LocalizedModule S A
a : A
s : ↥S
⊢ HMul.hMul (α := LocalizedModule S A) 1 (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:
with_unfolding_all exact mk_eq.mpr ⟨1, by simp only [one_mul, mul_one, one_smul]⟩

Premises used: Iff.mpr, LocalizedModule.mk_eq, Exists.intro, OfNat.ofNat
-- 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_1 : LocalizedModule S A
a : A
s : ↥S
⊢ HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 (s • ((a, s).1 * (1, 1).1)) =
    HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 (((1, 1).2 * (a, s).2) • a)

Tactic:
simp only [mul_one, one_smul, one_mul]

Premises used: one_smul, mul_one, one_mul
-- 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_1 : LocalizedModule S A
a : A
s : ↥S
⊢ HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a, s)) 1 =
    Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a, s)

Tactic:
exact mk_eq.mpr ⟨1, by simp only [mul_one, one_smul, one_mul]⟩

Premises used: Iff.mpr, LocalizedModule.mk_eq, Exists.intro, OfNat.ofNat
-- 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_1 : LocalizedModule S A
a : A
s : ↥S
⊢ HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a, s)) 1 =
    Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a, s)

Tactic:
with_unfolding_all exact mk_eq.mpr ⟨1, by simp only [mul_one, one_smul, one_mul]⟩

Premises used: Iff.mpr, LocalizedModule.mk_eq, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
⊢ Eq.{u + 1} (α := Monoid (OreLocalization S R)) OreLocalization.instMonoid instMonoid

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
⊢ Eq.{u + 1} (α := Monoid (OreLocalization S R)) OreLocalization.instMonoid instMonoid

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
a₁ a₂ : A
s₁ s₂ : ↥S
⊢ HMul.hMul (α := LocalizedModule S A) (mk a₁ s₁) (mk a₂ s₂) = mk (a₁ * a₂) (s₂ * s₁)

Tactic:
rfl

Premises used: LocalizedModule.liftOn₂, Quotient.mk', LocalizedModule.mul, OreLocalization.oreDiv, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
a₁ a₂ : A
s₁ s₂ : ↥S
rw : Eq (α := LocalizedModule S A) (mk (a₁ * a₂) (s₂ * s₁)) (mk (a₁ * a₂) (s₁ * s₂))
rw₁ rw₂ : Eq (α := LocalizedModule S A) (mk (a₁ * a₂) (s₂ * s₁)) (mk (a₁ * a₂) (s₂ * s₁))
⊢ HMul.hMul (α := LocalizedModule S A) (mk a₁ s₁) (mk a₂ s₂) = mk (a₁ * a₂) (s₁ * s₂)

Tactic:
rw [mk_mul_mk', mul_comm s₁ s₂]

Premises used: LocalizedModule.mk_mul_mk', 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_1 : LocalizedModule S A
a : A
s : ↥S
⊢ HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 (HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 ((0, 1).1 * (a, s).1)) =
    HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 (HSMul.hSMul (β := A) ((a, s).2 * (0, 1).2) 0)

Tactic:
simp only [zero_mul, smul_zero]

Premises used: MulZeroClass.zero_mul, smul_zero
-- 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_1 : LocalizedModule S A
a : A
s : ↥S
⊢ HMul.hMul (α := LocalizedModule S A) 0 (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a, s)) = 0

Tactic:
exact mk_eq.mpr ⟨1, by simp only [zero_mul, smul_zero]⟩

Premises used: Iff.mpr, LocalizedModule.mk_eq, Exists.intro, OfNat.ofNat
-- 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
mk :
  ∀ (a : LocalizedModule S A) (a : A) (s : ↥S),
    HMul.hMul (α := LocalizedModule S A) 0 (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a, s)) = 0
⊢ ∀ (a : LocalizedModule S A), 0 * a = 0

Tactic:
with_unfolding_all
      rintro ⟨a, s⟩
      exact mk_eq.mpr ⟨1, by simp only [zero_mul, smul_zero]⟩

Premises used: Iff.mpr, LocalizedModule.mk_eq, Exists.intro, OfNat.ofNat
-- 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_1 : LocalizedModule S A
a : A
s : ↥S
⊢ HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 (HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 ((a, s).1 * (0, 1).1)) =
    HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 (HSMul.hSMul (β := A) ((0, 1).2 * (a, s).2) 0)

Tactic:
simp only [mul_zero, smul_zero]

Premises used: smul_zero, MulZeroClass.mul_zero
-- 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_1 : LocalizedModule S A
a : A
s : ↥S
⊢ HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a, s)) 0 = 0

Tactic:
exact mk_eq.mpr ⟨1, by simp only [mul_zero, smul_zero]⟩

Premises used: Iff.mpr, LocalizedModule.mk_eq, Exists.intro, OfNat.ofNat
-- 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
mk :
  ∀ (a : LocalizedModule S A) (a : A) (s : ↥S),
    HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a, s)) 0 = 0
⊢ ∀ (a : LocalizedModule S A), a * 0 = 0

Tactic:
with_unfolding_all
      rintro ⟨a, s⟩
      exact mk_eq.mpr ⟨1, by simp only [mul_zero, smul_zero]⟩

Premises used: Iff.mpr, LocalizedModule.mk_eq, Exists.intro, OfNat.ofNat
-- 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
mk :
  a₁ /ₒ s₁ * HAdd.hAdd (α := OreLocalization S A) (a₂ /ₒ s₂) (a₃ /ₒ s₃) =
    HMul.hMul (α := OreLocalization S A) (a₁ /ₒ s₁) (a₂ /ₒ s₂) +
      HMul.hMul (α := OreLocalization S A) (a₁ /ₒ s₁) (a₃ /ₒ s₃)
⊢ Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁) *
      HAdd.hAdd (α := 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₃)) =
    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₂)) +
      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:
change a₁ /ₒ s₁ * (a₂ /ₒ s₂ + a₃ /ₒ s₃) = a₁ /ₒ s₁ * (a₂ /ₒ s₂) + a₁ /ₒ s₁ * (a₃ /ₒ s₃)

Premises used: HAdd.hAdd, OreLocalization.oreDiv
-- 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
mk :
  Eq (α := OreLocalization S A) (LocalizedModule.mk (a₁ * (s₃ • a₂ + s₂ • a₃)) (s₁ * (s₂ * s₃)))
    (LocalizedModule.mk ((s₁ * s₃) • (a₁ * a₂) + (s₁ * s₂) • (a₁ * a₃)) (s₁ * s₂ * (s₁ * s₃)))
⊢ a₁ /ₒ s₁ * HAdd.hAdd (α := OreLocalization S A) (a₂ /ₒ s₂) (a₃ /ₒ s₃) =
    HMul.hMul (α := OreLocalization S A) (a₁ /ₒ s₁) (a₂ /ₒ s₂) +
      HMul.hMul (α := OreLocalization S A) (a₁ /ₒ s₁) (a₃ /ₒ s₃)

Tactic:
rw [← mk, ← mk, ← mk, mk_mul_mk, mk_mul_mk, mk_add_mk, mk_mul_mk, mk_add_mk]

Premises used: LocalizedModule.mk_add_mk, LocalizedModule.mk_mul_mk, 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
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 • (s₁ * s₂ * (s₁ * s₃)) • (a₁ * (s₃ • a₂ + s₂ • a₃)) =
      u • (s₁ * (s₂ * s₃)) • ((s₁ * s₃) • (a₁ * a₂) + (s₁ * s₂) • (a₁ * a₃))
⊢ Eq (α := OreLocalization S A) (mk (a₁ * (s₃ • a₂ + s₂ • a₃)) (s₁ * (s₂ * s₃)))
    (mk ((s₁ * s₃) • (a₁ * a₂) + (s₁ * s₂) • (a₁ * a₃)) (s₁ * s₂ * (s₁ * 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 ((s₁ * s₂ * (s₁ * s₃)) • (a₁ * (s₃ • a₂ + s₂ • a₃))) =
    HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 ((s₁ * (s₂ * s₃)) • ((s₁ * s₃) • (a₁ * a₂) + (s₁ * s₂) • (a₁ * a₃)))
⊢ ∃ (u : ↥S),
    u • (s₁ * s₂ * (s₁ * s₃)) • (a₁ * (s₃ • a₂ + s₂ • a₃)) =
      u • (s₁ * (s₂ * s₃)) • ((s₁ * s₃) • (a₁ * a₂) + (s₁ * s₂) • (a₁ * a₃))

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 ((s₁ * s₂ * (s₁ * s₃)) • (a₁ * (s₃ • a₂ + s₂ • a₃))) =
    HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 ((s₁ * (s₂ * s₃)) • ((s₁ * s₃) • (a₁ * a₂) + (s₁ * s₂) • (a₁ * a₃)))

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

Premises used: mul_assoc, smul_smul, mul_right_comm, mul_smul_comm, mul_add, smul_add, one_mul
-- 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
mk :
  HAdd.hAdd (α := OreLocalization S A) (a₁ /ₒ s₁) (a₂ /ₒ s₂) * (a₃ /ₒ s₃) =
    HMul.hMul (α := OreLocalization S A) (a₁ /ₒ s₁) (a₃ /ₒ s₃) +
      HMul.hMul (α := OreLocalization S A) (a₂ /ₒ s₂) (a₃ /ₒ s₃)
⊢ HAdd.hAdd (α := 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₃) =
    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₃)) +
      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:
change (a₁ /ₒ s₁ + a₂ /ₒ s₂) * (a₃ /ₒ s₃) = a₁ /ₒ s₁ * (a₃ /ₒ s₃) + a₂ /ₒ s₂ * (a₃ /ₒ s₃)

Premises used: HAdd.hAdd, OreLocalization.oreDiv
-- 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
mk :
  Eq (α := OreLocalization S A) (LocalizedModule.mk ((s₂ • a₁ + s₁ • a₂) * a₃) (s₁ * s₂ * s₃))
    (LocalizedModule.mk ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃)) (s₁ * s₃ * (s₂ * s₃)))
⊢ HAdd.hAdd (α := OreLocalization S A) (a₁ /ₒ s₁) (a₂ /ₒ s₂) * (a₃ /ₒ s₃) =
    HMul.hMul (α := OreLocalization S A) (a₁ /ₒ s₁) (a₃ /ₒ s₃) +
      HMul.hMul (α := OreLocalization S A) (a₂ /ₒ s₂) (a₃ /ₒ s₃)

Tactic:
rw [← mk, ← mk, ← mk, mk_mul_mk, mk_mul_mk, mk_add_mk, mk_mul_mk, mk_add_mk]

Premises used: LocalizedModule.mk_add_mk, LocalizedModule.mk_mul_mk, 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
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 • (s₁ * s₃ * (s₂ * s₃)) • ((s₂ • a₁ + s₁ • a₂) * a₃) =
      u • (s₁ * s₂ * s₃) • ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃))
⊢ Eq (α := OreLocalization S A) (mk ((s₂ • a₁ + s₁ • a₂) * a₃) (s₁ * s₂ * s₃))
    (mk ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃)) (s₁ * s₃ * (s₂ * 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 ((s₁ * s₃ * (s₂ * s₃)) • ((s₂ • a₁ + s₁ • a₂) * a₃)) =
    HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 ((s₁ * s₂ * s₃) • ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃)))
⊢ ∃ (u : ↥S),
    u • (s₁ * s₃ * (s₂ * s₃)) • ((s₂ • a₁ + s₁ • a₂) * a₃) =
      u • (s₁ * s₂ * s₃) • ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃))

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 ((s₁ * s₃ * (s₂ * s₃)) • ((s₂ • a₁ + s₁ • a₂) * a₃)) =
    HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 ((s₁ * s₂ * s₃) • ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃)))

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

Premises used: add_mul, mul_assoc, smul_smul, smul_mul_assoc, mul_right_comm, smul_add, one_mul
-- 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 : CommSemiring 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
⊢ HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 (((a₁, s₁).2 * (a₂, s₂).2) • ((a₁, s₁).1 * (a₂, s₂).1)) =
    HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 (((a₂, s₂).2 * (a₁, s₁).2) • ((a₂, s₂).1 * (a₁, s₁).1))

Tactic:
simp only [one_smul, mul_comm]

Premises used: one_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 : CommSemiring 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
⊢ 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₂)) =
    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:
exact mk_eq.mpr ⟨1, by simp only [one_smul, mul_comm]⟩

Premises used: Iff.mpr, LocalizedModule.mk_eq, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_2
inst : CommRing R
S : Submonoid R
⊢ Eq.{u_2 + 1} (α := CommRing (OreLocalization S R)) OreLocalization.instCommRing instCommRing

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_2
inst : CommRing R
S : Submonoid R
⊢ Eq.{u_2 + 1} (α := CommRing (OreLocalization S R)) OreLocalization.instCommRing instCommRing

Tactic:
with_reducible_and_instances rfl