awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this :
  ((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m =
    (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
⊢ ((↑a.den : ℤ) * HMul.hMul (α := ℤ) (↑b.den : ℤ) (↑(↑s : ℕ) : ℤ) * (a * b).num) • m =
    ((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this :
  ((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m =
    (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
h :
  (HMul.hMul (α := ℤ) (↑(a * b).den : ℤ) (↑(↑s : ℕ) : ℤ) * (a.num * b.num)) • m =
    (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
⊢ (↑1 : ℕ) • (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a * b).den ⋯ * s) : ℕ) • a.num • b.num • m =
    (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m

Tactic:
simp [← natCast_zsmul, smul_smul]

Premises used: smul_smul, natCast_zsmul
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this :
  ((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m =
    (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
⊢ (HMul.hMul (α := ℤ) (↑(a * b).den : ℤ) (↑(↑s : ℕ) : ℤ) * (a.num * b.num)) • m =
    (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
h :
  ((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m =
    (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
⊢ (↑1 : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s)) : ℕ) •
        (a * b).num • m =
    (↑1 : ℕ) • (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a * b).den ⋯ * s) : ℕ) • a.num • b.num • m

Tactic:
suffices ((a * b).num * a.den * b.den * s) • m = (a.num * b.num * (a * b).den * s) • m by
      convert! this using 1
      all_goals
      simp [← natCast_zsmul, smul_smul]
      ring_nf
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
h h₁ :
  (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m =
    (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
⊢ ((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m =
    (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m

Tactic:
rw [Rat.mul_num_den']

Premises used: Rat.mul_num_den'
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
x : DivisibleHull M
mk : ∀ (m : M) (s : ℕ+), HSMul.hSMul (α := ℚ) (β := DivisibleHull M) 1 (DivisibleHull.mk m s) = DivisibleHull.mk m s
⊢ HSMul.hSMul (α := ℚ) 1 x = x

Tactic:
induction x with | mk m s

Premises used: DivisibleHull.mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
m : M
s : ℕ+
⊢ HSMul.hSMul (α := ℚ) (β := DivisibleHull M) 1 (mk m s) = mk m s

Tactic:
simp [qsmul_of_nonneg zero_le_one, nnqsmul_mk]

Premises used: zero_le_one, DivisibleHull.qsmul_of_nonneg, DivisibleHull.nnqsmul_mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a : ℚ
⊢ HSMul.hSMul (β := DivisibleHull M) a 0 = 0

Tactic:
simp [qsmul_def]

Premises used: DivisibleHull.qsmul_def
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a : ℚ
x y : DivisibleHull M
⊢ a • (x + y) = a • x + a • y

Tactic:
simp [qsmul_def, smul_add]

Premises used: DivisibleHull.qsmul_def, smul_add
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
x : DivisibleHull M
mk :
  ∀ (m : M) (s : ℕ+),
    HSMul.hSMul (β := DivisibleHull M) (a + b) (DivisibleHull.mk m s) =
      HSMul.hSMul (β := DivisibleHull M) a (DivisibleHull.mk m s) +
        HSMul.hSMul (β := DivisibleHull M) b (DivisibleHull.mk m s)
⊢ (a + b) • x = a • x + b • x

Tactic:
induction x with | mk m s

Premises used: DivisibleHull.mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
mk :
  ∃ (u : ℕ+),
    (↑u : ℕ) •
        (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s)) :
            ℕ) •
          (a + b).num • m =
      (↑u : ℕ) •
        (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a + b).den ⋯ * s) : ℕ) •
          ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s) : ℕ) • a.num • m +
            (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s) : ℕ) • b.num • m)
⊢ HSMul.hSMul (β := DivisibleHull M) (a + b) (DivisibleHull.mk m s) =
    HSMul.hSMul (β := DivisibleHull M) a (DivisibleHull.mk m s) +
      HSMul.hSMul (β := DivisibleHull M) b (DivisibleHull.mk m s)

Tactic:
simp_rw [qsmul_mk, mk_add_mk, mk_eq_mk]

Premises used: DivisibleHull.mk_add_mk, DivisibleHull.qsmul_mk, DivisibleHull.mk_eq_mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
h :
  (↑1 : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s)) : ℕ) •
        (a + b).num • m =
    (↑1 : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a + b).den ⋯ * s) : ℕ) •
        ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s) : ℕ) • a.num • m +
          (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s) : ℕ) • b.num • m)
⊢ ∃ (u : ℕ+),
    (↑u : ℕ) •
        (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s)) :
            ℕ) •
          (a + b).num • m =
      (↑u : ℕ) •
        (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a + b).den ⋯ * s) : ℕ) •
          ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s) : ℕ) • a.num • m +
            (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s) : ℕ) • b.num • m)

Tactic:
use 1
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this :
  ((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) • m =
    ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m
⊢ ((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) • m =
    ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m

Tactic:
this
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this :
  ((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) • m =
    ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m
h :
  (↑1 : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s)) : ℕ) •
        (a + b).num • m =
    ((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) • m
h₁ :
  (↑1 : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a + b).den ⋯ * s) : ℕ) •
        ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s) : ℕ) • a.num • m +
          (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s) : ℕ) • b.num • m) =
    ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m
⊢ (↑1 : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s)) : ℕ) •
        (a + b).num • m =
    (↑1 : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a + b).den ⋯ * s) : ℕ) •
        ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s) : ℕ) • a.num • m +
          (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s) : ℕ) • b.num • m)

Tactic:
convert! this using 1
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this :
  ((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) • m =
    ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m
h :
  (HMul.hMul (α := ℤ) (↑a.den : ℤ) (↑(↑s : ℕ) : ℤ) * HMul.hMul (α := ℤ) (↑b.den : ℤ) (↑(↑s : ℕ) : ℤ) * (a + b).num) •
      m =
    ((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) • m
⊢ (↑1 : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s)) : ℕ) •
        (a + b).num • m =
    ((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) • m

Tactic:
simp [← natCast_zsmul, smul_smul, ← add_smul]

Premises used: smul_smul, add_smul, natCast_zsmul
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this :
  ((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) • m =
    ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m
⊢ (HMul.hMul (α := ℤ) (↑a.den : ℤ) (↑(↑s : ℕ) : ℤ) * HMul.hMul (α := ℤ) (↑b.den : ℤ) (↑(↑s : ℕ) : ℤ) * (a + b).num) •
      m =
    ((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) • m

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this :
  ((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) • m =
    ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m
h :
  (HMul.hMul (α := ℤ) (↑(a + b).den : ℤ) (↑(↑s : ℕ) : ℤ) *
        (HMul.hMul (α := ℤ) (↑b.den : ℤ) (↑(↑s : ℕ) : ℤ) * a.num +
          HMul.hMul (α := ℤ) (↑a.den : ℤ) (↑(↑s : ℕ) : ℤ) * b.num)) •
      m =
    ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m
⊢ (↑1 : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a + b).den ⋯ * s) : ℕ) •
        ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s) : ℕ) • a.num • m +
          (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s) : ℕ) • b.num • m) =
    ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m

Tactic:
simp [← natCast_zsmul, smul_smul, ← add_smul]

Premises used: smul_smul, add_smul, natCast_zsmul
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this :
  ((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) • m =
    ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m
⊢ (HMul.hMul (α := ℤ) (↑(a + b).den : ℤ) (↑(↑s : ℕ) : ℤ) *
        (HMul.hMul (α := ℤ) (↑b.den : ℤ) (↑(↑s : ℕ) : ℤ) * a.num +
          HMul.hMul (α := ℤ) (↑a.den : ℤ) (↑(↑s : ℕ) : ℤ) * b.num)) •
      m =
    ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
h :
  ((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) • m =
    ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m
⊢ (↑1 : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s)) : ℕ) •
        (a + b).num • m =
    (↑1 : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a + b).den ⋯ * s) : ℕ) •
        ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s) : ℕ) • a.num • m +
          (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s) : ℕ) • b.num • m)

Tactic:
suffices ((a + b).num * a.den * b.den * (s * s)) • m =
        ((a.num * b.den + b.num * a.den) * (a + b).den * (s * s)) • m by
      convert! this using 1
      all_goals
      simp [← natCast_zsmul, smul_smul, ← add_smul]
      ring_nf
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
h h₁ :
  ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m =
    ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m
⊢ ((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) • m =
    ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
        HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
      m

Tactic:
rw [Rat.add_num_den']

Premises used: Rat.add_num_den'
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℤ
m : M
s : ℕ+
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a • m) s

Tactic:
simp [← Int.cast_smul_eq_zsmul ℚ a, qsmul_mk]

Premises used: Rat, DivisibleHull.qsmul_mk, Int.cast_smul_eq_zsmul
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : Eq (α := DivisibleHull M) (mk m s) (mk m' s')
h' : Eq (α := DivisibleHull M) (mk n t) (mk n' t')
⊢ (↑s' : ℕ) • m = (↑s : ℕ) • m'

Tactic:
rw [mk_eq_mk_iff_smul_eq_smul] at h h'

Premises used: DivisibleHull.mk_eq_mk_iff_smul_eq_smul
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : Eq (α := DivisibleHull M) (mk m s) (mk m' s')
h' : Eq (α := DivisibleHull M) (mk n t) (mk n' t')
h₁ : (↑s' : ℕ) • m = (↑s : ℕ) • m'
⊢ (↑t' : ℕ) • n = (↑t : ℕ) • n'

Tactic:
rw [mk_eq_mk_iff_smul_eq_smul] at h h'

Premises used: DivisibleHull.mk_eq_mk_iff_smul_eq_smul
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : (↑s' : ℕ) • m = (↑s : ℕ) • m'
h' : (↑t' : ℕ) • n = (↑t : ℕ) • n'
rw : ((↑s' : ℕ) * (↑t' : ℕ)) • (↑t : ℕ) • m ≤ ((↑s' : ℕ) * (↑t' : ℕ)) • (↑s : ℕ) • n ↔ (↑t' : ℕ) • m' ≤ (↑s' : ℕ) • n'
⊢ ((↑t : ℕ) • m ≤ (↑s : ℕ) • n) = ((↑t' : ℕ) • m' ≤ (↑s' : ℕ) • n')

Tactic:
rw [propext_iff, ← nsmul_le_nsmul_iff_right (mul_ne_zero s'.ne_zero t'.ne_zero)]

Premises used: PNat.ne_zero, nsmul_le_nsmul_iff_right, propext_iff, mul_ne_zero
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : (↑s' : ℕ) • m = (↑s : ℕ) • m'
h' : (↑t' : ℕ) • n = (↑t : ℕ) • n'
⊢ ((↑s : ℕ) * (↑t : ℕ)) • (↑t' : ℕ) • m' ≤ ((↑s : ℕ) * (↑t : ℕ)) • (↑s' : ℕ) • n' ↔ (↑t' : ℕ) • m' ≤ (↑s' : ℕ) • n'

Tactic:
(nsmul_le_nsmul_iff_right (M := M) (mul_ne_zero s.ne_zero t.ne_zero))

Premises used: PNat.ne_zero, nsmul_le_nsmul_iff_right, mul_ne_zero
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : (↑s' : ℕ) • m = (↑s : ℕ) • m'
h' : (↑t' : ℕ) • n = (↑t : ℕ) • n'
h₁ : ((↑s' : ℕ) * (↑t' : ℕ)) • (↑t : ℕ) • m = ((↑s : ℕ) * (↑t : ℕ)) • (↑t' : ℕ) • m'
h₂ : ((↑s' : ℕ) * (↑t' : ℕ)) • (↑s : ℕ) • n = ((↑s : ℕ) * (↑t : ℕ)) • (↑s' : ℕ) • n'
⊢ ((↑s' : ℕ) * (↑t' : ℕ)) • (↑t : ℕ) • m ≤ ((↑s' : ℕ) * (↑t' : ℕ)) • (↑s : ℕ) • n ↔ (↑t' : ℕ) • m' ≤ (↑s' : ℕ) • n'

Tactic:
convert! (nsmul_le_nsmul_iff_right (M := M) (mul_ne_zero s.ne_zero t.ne_zero)) using 2

Premises used: PNat.ne_zero, nsmul_le_nsmul_iff_right, mul_ne_zero
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : (↑s' : ℕ) • m = (↑s : ℕ) • m'
h' : (↑t' : ℕ) • n = (↑t : ℕ) • n'
h₁ : ((↑t' : ℕ) * ((↑t : ℕ) * (↑s : ℕ))) • m' = ((↑s : ℕ) * ((↑t : ℕ) * (↑t' : ℕ))) • m'
⊢ ((↑s' : ℕ) * (↑t' : ℕ)) • (↑t : ℕ) • m = ((↑s : ℕ) * (↑t : ℕ)) • (↑t' : ℕ) • m'

Tactic:
simp_rw [smul_smul, mul_rotate s'.val, ← smul_smul, h, smul_smul]

Premises used: PNat.val, smul_smul, mul_rotate
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : (↑s' : ℕ) • m = (↑s : ℕ) • m'
h' : (↑t' : ℕ) • n = (↑t : ℕ) • n'
⊢ ((↑t' : ℕ) * ((↑t : ℕ) * (↑s : ℕ))) • m' = ((↑s : ℕ) * ((↑t : ℕ) * (↑t' : ℕ))) • m'

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : (↑s' : ℕ) • m = (↑s : ℕ) • m'
h' : (↑t' : ℕ) • n = (↑t : ℕ) • n'
h₁ : ((↑s' : ℕ) * ((↑t' : ℕ) * (↑s : ℕ))) • n = ((↑s' : ℕ) * ((↑s : ℕ) * (↑t' : ℕ))) • n
⊢ ((↑s' : ℕ) * (↑t' : ℕ)) • (↑s : ℕ) • n = ((↑s : ℕ) * (↑t : ℕ)) • (↑s' : ℕ) • n'

Tactic:
simp_rw [smul_smul, ← mul_rotate s'.val, ← smul_smul, ← h', smul_smul]

Premises used: PNat.val, smul_smul, mul_rotate
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : (↑s' : ℕ) • m = (↑s : ℕ) • m'
h' : (↑t' : ℕ) • n = (↑t : ℕ) • n'
⊢ ((↑s' : ℕ) * ((↑t' : ℕ) * (↑s : ℕ))) • n = ((↑s' : ℕ) * ((↑s : ℕ) * (↑t' : ℕ))) • n

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedCancelAddMonoid M
m m' : M
s s' : ℕ+
⊢ LE.le (α := DivisibleHull M) (mk m s) (mk m' s') ↔ (↑s' : ℕ) • m ≤ (↑s : ℕ) • m'

Tactic:
rfl
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
a : DivisibleHull M
mk : ∀ (m : M) (s : ℕ+), LE.le (α := DivisibleHull M) (DivisibleHull.mk m s) (DivisibleHull.mk m s)
⊢ a ≤ a

Tactic:
induction a with | mk m s

Premises used: DivisibleHull.mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
m : M
s : ℕ+
⊢ LE.le (α := DivisibleHull M) (mk m s) (mk m s)

Tactic:
simp
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
a b c : DivisibleHull M
hab : a ≤ b
hbc : b ≤ c
mk : ∀ (ma : M) (sa : ℕ+) (hab : DivisibleHull.mk ma sa ≤ b), DivisibleHull.mk ma sa ≤ c
⊢ a ≤ c

Tactic:
induction a with | mk ma sa

Premises used: DivisibleHull.mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
b c : DivisibleHull M
hbc : b ≤ c
ma : M
sa : ℕ+
hab : DivisibleHull.mk ma sa ≤ b
mk :
  ∀ (mb : M) (sb : ℕ+) (hbc : DivisibleHull.mk mb sb ≤ c)
    (hab : LE.le (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mb sb)), DivisibleHull.mk ma sa ≤ c
⊢ DivisibleHull.mk ma sa ≤ c

Tactic:
induction b with | mk mb sb

Premises used: DivisibleHull.mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
c : DivisibleHull M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
hbc : DivisibleHull.mk mb sb ≤ c
hab : LE.le (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mb sb)
mk :
  ∀ (mc : M) (sc : ℕ+) (hbc : LE.le (α := DivisibleHull M) (DivisibleHull.mk mb sb) (DivisibleHull.mk mc sc)),
    LE.le (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mc sc)
⊢ DivisibleHull.mk ma sa ≤ c

Tactic:
induction c with | mk mc sc

Premises used: DivisibleHull.mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
hab : LE.le (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mb sb)
mc : M
sc : ℕ+
hbc : LE.le (α := DivisibleHull M) (DivisibleHull.mk mb sb) (DivisibleHull.mk mc sc)
mk :
  ∀ (hab : (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb) (mc : M) (sc : ℕ+) (hbc : (↑sc : ℕ) • mb ≤ (↑sb : ℕ) • mc),
    (↑sc : ℕ) • ma ≤ (↑sa : ℕ) • mc
⊢ LE.le (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mc sc)

Tactic:
rw [mk_le_mk] at ⊢ hab hbc

Premises used: DivisibleHull.mk_le_mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
hab : (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb
mc : M
sc : ℕ+
hbc : (↑sc : ℕ) • mb ≤ (↑sb : ℕ) • mc
⊢ (↑sb : ℕ) ≠ 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
hab : (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb
mc : M
sc : ℕ+
hbc : (↑sc : ℕ) • mb ≤ (↑sb : ℕ) • mc
mk : (↑sc : ℕ) • (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • (↑sb : ℕ) • mc
⊢ (↑sc : ℕ) • ma ≤ (↑sa : ℕ) • mc

Tactic:
rw [← nsmul_le_nsmul_iff_right (show sb.val ≠ 0 by simp), smul_comm _ _ ma, smul_comm _ _ mc]

Premises used: nsmul_le_nsmul_iff_right, SMulCommClass.smul_comm
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
hab : (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb
mc : M
sc : ℕ+
hbc : (↑sc : ℕ) • mb ≤ (↑sb : ℕ) • mc
⊢ (↑sc : ℕ) ≠ 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
hab : (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb
mc : M
sc : ℕ+
hbc : (↑sc : ℕ) • mb ≤ (↑sb : ℕ) • mc
⊢ (↑sc : ℕ) • (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • (↑sc : ℕ) • mb

Tactic:
rw [← nsmul_le_nsmul_iff_right (show sc.val ≠ 0 by simp), smul_comm _ _ mb] at hab

Premises used: nsmul_le_nsmul_iff_right, SMulCommClass.smul_comm