awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type ?u.80272
inst_2 : MulAction R X
T : Type u_2
inst_3 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : (↑sa : R) * r₁ = ra * (↑s₂ : R)
ha' : HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
c :
  liftExpand
      (fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      ⋯ (ra * r₂ /ₒ (sa * s₁)) =
    HMul.hMul (α := T)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₁ /ₒ s₁))
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂))
⊢ liftExpand
      (fun (r : R) (s : ↥S) ↦
        HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
      ⋯ (HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂)) =
    HMul.hMul (α := T)
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₁ /ₒ s₁))
      (liftExpand
        (fun (r : R) (s : ↥S) ↦
          HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T))
        ⋯ (r₂ /ₒ s₂))

Tactic:
rw [ha']
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r : R
s : ↥S
⊢ (universalMulHom f fS hf : (a : OreLocalization S R) → T) (r /ₒ s) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s)⁻¹ : T) : T) ((f : (a : R) → T) r : T)

Tactic:
rfl

Premises used: OreLocalization.liftExpand, rfl
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r : R
⊢ Eq.{u_2 + 1} (α := T)
    ((universalMulHom f fS hf : (a : OreLocalization S R) → T)
        ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) :
      T)
    ((f : (a : R) → T) r : T)

Tactic:
simp [numeratorHom_apply, universalMulHom_apply]

Premises used: OreLocalization.numeratorHom_apply, OreLocalization.universalMulHom_apply
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
φ : MonoidHom.{u_1, u_2} (OreLocalization S R) T
huniv :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
      ((f : (a : R) → T) r : T)
h :
  ∀ (x : OreLocalization S R),
    Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) x : T)
      ((universalMulHom f fS hf : (a : OreLocalization S R) → T) x : T)
⊢ φ = universalMulHom f fS hf

Tactic:
ext x
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
T : Type u_2
inst_2 : Monoid T
f : R →* T
fS : MonoidHom.{u_1, u_2} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_2 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
φ : MonoidHom.{u_1, u_2} (OreLocalization S R) T
huniv :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := T)
      ((φ : (a : OreLocalization S R) → T) ((numeratorHom : (a : R) → OreLocalization S R) r : OreLocalization S R) : T)
      ((f : (a : R) → T) r : T)
x : OreLocalization S R
h :
  ∀ (r : R) (s : ↥S),
    Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) (r /ₒ s) : T)
      ((universalMulHom f fS hf : (a : OreLocalization S R) → T) (r /ₒ s) : T)
⊢ Eq.{u_2 + 1} (α := T) ((φ : (a : OreLocalization S R) → T) x : T)
    ((universalMulHom f fS hf : (a : OreLocalization S R) → T) x : T)

Tactic:
cases x with | _ r s
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
c : R
r : X
t : M
s : ↥S
ht : t * (↑s : M) ∈ S
rw :
  Eq (α := OreLocalization S X) (oreNum (HSMul.hSMul (β := M) c 1) s • r /ₒ (oreDenom (HSMul.hSMul (β := M) c 1) s * 1))
    (oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht))
rw₁ :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s) =
    oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht)
rw₂ :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s) =
    oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      (oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) * 1)
rw₃ :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s) =
    HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1)
      (t • r /ₒ Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht)
rw₄ rw₅ :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s) =
    HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) c 1 /ₒ 1) (r /ₒ s)
⊢ Eq (α := OreLocalization S X) (oreNum (HSMul.hSMul (β := M) c 1) s • r /ₒ oreDenom (HSMul.hSMul (β := M) c 1) s)
    (oreNum (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht) • t • r /ₒ
      oreDenom (HSMul.hSMul (β := M) c 1) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) (t * (↑s : M)) ht))

Tactic:
rw [← mul_one (oreDenom (c • 1) s), ← oreDiv_smul_oreDiv, ← mul_one (oreDenom (c • 1) _),
      ← oreDiv_smul_oreDiv, ← OreLocalization.expand]

Premises used: OreLocalization.expand, OreLocalization.oreDiv_smul_oreDiv, HSMul.hSMul, mul_one, OfNat.ofNat, OreLocalization.oreDenom
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
r : R
x : X
s : ↥S
⊢ HSMul.hSMul (β := OreLocalization S X) r (x /ₒ s) =
    oreNum (HSMul.hSMul (β := M) r 1) s • x /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s

Tactic:
rfl
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
r : R
x : X
s : ↥S
⊢ HSMul.hSMul (β := OreLocalization S X) r (x /ₒ s) =
    oreNum (HSMul.hSMul (β := M) r 1) s • x /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s

Tactic:
with_unfolding_all rfl
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
r : M
x : OreLocalization S X
c :
  ∀ (r_1 : X) (s : ↥S),
    HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r /ₒ 1) (r_1 /ₒ s) =
      HSMul.hSMul (β := OreLocalization S X) r (r_1 /ₒ s)
⊢ HSMul.hSMul (α := OreLocalization S M) (r /ₒ 1) x = r • x

Tactic:
cases x
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
r : M
r_1 : X
s : ↥S
c :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r /ₒ 1) (r_1 /ₒ s) =
    oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s
c₁ :
  Eq (α := OreLocalization S X) (oreNum r s • r_1 /ₒ (oreDenom r s * 1))
    (oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s)
c₂ :
  Eq (α := OreLocalization S X) (oreNum r s • r_1 /ₒ oreDenom r s)
    (oreNum (HSMul.hSMul (β := M) r 1) s • r_1 /ₒ oreDenom (HSMul.hSMul (β := M) r 1) s)
c₃ : Eq (α := OreLocalization S X) (oreNum r s • r_1 /ₒ oreDenom r s) (oreNum (r * 1) s • r_1 /ₒ oreDenom (r * 1) s)
c₄ c₅ : Eq (α := OreLocalization S X) (oreNum r s • r_1 /ₒ oreDenom r s) (oreNum r s • r_1 /ₒ oreDenom r s)
⊢ HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r /ₒ 1) (r_1 /ₒ s) =
    HSMul.hSMul (β := OreLocalization S X) r (r_1 /ₒ s)

Tactic:
rw [smul_oreDiv, oreDiv_smul_oreDiv, mul_one, smul_eq_mul, mul_one]

Premises used: OreLocalization.smul_oreDiv, OreLocalization.oreDiv_smul_oreDiv, smul_eq_mul, mul_one
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
r : R
x : OreLocalization S X
c :
  ∀ (r_1 : X) (s : ↥S),
    HSMul.hSMul (β := OreLocalization S X) (HSMul.hSMul (β := M) r 1) (r_1 /ₒ s) =
      HSMul.hSMul (β := OreLocalization S X) r (r_1 /ₒ s)
⊢ HSMul.hSMul (β := M) r 1 • x = r • x

Tactic:
cases x
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
r : R
r_1 : X
s : ↥S
⊢ HSMul.hSMul (β := OreLocalization S X) (HSMul.hSMul (β := M) r 1) (r_1 /ₒ s) =
    HSMul.hSMul (β := OreLocalization S X) r (r_1 /ₒ s)

Tactic:
simp only [smul_oreDiv, smul_eq_mul, mul_one]

Premises used: OreLocalization.smul_oreDiv, smul_eq_mul, mul_one
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
r : R
x : OreLocalization S X
rw : HSMul.hSMul (β := M) r 1 • x = r • x
rw₁ rw₂ : r • x = r • x
⊢ HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) x = r • x

Tactic:
rw [oreDiv_one_smul, smul_one_smul]

Premises used: OreLocalization.smul_one_smul, OreLocalization.oreDiv_one_smul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
r : R
m : R'
x : OreLocalization S X
rw :
  HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) (r • m) 1 /ₒ 1) x =
    HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 * HSMul.hSMul (β := M) m 1 /ₒ 1) x
⊢ (r • m) • x = r • m • x

Tactic:
rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul,
      ← mul_smul, mul_div_one]

Premises used: OreLocalization.mul_div_one, OreLocalization.smul_one_oreDiv_one_smul, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
r : R
m : R'
x : OreLocalization S X
⊢ HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) (r • m) 1 /ₒ 1) x =
    HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 * HSMul.hSMul (β := M) m 1 /ₒ 1) x

Tactic:
simp only [smul_mul_assoc, smul_assoc, one_mul]

Premises used: smul_assoc, smul_mul_assoc, one_mul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
inst_13 : SMulCommClass R R' M
r : R
m : R'
x : OreLocalization S X
rw : r • HSMul.hSMul (β := M) m 1 • x = m • r • x
rw₁ : (r • HSMul.hSMul (β := M) m 1) • x = m • r • x
rw₂ : (m • HSMul.hSMul (β := M) r 1) • x = m • r • x
rw₃ : m • HSMul.hSMul (β := M) r 1 • x = m • r • x
rw₄ rw₅ : m • r • x = m • r • x
⊢ r • m • x = m • r • x

Tactic:
rw [← smul_one_smul m, ← smul_assoc, smul_comm, smul_assoc, smul_one_smul]

Premises used: smul_assoc, SMulCommClass.smul_comm, OreLocalization.smul_one_smul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
r : R
m : OreLocalization S M
x : OreLocalization S X
rw : HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) m • x = r • m • x
rw₁ :
  HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) m • x =
    HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) (m • x)
rw₂ :
  HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) m • x = (HSMul.hSMul (β := M) r 1 /ₒ 1 * m) • x
rw₃ rw₄ : (HSMul.hSMul (β := M) r 1 /ₒ 1 * m) • x = (HSMul.hSMul (β := M) r 1 /ₒ 1 * m) • x
⊢ (r • m) • x = r • m • x

Tactic:
rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← mul_smul, smul_eq_mul]

Premises used: OreLocalization.smul_one_oreDiv_one_smul, smul_eq_mul, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
inst_13 : SMulCommClass R M M
r : R
x : OreLocalization S M
y : OreLocalization S X
c :
  ∀ (r₁ : M) (s₁ : ↥S),
    r • HSMul.hSMul (α := OreLocalization S M) (r₁ /ₒ s₁) y = HSMul.hSMul (α := OreLocalization S M) (r₁ /ₒ s₁) (r • y)
⊢ r • x • y = x • r • y

Tactic:
cases x with | _ r₁ s₁
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
inst_13 : SMulCommClass R M M
r : R
y : OreLocalization S X
r₁ : M
s₁ : ↥S
c :
  ∀ (r₂ : X) (s₂ : ↥S),
    r • HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
      HSMul.hSMul (α := OreLocalization S M) (r₁ /ₒ s₁) (HSMul.hSMul (β := OreLocalization S X) r (r₂ /ₒ s₂))
⊢ r • HSMul.hSMul (α := OreLocalization S M) (r₁ /ₒ s₁) y = HSMul.hSMul (α := OreLocalization S M) (r₁ /ₒ s₁) (r • y)

Tactic:
cases y with | _ r₂ s₂
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
inst_13 : SMulCommClass R M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ (↑s₁ : M) * HSMul.hSMul (β := M) r 1 = HSMul.hSMul (β := M) r 1 * (↑s₁ : M)

Tactic:
simp
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
inst_13 : SMulCommClass R M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
c :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) r 1 * r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r₁ * HSMul.hSMul (β := M) r 1 /ₒ s₁) (r₂ /ₒ s₂)
⊢ r • HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    HSMul.hSMul (α := OreLocalization S M) (r₁ /ₒ s₁) (HSMul.hSMul (β := OreLocalization S X) r (r₂ /ₒ s₂))

Tactic:
rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, smul_smul, smul_smul,
      mul_div_one, oreDiv_mul_char _ _ _ _ (r • 1) s₁ (by simp), mul_one]

Premises used: OreLocalization.mul_div_one, smul_smul, OreLocalization.smul_one_oreDiv_one_smul, OreLocalization.oreDiv_mul_char, HSMul.hSMul, mul_one, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
inst_13 : SMulCommClass R M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) r 1 * r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (r₁ * HSMul.hSMul (β := M) r 1 /ₒ s₁) (r₂ /ₒ s₂)

Tactic:
simp
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R R'
inst_12 : IsScalarTower R R' M
inst_13 : SMul.{u_1, u_3} Rᵐᵒᵖ M
inst_14 : SMul.{u_1, u_4} Rᵐᵒᵖ X
inst_15 : IsScalarTower.{u_1, u_3, u_3} Rᵐᵒᵖ M M
inst_16 : IsScalarTower.{u_1, u_3, u_4} Rᵐᵒᵖ M X
inst_17 : IsCentralScalar R M
r : R
x : OreLocalization S X
rw : HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) (MulOpposite.op r) 1 /ₒ 1) x = r • x
rw₁ :
  HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) (MulOpposite.op r) 1 /ₒ 1) x =
    HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) x
rw₂ rw₃ :
  HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) x =
    HSMul.hSMul (α := OreLocalization S M) (HSMul.hSMul (β := M) r 1 /ₒ 1) x
⊢ MulOpposite.op r • x = r • x

Tactic:
rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, op_smul_eq_smul]

Premises used: OreLocalization.smul_one_oreDiv_one_smul, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R_1 : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R_1 X
inst_4 : SMul R_1 M
inst_5 : IsScalarTower R_1 M M
inst_6 : IsScalarTower R_1 M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R_1 R'
inst_12 : IsScalarTower R_1 R' M
R : Type u_5
inst_13 : Monoid R
inst_14 : MulAction R M
inst_15 : IsScalarTower R M M
inst_16 : MulAction R X
inst_17 : IsScalarTower R M X
s₁ s₂ : R
x : OreLocalization S X
rw : (s₁ • s₂) • x = s₁ • s₂ • x
rw₁ rw₂ : s₁ • s₂ • x = s₁ • s₂ • x
⊢ (s₁ * s₂) • x = s₁ • s₂ • x

Tactic:
rw [← smul_eq_mul, smul_assoc]

Premises used: smul_assoc, smul_eq_mul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R_1 : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R_1 X
inst_4 : SMul R_1 M
inst_5 : IsScalarTower R_1 M M
inst_6 : IsScalarTower R_1 M X
inst_7 : SMul R' X
inst_8 : SMul R' M
inst_9 : IsScalarTower R' M M
inst_10 : IsScalarTower R' M X
inst_11 : SMul R_1 R'
inst_12 : IsScalarTower R_1 R' M
R : Type u_5
inst_13 : Monoid R
inst_14 : MulAction R M
inst_15 : IsScalarTower R M M
inst_16 : MulAction R X
inst_17 : IsScalarTower R M X
x : X
s : ↥S
rw :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X)
      (HSMul.hSMul.{u_5, u_3, u_3} (α := R) (β := M) 1 1 /ₒ 1) (x /ₒ s) =
    x /ₒ s
rw₁ : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (1 /ₒ 1) (x /ₒ s) = x /ₒ s
rw₂ : HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) 1 (x /ₒ s) = x /ₒ s
rw₃ rw₄ : Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s)
⊢ HSMul.hSMul (α := R) (β := OreLocalization S X) 1 (x /ₒ s) = x /ₒ s

Tactic:
rw [← smul_one_oreDiv_one_smul, one_smul, ← OreLocalization.one_def, one_smul]

Premises used: one_smul, OreLocalization.smul_one_oreDiv_one_smul, OreLocalization.one_def
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
M : Type u_3
X : Type u_4
inst : Monoid M
S : Submonoid M
inst_1 : OreSet S
inst_2 : MulAction M X
inst_3 : SMul R X
inst_4 : SMul R M
inst_5 : IsScalarTower R M M
inst_6 : IsScalarTower R M X
r : R
x : X
rw :
  HSMul.hSMul (α := OreLocalization S M) (β := OreLocalization S X) (HSMul.hSMul (β := M) r 1 /ₒ 1) (x /ₒ 1) =
    r • x /ₒ 1
rw₁ : Eq (α := OreLocalization S X) (HSMul.hSMul (β := M) r 1 • x /ₒ 1) (r • x /ₒ 1)
rw₂ : Eq (α := OreLocalization S X) (r • HSMul.hSMul.{u_3, u_4, u_4} (α := M) 1 x /ₒ 1) (r • x /ₒ 1)
rw₃ rw₄ : Eq (α := OreLocalization S X) (r • x /ₒ 1) (r • x /ₒ 1)
⊢ HSMul.hSMul (β := OreLocalization S X) r (x /ₒ 1) = r • x /ₒ 1

Tactic:
rw [← smul_one_oreDiv_one_smul, smul_div_one, smul_assoc, one_smul]

Premises used: smul_assoc, one_smul, OreLocalization.smul_one_oreDiv_one_smul, OreLocalization.smul_div_one
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : CommMonoid R
S : Submonoid R
inst_1 : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ (↑s₂ : R) * r₁ = r₁ * (↑s₂ : R)

Tactic:
simp [mul_comm]

Premises used: mul_comm