awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
m m' : M
s s' : ℕ+
⊢ (∃ (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:
rfl
-- Module: Mathlib.GroupTheory.DivisibleHull
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'
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))
⊢ Eq (α := DivisibleHull M) (mk p.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) p.2))
    (mk p'.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) p'.2))

Tactic:
obtain ⟨u, hu⟩ := heq
-- Module: Mathlib.GroupTheory.DivisibleHull
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 ℕ)
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:
mk_eq_mk.mpr ⟨↑ⁿ.symm u, hu⟩

Premises used: Iff.mpr, PNat.equivNonZeroDivisorsNat, OrderMonoidIso.symm, Exists.intro, DivisibleHull.mk_eq_mk, DFunLike.coe
-- Module: Mathlib.GroupTheory.DivisibleHull
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 ℕ)
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:
exact mk_eq_mk.mpr ⟨↑ⁿ.symm u, hu⟩

Premises used: Iff.mpr, PNat.equivNonZeroDivisorsNat, OrderMonoidIso.symm, Exists.intro, DivisibleHull.mk_eq_mk, DFunLike.coe
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
α : Type u_2
m : M
s : ℕ+
f : M → ℕ+ → α
h : ∀ (m m' : M) (s s' : ℕ+), Eq (α := DivisibleHull M) (mk m s) (mk m' s') → f m s = f m' s'
⊢ liftOn (mk m s) f h = f m s

Tactic:
rfl

Premises used: PNat.val, Set.Mem, setOf, LocalizedModule.liftOn, Set.inter, DivisibleHull.liftOn, Nat.lt, rfl, PNat
-- Module: Mathlib.GroupTheory.DivisibleHull
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'
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))
⊢ Eq (α := DivisibleHull M) (mk p.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) p.2))
    (mk p'.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) p'.2))

Tactic:
obtain ⟨u, hu⟩ := heq
-- Module: Mathlib.GroupTheory.DivisibleHull
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' : q ≈ q'
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:
mk_eq_mk.mpr ⟨↑ⁿ.symm u, hu⟩

Premises used: Iff.mpr, PNat.equivNonZeroDivisorsNat, OrderMonoidIso.symm, Exists.intro, DivisibleHull.mk_eq_mk, DFunLike.coe
-- Module: Mathlib.GroupTheory.DivisibleHull
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' : q ≈ q'
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:
exact mk_eq_mk.mpr ⟨↑ⁿ.symm u, hu⟩

Premises used: Iff.mpr, PNat.equivNonZeroDivisorsNat, OrderMonoidIso.symm, Exists.intro, DivisibleHull.mk_eq_mk, DFunLike.coe
-- Module: Mathlib.GroupTheory.DivisibleHull
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'
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))
⊢ Eq (α := DivisibleHull M) (mk q.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) q.2))
    (mk q'.1 ((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) q'.2))

Tactic:
obtain ⟨u, hu⟩ := heq'
-- Module: Mathlib.GroupTheory.DivisibleHull
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'
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:
mk_eq_mk.mpr ⟨↑ⁿ.symm u, hu⟩

Premises used: Iff.mpr, PNat.equivNonZeroDivisorsNat, OrderMonoidIso.symm, Exists.intro, DivisibleHull.mk_eq_mk, DFunLike.coe
-- Module: Mathlib.GroupTheory.DivisibleHull
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'
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:
exact mk_eq_mk.mpr ⟨↑ⁿ.symm u, hu⟩

Premises used: Iff.mpr, PNat.equivNonZeroDivisorsNat, OrderMonoidIso.symm, Exists.intro, DivisibleHull.mk_eq_mk, DFunLike.coe
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
α : Type u_2
m m' : M
s s' : ℕ+
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'
⊢ liftOn₂ (mk m s) (mk m' s') f h = f m s m' s'

Tactic:
rfl

Premises used: PNat.val, LocalizedModule.liftOn₂, Set.Mem, setOf, Set.inter, DivisibleHull.liftOn₂, Nat.lt, rfl, PNat
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
m1 m2 : M
s1 s2 : ℕ+
⊢ HAdd.hAdd (α := DivisibleHull M) (mk m1 s1) (mk m2 s2) = mk ((↑s2 : ℕ) • m1 + (↑s1 : ℕ) • m2) (s1 * s2)

Tactic:
LocalizedModule.mk_add_mk

Premises used: PNat.val, LocalizedModule.mk_add_mk, Set.Mem, setOf, Set.inter, DivisibleHull.mk, Nat.lt, PNat
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
m1 m2 : M
s : ℕ+
rw : ∃ (u : ℕ+), (↑u : ℕ) • (↑s : ℕ) • ((↑s : ℕ) • m1 + (↑s : ℕ) • m2) = (↑u : ℕ) • (↑(s * s) : ℕ) • (m1 + m2)
⊢ HAdd.hAdd (α := DivisibleHull M) (mk m1 s) (mk m2 s) = mk (m1 + m2) s

Tactic:
rw [mk_add_mk, mk_eq_mk]

Premises used: DivisibleHull.mk_add_mk, DivisibleHull.mk_eq_mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
m1 m2 : M
s : ℕ+
⊢ (↑1 : ℕ) • (↑s : ℕ) • ((↑s : ℕ) • m1 + (↑s : ℕ) • m2) = (↑1 : ℕ) • (↑(s * s) : ℕ) • (m1 + m2)

Tactic:
simp [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
m1 m2 : M
s : ℕ+
⊢ ∃ (u : ℕ+), (↑u : ℕ) • (↑s : ℕ) • ((↑s : ℕ) • m1 + (↑s : ℕ) • m2) = (↑u : ℕ) • (↑(s * s) : ℕ) • (m1 + m2)

Tactic:
exact ⟨1, by simp [smul_smul]⟩
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
m1 m2 : M
⊢ (↑(m1 + m2) : DivisibleHull M) = HAdd.hAdd (α := DivisibleHull M) (↑m1 : DivisibleHull M) (↑m2 : DivisibleHull M)

Tactic:
simp [mk_add_mk_left]

Premises used: DivisibleHull.mk_add_mk_left
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
⊢ Eq.{u_1 + 1} (α := DivisibleHull M) (↑0 : DivisibleHull M) 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
⊢ ∀ (x y : M),
    (↑(x + y) : DivisibleHull M) = HAdd.hAdd (α := DivisibleHull M) (↑x : DivisibleHull M) (↑y : DivisibleHull M)

Tactic:
simp
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
m : M
s : ℕ+
⊢ HSMul.hSMul (α := ℕ) (β := DivisibleHull M) 0 (mk m s) = mk (HSMul.hSMul (α := ℕ) 0 m) s

Tactic:
simp
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
m : M
s : ℕ+
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:
simp [add_nsmul, mk_add_mk_left, h]

Premises used: DivisibleHull.mk_add_mk_left, add_nsmul
-- Module: Mathlib.GroupTheory.DivisibleHull
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
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
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a • m) s

Tactic:
induction a with
  | zero => simp
  | succ n h => simp [add_nsmul, mk_add_mk_left, h]

Premises used: DivisibleHull.mk_add_mk_left, add_nsmul
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
a : ℚ≥0
m : M
s : ℕ+
⊢ Membership.mem (γ := Submonoid ℕ) (nonZeroDivisors ℕ) a.den

Tactic:
simp
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
a : ℚ≥0
m : M
s : ℕ+
h :
  a =
    IsLocalization.mk' ℚ≥0 a.num
      (Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Submonoid ℕ) (nonZeroDivisors ℕ) x) a.den ⋯)
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s)

Tactic:
convert! LocalizedModule.mk'_smul_mk ℚ≥0 a.num m ⟨a.den, by simp⟩ (↑ⁿ s)

Premises used: PNat.equivNonZeroDivisorsNat, NNRat, NNRat.num, Subtype.mk, NNRat.den, LocalizedModule.mk'_smul_mk, DFunLike.coe
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
a : ℚ≥0
m : M
s : ℕ+
⊢ a =
    IsLocalization.mk' ℚ≥0 a.num
      (Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Submonoid ℕ) (nonZeroDivisors ℕ) x) a.den ⋯)

Tactic:
simp [IsLocalization.eq_mk'_iff_mul_eq]

Premises used: IsLocalization.eq_mk'_iff_mul_eq
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsAddTorsionFree M
m m' : M
s s' : ℕ+
⊢ Eq (α := DivisibleHull M) (mk m s) (mk m' s') ↔ (↑s' : ℕ) • m = (↑s : ℕ) • m'

Tactic:
aesop (add simp [mk_eq_mk, nsmul_right_inj])

Premises used: nsmul_right_inj, DivisibleHull.mk_eq_mk
-- Module: Mathlib.GroupTheory.DivisibleHull
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)
⊢ (↑s : ℕ) • m = (↑s : ℕ) • n

Tactic:
simp_rw [mk_eq_mk_iff_smul_eq_smul] at h

Premises used: DivisibleHull.mk_eq_mk_iff_smul_eq_smul
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsAddTorsionFree M
s : ℕ+
m n : M
h : (↑s : ℕ) • m = (↑s : ℕ) • n
⊢ (↑s : ℕ) ≠ 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsAddTorsionFree M
s : ℕ+
m n : M
h : (↑s : ℕ) • m = (↑s : ℕ) • n
⊢ m = n

Tactic:
exact nsmul_right_injective (by simp) h

Premises used: nsmul_right_injective
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsAddTorsionFree M
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := M) (β := DivisibleHull M) coe

Tactic:
mk_left_injective 1

Premises used: DivisibleHull.mk_left_injective, OfNat.ofNat
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsAddTorsionFree M
m m' : M
⊢ Eq (α := DivisibleHull M) (↑m : DivisibleHull M) (↑m' : DivisibleHull M) ↔ m = m'

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, DivisibleHull.coe_injective
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
m : M
s : ℕ+
⊢ HAdd.hAdd (α := DivisibleHull M) (mk (-m) s) (mk m s) = 0

Tactic:
simp [mk_add_mk_left]

Premises used: DivisibleHull.mk_add_mk_left
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
x : DivisibleHull M
⊢ a • x =
    HSMul.hSMul (α := ℤ) (↑((SignType.sign : (a : ℚ) → SignType) a) : ℤ)
      (HSMul.hSMul (α := ℚ≥0)
        (have this := Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) |a| ⋯;
        this)
        x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
x : DivisibleHull M
⊢ HSMul.hSMul (α := ℚ) 0 x = 0

Tactic:
simp [qsmul_def]

Premises used: DivisibleHull.qsmul_def
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
h : 0 ≤ a
x : DivisibleHull M
⊢ 0 = a ∨ 0 < a

Tactic:
have := h.eq_or_lt
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
h : 0 ≤ a
x : DivisibleHull M
this : 0 = a ∨ 0 < a
⊢ a • x =
    HSMul.hSMul (α := ℚ≥0)
      (have this := Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a h;
      this)
      x

Tactic:
aesop (add simp [qsmul_def, abs_of_pos])

Premises used: DivisibleHull.qsmul_def, abs_of_pos
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
h : a ≤ 0
x : DivisibleHull M
⊢ a = 0 ∨ a < 0

Tactic:
have := h.eq_or_lt
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
h : a ≤ 0
x : DivisibleHull M
this : a = 0 ∨ a < 0
⊢ a • x =
    -HSMul.hSMul (α := ℚ≥0)
        (have this := Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (-a) ⋯;
        this)
        x

Tactic:
aesop (add simp [qsmul_def, abs_of_neg])

Premises used: abs_of_neg, DivisibleHull.qsmul_def
-- Module: Mathlib.GroupTheory.DivisibleHull
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)
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 ⋯ * s)
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s)

Tactic:
obtain h | h := le_total 0 a

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : 0 ≤ a
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))
          ⋯ *
        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)

Tactic:
rw [qsmul_of_nonneg h, nnqsmul_mk, ← natCast_zsmul]

Premises used: DivisibleHull.qsmul_of_nonneg, natCast_zsmul, DivisibleHull.nnqsmul_mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : 0 ≤ a
inl :
  (↑(NNRat.num
          (have this := Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a h;
          this)) :
      ℤ) =
    a.num
⊢ 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))

Tactic:
congr
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : 0 ≤ a
⊢ (↑(NNRat.num
          (have this := Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a h;
          this)) :
      ℤ) =
    a.num

Tactic:
simpa using h
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
inr :
  -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)
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk m s) = mk (a.num • m) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯ * s)

Tactic:
rw [qsmul_of_nonpos h]

Premises used: DivisibleHull.qsmul_of_nonpos
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
rw : HSMul.hSMul (α := ℤ) (↑a.num.natAbs : ℤ) m = -a.num • m
⊢ a.num.natAbs • m = -a.num • m

Tactic:
rw [← natCast_zsmul]

Premises used: natCast_zsmul
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
e_a : (↑a.num.natAbs : ℤ) = -a.num
⊢ HSMul.hSMul (α := ℤ) (↑a.num.natAbs : ℤ) m = -a.num • m

Tactic:
congr
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ (↑a.num.natAbs : ℤ) = -a.num

Tactic:
simpa using h
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ a.num.natAbs • m = -a.num • m

Tactic:
have : a.num.natAbs • m = -a.num • m := by
      rw [← natCast_zsmul]
      congr
      simpa using h
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
this : a.num.natAbs • m = -a.num • m
⊢ -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)

Tactic:
simp [nnqsmul_mk, this, ← neg_mk]

Premises used: DivisibleHull.neg_mk, 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 b : ℚ
x : DivisibleHull M
mk :
  ∀ (m : M) (s : ℕ+),
    HSMul.hSMul (β := DivisibleHull M) (a * b) (DivisibleHull.mk m s) =
      a • HSMul.hSMul (β := DivisibleHull M) b (DivisibleHull.mk m s)
⊢ (a * b) • x = a • 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 ⋯ * (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
⊢ HSMul.hSMul (β := DivisibleHull M) (a * b) (DivisibleHull.mk m s) =
    a • HSMul.hSMul (β := DivisibleHull M) b (DivisibleHull.mk m s)

Tactic:
simp_rw [qsmul_mk, mk_eq_mk]

Premises used: 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 ⋯ * (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
⊢ ∃ (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

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 : ℤ) * (↑(↑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:
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 : ℤ) * (↑(↑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
h₁ :
  (↑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
⊢ (↑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:
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 : ℤ) * (↑(↑s : ℕ) : ℤ)) • m =
    (a.num * b.num * (↑(a * b).den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m
h :
  ((↑a.den : ℤ) * HMul.hMul (α := ℤ) (↑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 =
    ((a * b).num * (↑a.den : ℤ) * (↑b.den : ℤ) * (↑(↑s : ℕ) : ℤ)) • m

Tactic:
simp [← natCast_zsmul, smul_smul]

Premises used: smul_smul, natCast_zsmul