awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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
⊢ (↑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
have 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
Tactic: simp [← natCast_zsmul, smul_smul, ← add_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ (↑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)
have 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
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
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ ((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
have 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
Tactic: rw [Rat.add_num_den']
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (hypothesis)
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')
⊢ ((↑t : ℕ) • m ≤ (↑s : ℕ) • n) = ((↑t' : ℕ) • m' ≤ (↑s' : ℕ) • n')
have h₁ : (↑s' : ℕ) • m = (↑s : ℕ) • m'
Tactic: rw [mk_eq_mk_iff_smul_eq_smul] at h h'
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (hypothesis)
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 : ℕ) • m ≤ (↑s : ℕ) • n) = ((↑t' : ℕ) • m' ≤ (↑s' : ℕ) • n')
have h'₁ : (↑t' : ℕ) • n = (↑t : ℕ) • n'
Tactic: rw [mk_eq_mk_iff_smul_eq_smul] at h h'
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 : ℕ) • m ≤ (↑s : ℕ) • n) = ((↑t' : ℕ) • m' ≤ (↑s' : ℕ) • n')
have rw : ((↑s' : ℕ) * (↑t' : ℕ)) • (↑t : ℕ) • m ≤ ((↑s' : ℕ) * (↑t' : ℕ)) • (↑s : ℕ) • n ↔ (↑t' : ℕ) • m' ≤ (↑s' : ℕ) • n'
Tactic: rw [propext_iff, ← nsmul_le_nsmul_iff_right (mul_ne_zero s'.ne_zero t'.ne_zero)]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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'
have h₁ : ((↑s' : ℕ) * (↑t' : ℕ)) • (↑t : ℕ) • m = ((↑s : ℕ) * (↑t : ℕ)) • (↑t' : ℕ) • m'
Tactic: convert! (nsmul_le_nsmul_iff_right (M := M) (mul_ne_zero s.ne_zero t.ne_zero)) using 2
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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'
⊢ ((↑s' : ℕ) * (↑t' : ℕ)) • (↑t : ℕ) • m ≤ ((↑s' : ℕ) * (↑t' : ℕ)) • (↑s : ℕ) • n ↔ (↑t' : ℕ) • m' ≤ (↑s' : ℕ) • n'
have h₂ : ((↑s' : ℕ) * (↑t' : ℕ)) • (↑s : ℕ) • n = ((↑s : ℕ) * (↑t : ℕ)) • (↑s' : ℕ) • n'
Tactic: convert! (nsmul_le_nsmul_iff_right (M := M) (mul_ne_zero s.ne_zero t.ne_zero)) using 2
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 : ℕ)) • (↑t' : ℕ) • m'
have h₁ : ((↑t' : ℕ) * ((↑t : ℕ) * (↑s : ℕ))) • m' = ((↑s : ℕ) * ((↑t : ℕ) * (↑t' : ℕ))) • m'
Tactic: simp_rw [smul_smul, mul_rotate s'.val, ← smul_smul, h, smul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 : ℕ) * (↑t : ℕ)) • (↑s' : ℕ) • n'
have h₁ : ((↑s' : ℕ) * ((↑t' : ℕ) * (↑s : ℕ))) • n = ((↑s' : ℕ) * ((↑s : ℕ) * (↑t' : ℕ))) • n
Tactic: simp_rw [smul_smul, ← mul_rotate s'.val, ← smul_smul, ← h', smul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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
⊢ a ≤ a
have mk : ∀ (m : M) (s : ℕ+), LE.le (α := DivisibleHull M) (mk m s) (mk m s)
Tactic: induction a with | mk m s
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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
⊢ a ≤ c
have mk : ∀ (ma : M) (sa : ℕ+) (hab : mk ma sa ≤ b), mk ma sa ≤ c
Tactic: induction a with | mk ma sa
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 : mk ma sa ≤ b
⊢ mk ma sa ≤ c
have mk : ∀ (mb : M) (sb : ℕ+) (hbc : mk mb sb ≤ c) (hab : LE.le (α := DivisibleHull M) (mk ma sa) (mk mb sb)), mk ma sa ≤ c
Tactic: induction b with | mk mb sb
Cleared hypotheses: b, hbc, hab
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 : mk mb sb ≤ c
hab : LE.le (α := DivisibleHull M) (mk ma sa) (mk mb sb)
⊢ mk ma sa ≤ c
have mk : ∀ (mc : M) (sc : ℕ+) (hbc : LE.le (α := DivisibleHull M) (mk mb sb) (mk mc sc)),
  LE.le (α := DivisibleHull M) (mk ma sa) (mk mc sc)
Tactic: induction c with | mk mc sc
Cleared hypotheses: c, hbc
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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) (mk ma sa) (mk mb sb)
mc : M
sc : ℕ+
hbc : LE.le (α := DivisibleHull M) (mk mb sb) (mk mc sc)
⊢ LE.le (α := DivisibleHull M) (mk ma sa) (mk mc sc)
have mk : ∀ (hab : (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb) (mc : M) (sc : ℕ+) (hbc : (↑sc : ℕ) • mb ≤ (↑sb : ℕ) • mc),
  (↑sc : ℕ) • ma ≤ (↑sa : ℕ) • mc
Tactic: rw [mk_le_mk] at ⊢ hab hbc
Cleared hypotheses: hab, mc, sc, hbc
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 : ℕ) • ma ≤ (↑sa : ℕ) • mc
have mk : (↑sc : ℕ) • (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • (↑sb : ℕ) • mc
Tactic: rw [← nsmul_le_nsmul_iff_right (show sb.val ≠ 0 by simp), smul_comm _ _ ma, smul_comm _ _ mc]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (hypothesis)
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 : ℕ) • (↑sb : ℕ) • mc
have hab₁ : (↑sc : ℕ) • (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • (↑sc : ℕ) • mb
Tactic: rw [← nsmul_le_nsmul_iff_right (show sc.val ≠ 0 by simp), smul_comm _ _ mb] at hab
Cleared hypotheses: hab, hbc
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (hypothesis)
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
⊢ (↑sc : ℕ) • (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • (↑sb : ℕ) • mc
have hbc₁ : (↑sa : ℕ) • (↑sc : ℕ) • mb ≤ (↑sa : ℕ) • (↑sb : ℕ) • mc
Tactic: rw [← nsmul_le_nsmul_iff_right (show sa.val ≠ 0 by simp)] at hbc
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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
⊢ a = b
have mk : ∀ (ma : M) (sa : ℕ+) (h : mk ma sa ≤ b) (h' : b ≤ mk ma sa), mk ma sa = b
Tactic: induction a with | mk ma sa
Cleared hypotheses: a, h, h'
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 : mk ma sa ≤ b
h' : b ≤ mk ma sa
⊢ mk ma sa = b
have mk : ∀ (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)), Eq (α := DivisibleHull M) (mk ma sa) (mk mb sb)
Tactic: induction b with | mk mb sb
Cleared hypotheses: b, h, h'
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (hypothesis)
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)
⊢ Eq (α := DivisibleHull M) (mk ma sa) (mk mb sb)
have h₁ : (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb
Tactic: rw [mk_le_mk] at h h'
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (hypothesis)
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
⊢ Eq (α := DivisibleHull M) (mk ma sa) (mk mb sb)
have h'₁ : (↑sa : ℕ) • mb ≤ (↑sb : ℕ) • ma
Tactic: rw [mk_le_mk] at h h'
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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
⊢ Eq (α := DivisibleHull M) (mk ma sa) (mk mb sb)
have mk : (↑sb : ℕ) • ma = (↑sa : ℕ) • mb
Tactic: rw [mk_eq_mk_iff_smul_eq_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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
⊢ a ≤ b ∨ b ≤ a
have mk : ∀ (ma : M) (sa : ℕ+), mk ma sa ≤ b ∨ b ≤ mk ma sa
Tactic: induction a with | mk ma sa
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 ma sa ≤ b ∨ b ≤ mk ma sa
have mk : ∀ (mb : M) (sb : ℕ+),
  LE.le (α := DivisibleHull M) (mk ma sa) (mk mb sb) ∨ LE.le (α := DivisibleHull M) (mk mb sb) (mk ma sa)
Tactic: induction b with | mk mb sb
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 : ℕ+
⊢ LE.le (α := DivisibleHull M) (mk ma sa) (mk mb sb) ∨ LE.le (α := DivisibleHull M) (mk mb sb) (mk ma sa)
have mk : (↑sb : ℕ) • ma ≤ (↑sa : ℕ) • mb ∨ (↑sa : ℕ) • mb ≤ (↑sb : ℕ) • ma
Tactic: simp_rw [mk_le_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_2
inst : AddCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedCancelAddMonoid M
m m' : M
s s' : ℕ+
⊢ LT.lt (α := DivisibleHull M) (mk m s) (mk m' s') ↔ (↑s' : ℕ) • m < (↑s : ℕ) • m'
have simp_rw : ¬LE.le (α := DivisibleHull M) (mk m' s') (mk m s) ↔ ¬(↑s : ℕ) • m' ≤ (↑s' : ℕ) • m
Tactic: simp_rw [lt_iff_not_ge, mk_le_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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
⊢ a + b < a + c
have mk : ∀ (ma : M) (sa : ℕ+), mk ma sa + b < mk ma sa + c
Tactic: induction a with | mk ma sa
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 ma sa + b < mk ma sa + c
have mk : ∀ (mb : M) (sb : ℕ+) (h : mk mb sb < c), HAdd.hAdd (α := DivisibleHull M) (mk ma sa) (mk mb sb) < mk ma sa + c
Tactic: induction b with | mk mb sb
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 : mk mb sb < c
⊢ HAdd.hAdd (α := DivisibleHull M) (mk ma sa) (mk mb sb) < mk ma sa + c
have mk : ∀ (mc : M) (sc : ℕ+) (h : LT.lt (α := DivisibleHull M) (mk mb sb) (mk mc sc)),
  HAdd.hAdd (α := DivisibleHull M) (mk ma sa) (mk mb sb) < HAdd.hAdd (α := DivisibleHull M) (mk ma sa) (mk mc sc)
Tactic: induction c with | mk mc sc
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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) (mk mb sb) (mk mc sc)
⊢ HAdd.hAdd (α := DivisibleHull M) (mk ma sa) (mk mb sb) < HAdd.hAdd (α := DivisibleHull M) (mk ma sa) (mk mc sc)
have mk : LT.lt (α := DivisibleHull M) (mk ((↑sb : ℕ) • ma + (↑sa : ℕ) • mb) (sa * sb))
  (mk ((↑sc : ℕ) • ma + (↑sa : ℕ) • mc) (sa * sc))
Tactic: simp_rw [mk_add_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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) (mk mb sb) (mk mc sc)
⊢ LT.lt (α := DivisibleHull M) (mk ((↑sb : ℕ) • ma + (↑sa : ℕ) • mb) (sa * sb))
    (mk ((↑sc : ℕ) • ma + (↑sa : ℕ) • mc) (sa * sc))
have mk : ∀ (h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc),
  (↑(sa * sc) : ℕ) • ((↑sb : ℕ) • ma + (↑sa : ℕ) • mb) < (↑(sa * sb) : ℕ) • ((↑sc : ℕ) • ma + (↑sa : ℕ) • mc)
Tactic: rw [mk_lt_mk] at ⊢ h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 * sc) : ℕ) • ((↑sb : ℕ) • ma + (↑sa : ℕ) • mb) < (↑(sa * sb) : ℕ) • ((↑sc : ℕ) • ma + (↑sa : ℕ) • mc)
have mk : ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sb : ℕ))) • ma + ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sa : ℕ))) • mb <
  ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sc : ℕ))) • ma + ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sa : ℕ))) • mc
Tactic: simp_rw [PNat.mul_coe, mul_smul, smul_add, smul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (hypothesis)
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 : ℕ) * ((↑sc : ℕ) * (↑sb : ℕ))) • ma + ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sa : ℕ))) • mb <
    ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sc : ℕ))) • ma + ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sa : ℕ))) • mc
have this : ((↑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)
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (hypothesis)
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 : ℕ))) • ma + ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sa : ℕ))) • mb <
    ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sc : ℕ))) • ma + ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sa : ℕ))) • mc
have this₁ : ((↑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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 : ℕ))) • ma + ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sa : ℕ))) • mb <
    ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sc : ℕ))) • ma + ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sa : ℕ))) • mc
have h₁ : (↑sa : ℕ) * ((↑sc : ℕ) * (↑sb : ℕ)) = (↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)
Tactic: convert! this using 3
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 : ℕ)
⊢ ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sb : ℕ))) • ma + ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sa : ℕ))) • mb <
    ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sc : ℕ))) • ma + ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sa : ℕ))) • mc
have h₂ : (↑sa : ℕ) * ((↑sc : ℕ) * (↑sa : ℕ)) = (↑sa : ℕ) * (↑sa : ℕ) * (↑sc : ℕ)
Tactic: convert! this using 3
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 : ℕ)
⊢ ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sb : ℕ))) • ma + ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sa : ℕ))) • mb <
    ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sc : ℕ))) • ma + ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sa : ℕ))) • mc
have h₃ : (↑sa : ℕ) * ((↑sb : ℕ) * (↑sc : ℕ)) = (↑sa : ℕ) * (↑sb : ℕ) * (↑sc : ℕ)
Tactic: convert! this using 3
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 : ℕ)
⊢ ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sb : ℕ))) • ma + ((↑sa : ℕ) * ((↑sc : ℕ) * (↑sa : ℕ))) • mb <
    ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sc : ℕ))) • ma + ((↑sa : ℕ) * ((↑sb : ℕ) * (↑sa : ℕ))) • mc
have h₄ : (↑sa : ℕ) * ((↑sb : ℕ) * (↑sa : ℕ)) = (↑sa : ℕ) * (↑sa : ℕ) * (↑sb : ℕ)
Tactic: convert! this using 3
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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
⊢ a • b < a • c
have mk : ∀ (mb : M) (sb : ℕ+) (h : mk mb sb < c), HSMul.hSMul (β := DivisibleHull M) a (mk mb sb) < a • c
Tactic: induction b with | mk mb sb
Cleared hypotheses: b, h