awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Divisible (goal)
Goal:
A : Type u_1
B : Type u_2
α : Type u_3
inst : Zero α
inst_1 : Monoid A
inst_2 : Monoid B
inst_3 : Pow A α
inst_4 : Pow B α
inst_5 : RootableBy A α
f : A → B
hf : Surjective f
hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n
n : α
hn : n ≠ 0
x : B
y : A
hy : f y = x
rw : f (@RootableBy.root _ _ inst_1 inst_3 inst _ y n ^ n) = x
rw₁ : f y = x
⊢ f (@RootableBy.root _ _ inst_1 inst_3 inst _ y n) ^ n = x
have rw₂ : x = x
Tactic: rw [← hpow (RootableBy.root y n) n, RootableBy.root_cancel _ hn, hy]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
m m' : M
s s' : ℕ+
⊢ Eq (α := DivisibleHull M) (LocalizedModule.mk m ((↑ⁿ : (a : ℕ+) → ↥(nonZeroDivisors ℕ)) s))
      (LocalizedModule.mk m' ((↑ⁿ : (a : ℕ+) → ↥(nonZeroDivisors ℕ)) s')) ↔
    ∃ (u : ℕ+), (↑u : ℕ) • (↑s' : ℕ) • m = (↑u : ℕ) • (↑s : ℕ) • m'
have rw : (∃ (u : ↥(nonZeroDivisors ℕ)),
    u • HSMul.hSMul (α := ↥(nonZeroDivisors ℕ)) ((↑ⁿ : (a : ℕ+) → ↥(nonZeroDivisors ℕ)) s' : ↥(nonZeroDivisors ℕ)) m =
      u •
        HSMul.hSMul (α := ↥(nonZeroDivisors ℕ)) ((↑ⁿ : (a : ℕ+) → ↥(nonZeroDivisors ℕ)) s : ↥(nonZeroDivisors ℕ)) m') ↔
  ∃ (b : ↥(nonZeroDivisors ℕ)),
    (↑((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) b) : ℕ) • (↑s' : ℕ) • m =
      (↑((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) b) : ℕ) • (↑s : ℕ) • m'
Tactic: rw [LocalizedModule.mk_eq, ↑ⁿ.exists_congr_left]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
α : Type u_2
x : DivisibleHull M
f : M → ℕ+ → α
h : ∀ (m m' : M) (s s' : ℕ+), Eq (α := DivisibleHull M) (mk m s) (mk m' s') → f m s = f m' s'
p p' : M × ↥(nonZeroDivisors ℕ)
heq : p ≈ p'
⊢ Eq (α := DivisibleHull M) (mk p.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) p.2))
    (mk p'.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) p'.2))
have obtain : ∀ (u : ↥(nonZeroDivisors ℕ)) (hu : u • p'.2 • p.1 = u • p.2 • p'.1),
  Eq (α := DivisibleHull M) (mk p.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) p.2))
    (mk p'.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) p'.2))
Tactic: obtain ⟨u, hu⟩ := heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
α : Type u_2
x y : DivisibleHull M
f : M → ℕ+ → M → ℕ+ → α
h :
  ∀ (m n m' n' : M) (s t s' t' : ℕ+),
    Eq (α := DivisibleHull M) (mk m s) (mk m' s') →
      Eq (α := DivisibleHull M) (mk n t) (mk n' t') → f m s n t = f m' s' n' t'
p q p' q' : M × ↥(nonZeroDivisors ℕ)
heq : p ≈ p'
heq' : q ≈ q'
⊢ Eq (α := DivisibleHull M) (mk p.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) p.2))
    (mk p'.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) p'.2))
have obtain : ∀ (u : ↥(nonZeroDivisors ℕ)) (hu : u • p'.2 • p.1 = u • p.2 • p'.1),
  Eq (α := DivisibleHull M) (mk p.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) p.2))
    (mk p'.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) p'.2))
Tactic: obtain ⟨u, hu⟩ := heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
α : Type u_2
x y : DivisibleHull M
f : M → ℕ+ → M → ℕ+ → α
h :
  ∀ (m n m' n' : M) (s t s' t' : ℕ+),
    Eq (α := DivisibleHull M) (mk m s) (mk m' s') →
      Eq (α := DivisibleHull M) (mk n t) (mk n' t') → f m s n t = f m' s' n' t'
p q p' q' : M × ↥(nonZeroDivisors ℕ)
heq : p ≈ p'
heq' : q ≈ q'
⊢ Eq (α := DivisibleHull M) (mk q.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) q.2))
    (mk q'.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) q'.2))
have obtain : ∀ (u : ↥(nonZeroDivisors ℕ)) (hu : u • q'.2 • q.1 = u • q.2 • q'.1),
  Eq (α := DivisibleHull M) (mk q.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) q.2))
    (mk q'.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) q'.2))
Tactic: obtain ⟨u, hu⟩ := heq'
Cleared hypotheses: heq'
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
m1 m2 : M
s : ℕ+
⊢ HAdd.hAdd (α := DivisibleHull M) (mk m1 s) (mk m2 s) = mk (m1 + m2) s
have rw : ∃ (u : ℕ+), (↑u : ℕ) • (↑s : ℕ) • ((↑s : ℕ) • m1 + (↑s : ℕ) • m2) = (↑u : ℕ) • (↑(s * s) : ℕ) • (m1 + m2)
Tactic: rw [mk_add_mk, mk_eq_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a : ℕ
m : M
s : ℕ+
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a • m) s
have zero : HSMul.hSMul (α := ℕ) (β := DivisibleHull M) 0 (mk m s) = mk (HSMul.hSMul (α := ℕ) 0 m) s
Tactic: induction a with
  | zero => simp
  | succ n h => simp [add_nsmul, mk_add_mk_left, h]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a : ℕ
m : M
s : ℕ+
zero : HSMul.hSMul (α := ℕ) (β := DivisibleHull M) 0 (mk m s) = mk (HSMul.hSMul (α := ℕ) 0 m) s
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a • m) s
have succ : ∀ (n : ℕ) (h : HSMul.hSMul (β := DivisibleHull M) n (mk m s) = mk (n • m) s),
  HSMul.hSMul (β := DivisibleHull M) (n + 1) (mk m s) = mk ((n + 1) • m) s
Tactic: induction a with
  | zero => simp
  | succ n h => simp [add_nsmul, mk_add_mk_left, h]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a : ℚ≥0
m : M
s : ℕ+
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s)
have h : a =
  IsLocalization.mk' ℚ≥0 a.num
    (Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Submonoid ℕ) (nonZeroDivisors ℕ) x) a.den sorry)
Tactic: convert! LocalizedModule.mk'_smul_mk ℚ≥0 a.num m ⟨a.den, by simp⟩ (↑ⁿ s)
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsAddTorsionFree M
s : ℕ+
m n : M
h :
  Eq.{u_1 + 1} (α := DivisibleHull M) ((fun (m : M) ↦ (mk m s : DivisibleHull M)) m)
    ((fun (m : M) ↦ (mk m s : DivisibleHull M)) n)
⊢ m = n
have h₁ : (↑s : ℕ) • m = (↑s : ℕ) • n
Tactic: simp_rw [mk_eq_mk_iff_smul_eq_smul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (hypothesis)
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
h : 0 ≤ a
x : DivisibleHull M
⊢ a • x =
    HSMul.hSMul (α := ℚ≥0)
      (have this := Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a h;
      this)
      x
have this : 0 = a ∨ 0 < a
Tactic: have := h.eq_or_lt
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (hypothesis)
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
h : a ≤ 0
x : DivisibleHull M
⊢ a • x =
    -HSMul.hSMul (α := ℚ≥0)
        (have this := Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (-a) ⋯;
        this)
        x
have this : a = 0 ∨ a < 0
Tactic: have := h.eq_or_lt
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s)
have inl : ∀ (h : 0 ≤ a),
  HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry * s)
Tactic: obtain h | h := le_total 0 a
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
inl :
  ∀ (h : 0 ≤ a),
    HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s)
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s)
have inr : ∀ (h : a ≤ 0),
  HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry * s)
Tactic: obtain h | h := le_total 0 a
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : 0 ≤ a
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s)
have inl : Eq (α := DivisibleHull M)
  (mk
    (HSMul.hSMul (α := ℤ)
      (↑(NNRat.num
            (have this := Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a h;
            this)) :
        ℤ)
      m)
    (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n)
        (NNRat.den
          (have this := Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a h;
          this))
        sorry *
      s))
  (mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry * s))
Tactic: rw [qsmul_of_nonneg h, nnqsmul_mk, ← natCast_zsmul]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : 0 ≤ a
⊢ Eq (α := DivisibleHull M)
    (mk
      (HSMul.hSMul (α := ℤ)
        (↑(NNRat.num
              (have this := Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a h;
              this)) :
          ℤ)
        m)
      (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n)
          (NNRat.den
            (have this := Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a h;
            this))
          ⋯ *
        s))
    (mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s))
have inl : (↑(NNRat.num
        (have this := Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a h;
        this)) :
    ℤ) =
  a.num
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s)
have inr : -HSMul.hSMul (α := ℚ≥0) (β := DivisibleHull M)
      (have this := Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (-a) sorry;
      this)
      (mk m s) =
  mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry * s)
Tactic: rw [qsmul_of_nonpos h]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ a.num.natAbs • m = -a.num • m
have rw : HSMul.hSMul (α := ℤ) (↑a.num.natAbs : ℤ) m = -a.num • m
Tactic: rw [← natCast_zsmul]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ HSMul.hSMul (α := ℤ) (↑a.num.natAbs : ℤ) m = -a.num • m
have e_a : (↑a.num.natAbs : ℤ) = -a.num
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (hypothesis)
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ -HSMul.hSMul (α := ℚ≥0) (β := DivisibleHull M)
        (have this := Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (-a) ⋯;
        this)
        (mk m s) =
    mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s)
have this : a.num.natAbs • m = -a.num • m
Tactic: have : a.num.natAbs • m = -a.num • m := by
      rw [← natCast_zsmul]
      congr
      simpa using 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 : AddCommGroup M
a b : ℚ
x : DivisibleHull M
⊢ (a * b) • x = a • b • x
have mk : ∀ (m : M) (s : ℕ+),
  HSMul.hSMul (β := DivisibleHull M) (a * b) (mk m s) = a • HSMul.hSMul (β := DivisibleHull M) b (mk m s)
Tactic: induction x with | mk m s
Cleared hypotheses: x
-- 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 : ℕ+
⊢ HSMul.hSMul (β := DivisibleHull M) (a * b) (mk m s) = a • HSMul.hSMul (β := DivisibleHull M) b (mk m s)
have mk : ∃ (u : ℕ+),
  (↑u : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den sorry * s)) : ℕ) •
        (a * b).num • m =
    (↑u : ℕ) • (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a * b).den sorry * s) : ℕ) • a.num • b.num • m
Tactic: simp_rw [qsmul_mk, mk_eq_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 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ ∃ (u : ℕ+),
    (↑u : ℕ) •
        (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * (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) : ℕ) • a.num • b.num • m
have h : (↑1 : ℕ) •
    (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den sorry * s)) : ℕ) •
      (a * b).num • m =
  (↑1 : ℕ) • (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a * b).den sorry * s) : ℕ) • a.num • b.num • m
Tactic: use 1
-- 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 : ℤ) * (↑(↑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
have h : (↑1 : ℕ) •
    (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den sorry * s)) : ℕ) •
      (a * b).num • m =
  ((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
Tactic: convert! this using 1
-- 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 : ℤ) * (↑(↑s : ℕ) : ℤ)) • m =
    (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
h :
  (↑1 : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den ⋯ * s)) : ℕ) •
        (a * b).num • m =
    ((a * b).num * (↑a.den : ℤ) * (↑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
have h₁ : (↑1 : ℕ) • (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a * b).den sorry * s) : ℕ) • a.num • b.num • m =
  (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
Tactic: convert! this using 1
-- 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 : ℤ) * (↑(↑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 =
    ((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
have h : ((↑a.den : ℤ) * HMul.hMul (α := ℤ) (↑b.den : ℤ) (↑(↑s : ℕ) : ℤ) * (a * b).num) • m =
  ((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
Tactic: simp [← natCast_zsmul, 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 : 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
⊢ (↑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
have h : (HMul.hMul (α := ℤ) (↑(a * b).den : ℤ) (↑(↑s : ℕ) : ℤ) * (a.num * b.num)) • m =
  (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
Tactic: simp [← natCast_zsmul, 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 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ (↑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
have h : ((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m =
  (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • 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
-- 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 : ℤ) * (↑(↑s : ℕ) : ℤ)) • m =
    (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
have h : (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m = (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
Tactic: rw [Rat.mul_num_den']
-- 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
x : DivisibleHull M
⊢ HSMul.hSMul (α := ℚ) 1 x = x
have mk : ∀ (m : M) (s : ℕ+), HSMul.hSMul (α := ℚ) (β := DivisibleHull M) 1 (mk m s) = mk m s
Tactic: induction x with | mk m s
Cleared hypotheses: x
-- 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 : ℚ
x : DivisibleHull M
⊢ (a + b) • x = a • x + b • x
have mk : ∀ (m : M) (s : ℕ+),
  HSMul.hSMul (β := DivisibleHull M) (a + b) (mk m s) =
    HSMul.hSMul (β := DivisibleHull M) a (mk m s) + HSMul.hSMul (β := DivisibleHull M) b (mk m s)
Tactic: induction x with | mk m s
Cleared hypotheses: x
-- 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 : ℕ+
⊢ HSMul.hSMul (β := DivisibleHull M) (a + b) (mk m s) =
    HSMul.hSMul (β := DivisibleHull M) a (mk m s) + HSMul.hSMul (β := DivisibleHull M) b (mk m s)
have mk : ∃ (u : ℕ+),
  (↑u : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry * s * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den sorry * s)) : ℕ) •
        (a + b).num • m =
    (↑u : ℕ) •
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a + b).den sorry * s) : ℕ) •
        ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den sorry * s) : ℕ) • a.num • m +
          (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry * s) : ℕ) • b.num • m)
Tactic: simp_rw [qsmul_mk, mk_add_mk, mk_eq_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 : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ ∃ (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)
have h : (↑1 : ℕ) •
    (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry * s * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den sorry * s)) : ℕ) •
      (a + b).num • m =
  (↑1 : ℕ) •
    (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a + b).den sorry * s) : ℕ) •
      ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den sorry * s) : ℕ) • a.num • m +
        (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry * s) : ℕ) • b.num • m)
Tactic: use 1
-- 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.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 : (↑1 : ℕ) •
    (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry * s * (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den sorry * s)) : ℕ) •
      (a + b).num • m =
  ((a + b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) • m
Tactic: convert! this using 1
-- 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
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
⊢ (↑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₁ : (↑1 : ℕ) •
    (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (a + b).den sorry * s) : ℕ) •
      ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) b.den sorry * s) : ℕ) • a.num • m +
        (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry * s) : ℕ) • b.num • m) =
  ((a.num * (↑b.den : ℤ) + b.num * (↑a.den : ℤ)) * (↑(a + b).den : ℤ) *
      HMul.hMul (α := ℤ) (↑(↑s : ℕ) : ℤ) (↑(↑s : ℕ) : ℤ)) •
    m
Tactic: convert! this using 1
-- 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.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
have 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
Tactic: simp [← natCast_zsmul, smul_smul, ← add_smul]