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 : 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
hab₁ : (↑sc : ℕ) • (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • (↑sc : ℕ) • mb
⊢ (↑sc : ℕ) • mb ≤ (↑sb : ℕ) • mc

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
-- 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 : ℕ+
mc : M
sc : ℕ+
hab : (↑sc : ℕ) • (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • (↑sc : ℕ) • mb
hbc : (↑sc : ℕ) • mb ≤ (↑sb : ℕ) • mc
⊢ (↑sa : ℕ) ≠ 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 : ℕ+
mc : M
sc : ℕ+
hab : (↑sc : ℕ) • (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • (↑sc : ℕ) • mb
hbc : (↑sc : ℕ) • mb ≤ (↑sb : ℕ) • mc
⊢ (↑sa : ℕ) • (↑sc : ℕ) • mb ≤ (↑sa : ℕ) • (↑sb : ℕ) • mc

Tactic:
rw [← nsmul_le_nsmul_iff_right (show sa.val ≠ 0 by simp)] at hbc

Premises used: nsmul_le_nsmul_iff_right
-- 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 : ℕ+
mc : M
sc : ℕ+
hab : (↑sc : ℕ) • (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • (↑sc : ℕ) • mb
hbc : (↑sa : ℕ) • (↑sc : ℕ) • mb ≤ (↑sa : ℕ) • (↑sb : ℕ) • mc
⊢ (↑sc : ℕ) • (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • (↑sb : ℕ) • mc

Tactic:
hab.trans hbc

Premises used: LE.le.trans
-- 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 : ℕ+
mc : M
sc : ℕ+
hab : (↑sc : ℕ) • (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • (↑sc : ℕ) • mb
hbc : (↑sa : ℕ) • (↑sc : ℕ) • mb ≤ (↑sa : ℕ) • (↑sb : ℕ) • mc
⊢ (↑sc : ℕ) • (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • (↑sb : ℕ) • mc

Tactic:
exact hab.trans hbc

Premises used: LE.le.trans
-- 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 : DivisibleHull M
h : a ≤ b
h' : b ≤ a
mk : ∀ (ma : M) (sa : ℕ+) (h : DivisibleHull.mk ma sa ≤ b) (h' : b ≤ DivisibleHull.mk ma sa), DivisibleHull.mk ma sa = b
⊢ a = b

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 : DivisibleHull M
ma : M
sa : ℕ+
h : DivisibleHull.mk ma sa ≤ b
h' : b ≤ DivisibleHull.mk ma sa
mk :
  ∀ (mb : M) (sb : ℕ+) (h : LE.le (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mb sb))
    (h' : LE.le (α := DivisibleHull M) (DivisibleHull.mk mb sb) (DivisibleHull.mk ma sa)),
    Eq (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mb sb)
⊢ DivisibleHull.mk ma sa = b

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
ma : M
sa : ℕ+
mb : M
sb : ℕ+
h : LE.le (α := DivisibleHull M) (mk ma sa) (mk mb sb)
h' : LE.le (α := DivisibleHull M) (mk mb sb) (mk ma sa)
⊢ (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb

Tactic:
rw [mk_le_mk] at h h'

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 : ℕ+
h : LE.le (α := DivisibleHull M) (mk ma sa) (mk mb sb)
h' : LE.le (α := DivisibleHull M) (mk mb sb) (mk ma sa)
h₁ : (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb
⊢ (↑sa : ℕ) • mb ≤ (↑sb : ℕ) • ma

Tactic:
rw [mk_le_mk] at h h'

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 : ℕ+
h : (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb
h' : (↑sa : ℕ) • mb ≤ (↑sb : ℕ) • ma
mk : (↑sb : ℕ) • ma = (↑sa : ℕ) • mb
⊢ Eq (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mb sb)

Tactic:
rw [mk_eq_mk_iff_smul_eq_smul]

Premises used: DivisibleHull.mk_eq_mk_iff_smul_eq_smul
-- 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 : ℕ+
h : (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb
h' : (↑sa : ℕ) • mb ≤ (↑sb : ℕ) • ma
⊢ (↑sb : ℕ) • ma = (↑sa : ℕ) • mb

Tactic:
le_antisymm h h'

Premises used: le_antisymm
-- 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 : ℕ+
h : (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb
h' : (↑sa : ℕ) • mb ≤ (↑sb : ℕ) • ma
⊢ (↑sb : ℕ) • ma = (↑sa : ℕ) • mb

Tactic:
exact le_antisymm h h'

Premises used: le_antisymm
-- 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 : DivisibleHull M
mk : ∀ (ma : M) (sa : ℕ+), DivisibleHull.mk ma sa ≤ b ∨ b ≤ DivisibleHull.mk ma sa
⊢ a ≤ b ∨ b ≤ a

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 : DivisibleHull M
ma : M
sa : ℕ+
mk :
  ∀ (mb : M) (sb : ℕ+),
    LE.le (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mb sb) ∨
      LE.le (α := DivisibleHull M) (DivisibleHull.mk mb sb) (DivisibleHull.mk ma sa)
⊢ DivisibleHull.mk ma sa ≤ b ∨ b ≤ DivisibleHull.mk ma sa

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
ma : M
sa : ℕ+
mb : M
sb : ℕ+
mk : (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb ∨ (↑sa : ℕ) • mb ≤ (↑sb : ℕ) • ma
⊢ LE.le (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mb sb) ∨
    LE.le (α := DivisibleHull M) (DivisibleHull.mk mb sb) (DivisibleHull.mk ma sa)

Tactic:
simp_rw [mk_le_mk]

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 : ℕ+
⊢ (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb ∨ (↑sa : ℕ) • mb ≤ (↑sb : ℕ) • ma

Tactic:
le_total _ _

Premises used: le_total
-- 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 : ℕ+
⊢ (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb ∨ (↑sa : ℕ) • mb ≤ (↑sb : ℕ) • ma

Tactic:
exact le_total _ _

Premises used: le_total
-- 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
⊢ DecidableRel (α := DivisibleHull M) (β := DivisibleHull M)
    {
        le := fun (x y : DivisibleHull M) ↦
          Quotient.liftOn₂ x y
            (fun (p q : M × ↥(nonZeroDivisors ℕ)) ↦
              (fun (m : M) (s : ℕ+) (n : M) (t : ℕ+) ↦ (↑t : ℕ) • m ≤ (↑s : ℕ) • n) p.1
                ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) p.2) q.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) q.2))
            ⋯ }.1

Tactic:
infer_instance
-- 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' : ℕ+
simp_rw : ¬LE.le (α := DivisibleHull M) (mk m' s') (mk m s) ↔ ¬(↑s : ℕ) • m' ≤ (↑s' : ℕ) • m
⊢ LT.lt (α := DivisibleHull M) (mk m s) (mk m' s') ↔ (↑s' : ℕ) • m < (↑s : ℕ) • m'

Tactic:
simp_rw [lt_iff_not_ge, mk_le_mk]

Premises used: lt_iff_not_ge, 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
a b c : DivisibleHull M
h : b < c
mk : ∀ (ma : M) (sa : ℕ+), DivisibleHull.mk ma sa + b < DivisibleHull.mk ma sa + c
⊢ a + b < 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
h : b < c
ma : M
sa : ℕ+
mk :
  ∀ (mb : M) (sb : ℕ+) (h : DivisibleHull.mk mb sb < c),
    HAdd.hAdd (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mb sb) < DivisibleHull.mk ma sa + c
⊢ DivisibleHull.mk ma sa + b < 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 : ℕ+
h : DivisibleHull.mk mb sb < c
mk :
  ∀ (mc : M) (sc : ℕ+) (h : LT.lt (α := DivisibleHull M) (DivisibleHull.mk mb sb) (DivisibleHull.mk mc sc)),
    HAdd.hAdd (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mb sb) <
      HAdd.hAdd (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mc sc)
⊢ HAdd.hAdd (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mb sb) < 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 : ℕ+
mc : M
sc : ℕ+
h : LT.lt (α := DivisibleHull M) (DivisibleHull.mk mb sb) (DivisibleHull.mk mc sc)
mk :
  LT.lt (α := DivisibleHull M) (DivisibleHull.mk ((↑sb : ℕ) • ma + (↑sa : ℕ) • mb) (sa * sb))
    (DivisibleHull.mk ((↑sc : ℕ) • ma + (↑sa : ℕ) • mc) (sa * sc))
⊢ HAdd.hAdd (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mb sb) <
    HAdd.hAdd (α := DivisibleHull M) (DivisibleHull.mk ma sa) (DivisibleHull.mk mc sc)

Tactic:
simp_rw [mk_add_mk]

Premises used: DivisibleHull.mk_add_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 : ℕ+
mc : M
sc : ℕ+
h : LT.lt (α := DivisibleHull M) (DivisibleHull.mk mb sb) (DivisibleHull.mk mc sc)
mk :
  ∀ (h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc),
    (↑(sa * sc) : ℕ) • ((↑sb : ℕ) • ma + (↑sa : ℕ) • mb) < (↑(sa * sb) : ℕ) • ((↑sc : ℕ) • ma + (↑sa : ℕ) • mc)
⊢ LT.lt (α := DivisibleHull M) (DivisibleHull.mk ((↑sb : ℕ) • ma + (↑sa : ℕ) • mb) (sa * sb))
    (DivisibleHull.mk ((↑sc : ℕ) • ma + (↑sa : ℕ) • mc) (sa * sc))

Tactic:
rw [mk_lt_mk] at ⊢ h

Premises used: DivisibleHull.mk_lt_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 : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
mk :
  ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sb : ℕ))) • ma + ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sa : ℕ))) • mb <
    ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sc : ℕ))) • ma + ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sa : ℕ))) • mc
⊢ (↑(sa * sc) : ℕ) • ((↑sb : ℕ) • ma + (↑sa : ℕ) • mb) < (↑(sa * sb) : ℕ) • ((↑sc : ℕ) • ma + (↑sa : ℕ) • mc)

Tactic:
simp_rw [PNat.mul_coe, mul_smul, smul_add, smul_smul]

Premises used: smul_smul, PNat.mul_coe, SemigroupAction.mul_smul, smul_add
-- 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 : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
⊢ ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + (↑(sa * sa) : ℕ) • (↑sc : ℕ) • mb <
    ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + (↑(sa * sa) : ℕ) • (↑sb : ℕ) • mc

Tactic:
have := add_lt_add_right (nsmul_lt_nsmul_right (sa * sa).ne_zero h) ((sa * sb * sc.val) • ma)
-- 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 : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
this :
  ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + (↑(sa * sa) : ℕ) • (↑sc : ℕ) • mb <
    ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + (↑(sa * sa) : ℕ) • (↑sb : ℕ) • mc
⊢ ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sc : ℕ)) • mb <
    ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sb : ℕ)) • mc

Tactic:
simp_rw [PNat.mul_coe, smul_smul] at this

Premises used: smul_smul, PNat.mul_coe
-- 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 : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
this :
  ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sc : ℕ)) • mb <
    ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sb : ℕ)) • mc
⊢ ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sc : ℕ)) • mb <
    ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sb : ℕ)) • mc

Tactic:
this
-- 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 : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
this :
  ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sc : ℕ)) • mb <
    ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sb : ℕ)) • mc
h₁ : (↑sa : ℕ) * ((↑sc : ℕ) * (↑sb : ℕ)) = (↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)
h₂ : (↑sa : ℕ) * ((↑sc : ℕ) * (↑sa : ℕ)) = (↑sa : ℕ) * (↑sa : ℕ) * (↑sc : ℕ)
h₃ : (↑sa : ℕ) * ((↑sb : ℕ) * (↑sc : ℕ)) = (↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)
h₄ : (↑sa : ℕ) * ((↑sb : ℕ) * (↑sa : ℕ)) = (↑sa : ℕ) * (↑sa : ℕ) * (↑sb : ℕ)
⊢ ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sb : ℕ))) • ma + ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sa : ℕ))) • mb <
    ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sc : ℕ))) • ma + ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sa : ℕ))) • mc

Tactic:
convert! this using 3
-- 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 : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
this :
  ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sc : ℕ)) • mb <
    ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sb : ℕ)) • mc
⊢ (↑sa : ℕ) * ((↑sc : ℕ) * (↑sb : ℕ)) = (↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)

Tactic:
ring
-- 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 : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
this :
  ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sc : ℕ)) • mb <
    ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sb : ℕ)) • mc
⊢ (↑sa : ℕ) * ((↑sc : ℕ) * (↑sa : ℕ)) = (↑sa : ℕ) * (↑sa : ℕ) * (↑sc : ℕ)

Tactic:
ring
-- 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 : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
this :
  ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sc : ℕ)) • mb <
    ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sb : ℕ)) • mc
⊢ (↑sa : ℕ) * ((↑sb : ℕ) * (↑sc : ℕ)) = (↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)

Tactic:
ring
-- 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 : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
this :
  ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sc : ℕ)) • mb <
    ((↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)) • ma + ((↑sa : ℕ) * (↑sa : ℕ) * (↑sb : ℕ)) • mc
⊢ (↑sa : ℕ) * ((↑sb : ℕ) * (↑sa : ℕ)) = (↑sa : ℕ) * (↑sa : ℕ) * (↑sb : ℕ)

Tactic:
ring
-- 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 : ℚ≥0
ha : 0 < a
b c : DivisibleHull M
h : b < c
mk :
  ∀ (mb : M) (sb : ℕ+) (h : DivisibleHull.mk mb sb < c),
    HSMul.hSMul (β := DivisibleHull M) a (DivisibleHull.mk mb sb) < a • c
⊢ a • b < a • 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
a : ℚ≥0
ha : 0 < a
c : DivisibleHull M
mb : M
sb : ℕ+
h : DivisibleHull.mk mb sb < c
mk :
  ∀ (mc : M) (sc : ℕ+) (h : LT.lt (α := DivisibleHull M) (DivisibleHull.mk mb sb) (DivisibleHull.mk mc sc)),
    HSMul.hSMul (β := DivisibleHull M) a (DivisibleHull.mk mb sb) <
      HSMul.hSMul (β := DivisibleHull M) a (DivisibleHull.mk mc sc)
⊢ HSMul.hSMul (β := DivisibleHull M) a (DivisibleHull.mk mb sb) < a • 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
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : LT.lt (α := DivisibleHull M) (mk mb sb) (mk mc sc)
⊢ (↑sc : ℕ) • mb < (↑sb : ℕ) • mc

Tactic:
simp_rw [mk_lt_mk] at h

Premises used: DivisibleHull.mk_lt_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
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
mk :
  ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯) : ℕ) * (↑sc : ℕ) * a.num) • mb <
    ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯) : ℕ) * (↑sb : ℕ) * a.num) • mc
⊢ HSMul.hSMul (β := DivisibleHull M) a (DivisibleHull.mk mb sb) <
    HSMul.hSMul (β := DivisibleHull M) a (DivisibleHull.mk mc sc)

Tactic:
simp_rw [nnqsmul_mk, mk_lt_mk, smul_smul, PNat.mul_coe]

Premises used: smul_smul, PNat.mul_coe, DivisibleHull.mk_lt_mk, DivisibleHull.nnqsmul_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
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
mk :
  ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯) : ℕ) * a.num) • (↑sc : ℕ) • mb <
    ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯) : ℕ) * a.num) • (↑sb : ℕ) • mc
⊢ ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯) : ℕ) * (↑sc : ℕ) * a.num) • mb <
    ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯) : ℕ) * (↑sb : ℕ) * a.num) • mc

Tactic:
simp_rw [mul_right_comm _ _ a.num, mul_smul _ _ mc, mul_smul _ _ mb]

Premises used: NNRat.num, mul_right_comm, SemigroupAction.mul_smul
-- 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 : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
⊢ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯) : ℕ) * a.num ≠ 0

Tactic:
simpa using ha.ne.symm

Premises used: Ne.symm, LT.lt.ne
-- 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 : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
⊢ ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯) : ℕ) * a.num) • (↑sc : ℕ) • mb <
    ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯) : ℕ) * a.num) • (↑sb : ℕ) • mc

Tactic:
exact (nsmul_right_strictMono (by simpa using ha.ne.symm)).lt_iff_lt.mpr h

Premises used: Iff.mpr, StrictMono.lt_iff_lt, nsmul_right_strictMono
-- 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
ha : 0 < a
b c : ℚ≥0
h : b < c
mk :
  ∀ (m : M) (s : ℕ+) (ha : LT.lt (α := DivisibleHull M) 0 (DivisibleHull.mk m s)),
    HSMul.hSMul (β := DivisibleHull M) b (DivisibleHull.mk m s) <
      HSMul.hSMul (β := DivisibleHull M) c (DivisibleHull.mk m s)
⊢ b • a < c • 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
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : LT.lt (α := DivisibleHull M) 0 (DivisibleHull.mk m s)
mk : (c.den * (↑s : ℕ) * b.num) • m < (b.den * (↑s : ℕ) * c.num) • m
⊢ HSMul.hSMul (β := DivisibleHull M) b (DivisibleHull.mk m s) <
    HSMul.hSMul (β := DivisibleHull M) c (DivisibleHull.mk m s)

Tactic:
simp_rw [nnqsmul_mk, mk_lt_mk, smul_smul, PNat.mul_coe, PNat.mk_coe]

Premises used: smul_smul, PNat.mul_coe, DivisibleHull.mk_lt_mk, PNat.mk_coe, DivisibleHull.nnqsmul_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 : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : LT.lt (α := DivisibleHull M) 0 (mk m s)
⊢ (c.den * (↑s : ℕ) * b.num) • m < (b.den * (↑s : ℕ) * c.num) • m

Tactic:
smul_lt_smul_of_pos_right ?_ ?_

Premises used: smul_lt_smul_of_pos_right
-- 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 : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : LT.lt (α := DivisibleHull M) 0 (DivisibleHull.mk m s)
mk : c.den * (↑s : ℕ) * b.num < b.den * (↑s : ℕ) * c.num
mk₁ : 0 < m
⊢ (c.den * (↑s : ℕ) * b.num) • m < (b.den * (↑s : ℕ) * c.num) • m

Tactic:
refine smul_lt_smul_of_pos_right ?_ ?_

Premises used: smul_lt_smul_of_pos_right
-- 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 : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : LT.lt (α := DivisibleHull M) 0 (mk m s)
⊢ 0 < (↑s : ℕ)

Tactic:
simp