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

Tactic:
convert! mul_lt_mul_of_pos_right (NNRat.lt_def.mp h) (show 0 < s.val by simp) using 1

Premises used: NNRat.lt_def, mul_lt_mul_of_pos_right, Iff.mp
-- 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 = b.num * c.den * (↑s : ℕ)

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

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

Tactic:
rw [← mk_zero 1, mk_lt_mk] at ha

Premises used: DivisibleHull.mk_lt_mk, DivisibleHull.mk_zero, OfNat.ofNat
-- 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 : HSMul.hSMul (β := M) (↑s : ℕ) 0 < (↑1 : ℕ) • m
⊢ 0 < m

Tactic:
simpa using ha
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : ℚ
ha : 0 < a
b c : DivisibleHull M
h : b < c
simp_rw : Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a ⋯ • b < Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a ⋯ • c
⊢ a • b < a • c

Tactic:
simp_rw [qsmul_of_nonneg ha.le]

Premises used: LT.lt.le, DivisibleHull.qsmul_of_nonneg
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : ℚ
ha : 0 < a
b c : DivisibleHull M
h : b < c
⊢ 0 < Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a ⋯

Tactic:
simpa using ha
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : ℚ
ha : 0 < a
b c : DivisibleHull M
h : b < c
⊢ Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a ⋯ • b < Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a ⋯ • c

Tactic:
apply smul_lt_smul_of_pos_left h (by simpa using ha)

Premises used: smul_lt_smul_of_pos_left
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
a₁ : 0 < c • a - b • a
⊢ b • a < c • a

Tactic:
apply lt_of_sub_pos

Premises used: lt_of_sub_pos
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
a₁ : 0 < (c - b) • a
⊢ 0 < c • a - b • a

Tactic:
rw [← sub_smul]

Premises used: sub_smul
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
a₁ : 0 < Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (c - b) ⋯ • a
⊢ 0 < (c - b) • a

Tactic:
simp_rw [qsmul_of_nonneg (sub_pos_of_lt h).le]

Premises used: LT.lt.le, DivisibleHull.qsmul_of_nonneg, sub_pos_of_lt
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
⊢ 0 < Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (c - b) ⋯

Tactic:
simpa [← NNRat.coe_pos] using h

Premises used: NNRat.coe_pos
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
⊢ 0 < Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (c - b) ⋯ • a

Tactic:
apply smul_pos (by simpa [← NNRat.coe_pos] using h) ha

Premises used: smul_pos
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a b : M
h : a ≤ b
⊢ LE.le (α := DivisibleHull M) (ZeroHom.toFun (↑(coeAddMonoidHom M) : ZeroHom M (DivisibleHull M)) a)
    (ZeroHom.toFun (↑(coeAddMonoidHom M) : ZeroHom M (DivisibleHull M)) b)

Tactic:
simpa using h
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this :
  HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s : ℕ) : ℤ) (mk m s) =
    HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s' : ℕ) : ℤ) (mk m s')
⊢ Eq (α := ArchimedeanClass (DivisibleHull M))
    (ArchimedeanClass.mk (HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s : ℕ) : ℤ) (mk m s)))
    (ArchimedeanClass.mk (HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s' : ℕ) : ℤ) (mk m s')))

Tactic:
apply_fun ArchimedeanClass.mk at this

Premises used: ArchimedeanClass.mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this :
  Eq (α := ArchimedeanClass (DivisibleHull M))
    (ArchimedeanClass.mk (HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s : ℕ) : ℤ) (mk m s)))
    (ArchimedeanClass.mk (HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s' : ℕ) : ℤ) (mk m s')))
⊢ Ne (α := ℤ) (↑(↑s : ℕ) : ℤ) 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this :
  Eq (α := ArchimedeanClass (DivisibleHull M))
    (ArchimedeanClass.mk (HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s : ℕ) : ℤ) (mk m s)))
    (ArchimedeanClass.mk (HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s' : ℕ) : ℤ) (mk m s')))
⊢ Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m s))
    (ArchimedeanClass.mk (HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s' : ℕ) : ℤ) (mk m s')))

Tactic:
rw [ArchimedeanClass.mk_smul _ (by simp)] at this

Premises used: ArchimedeanClass.mk_smul
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this :
  Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m s))
    (ArchimedeanClass.mk (HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s' : ℕ) : ℤ) (mk m s')))
⊢ Ne (α := ℤ) (↑(↑s' : ℕ) : ℤ) 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this :
  Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m s))
    (ArchimedeanClass.mk (HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s' : ℕ) : ℤ) (mk m s')))
⊢ Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m s)) (ArchimedeanClass.mk (mk m s'))

Tactic:
rw [ArchimedeanClass.mk_smul _ (by simp)] at this

Premises used: ArchimedeanClass.mk_smul
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this : Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m s)) (ArchimedeanClass.mk (mk m s'))
⊢ Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m s)) (ArchimedeanClass.mk (mk m s'))

Tactic:
this
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this : Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m s)) (ArchimedeanClass.mk (mk m s'))
⊢ Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m s)) (ArchimedeanClass.mk (mk m s'))

Tactic:
exact this
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
m : M
s s' : ℕ+
suffices :
  HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s : ℕ) : ℤ) (mk m s) =
    HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s' : ℕ) : ℤ) (mk m s')
⊢ Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m s)) (ArchimedeanClass.mk (mk m s'))

Tactic:
suffices (s : ℤ) • mk m s = (s' : ℤ) • mk m s' by
    apply_fun ArchimedeanClass.mk at this
    rw [ArchimedeanClass.mk_smul _ (by simp)] at this
    rw [ArchimedeanClass.mk_smul _ (by simp)] at this
    exact this
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
m : M
s s' : ℕ+
simp_rw :
  Eq (α := DivisibleHull M) (mk (HSMul.hSMul (α := ℤ) (↑(↑s : ℕ) : ℤ) m) s)
    (mk (HSMul.hSMul (α := ℤ) (↑(↑s' : ℕ) : ℤ) m) s')
simp_rw₁ : (↑s' : ℕ) • HSMul.hSMul (α := ℤ) (↑(↑s : ℕ) : ℤ) m = (↑s : ℕ) • HSMul.hSMul (α := ℤ) (↑(↑s' : ℕ) : ℤ) m
simp_rw₂ : (↑s' : ℕ) • (↑s : ℕ) • m = (↑s : ℕ) • (↑s' : ℕ) • m
simp_rw₃ : ((↑s' : ℕ) * (↑s : ℕ)) • m = ((↑s : ℕ) * (↑s' : ℕ)) • m
⊢ HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s : ℕ) : ℤ) (mk m s) =
    HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s' : ℕ) : ℤ) (mk m s')

Tactic:
simp_rw [zsmul_mk, mk_eq_mk_iff_smul_eq_smul, natCast_zsmul, smul_smul, mul_comm s'.val]

Premises used: PNat.val, smul_smul, DivisibleHull.mk_eq_mk_iff_smul_eq_smul, mul_comm, DivisibleHull.zsmul_mk, natCast_zsmul
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
m : M
s : ℕ+
rw :
  Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m s))
    (ArchimedeanClass.mk (↑m : DivisibleHull M))
⊢ Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m s))
    ((archimedeanClassOrderHom M : (a : ArchimedeanClass M) → ArchimedeanClass (DivisibleHull M))
      (ArchimedeanClass.mk m))

Tactic:
rw [archimedeanClassOrderHom, ArchimedeanClass.orderHom_mk, coeOrderAddMonoidHom_apply]

Premises used: _private.0.DivisibleHull.archimedeanClassOrderHom, DivisibleHull.coeOrderAddMonoidHom_apply, ArchimedeanClass.orderHom_mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
m : M
s : ℕ+
⊢ Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m s))
    (ArchimedeanClass.mk (↑m : DivisibleHull M))

Tactic:
apply archimedeanClassMk_mk_eq

Premises used: DivisibleHull.archimedeanClassMk_mk_eq
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
⊢ Function.Injective (α := ArchimedeanClass M) (β := ArchimedeanClass (DivisibleHull M))
    (⇑(archimedeanClassOrderHom M) : (a : ArchimedeanClass M) → ArchimedeanClass (DivisibleHull M))

Tactic:
ArchimedeanClass.orderHom_injective coe_injective

Premises used: DivisibleHull.coe_injective, ArchimedeanClass.orderHom_injective
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
x : DivisibleHull M
x_1 x_2 : M
x_3 x_4 : ℕ+
h : Eq (α := DivisibleHull M) (mk x_1 x_3) (mk x_2 x_4)
a :
  Eq (α := ArchimedeanClass (DivisibleHull M))
    ((archimedeanClassOrderHom M : (a : ArchimedeanClass M) → ArchimedeanClass (DivisibleHull M))
      ((fun (m : M) (s : ℕ+) ↦ (ArchimedeanClass.mk m : ArchimedeanClass M)) x_1 x_3))
    ((archimedeanClassOrderHom M : (a : ArchimedeanClass M) → ArchimedeanClass (DivisibleHull M))
      ((fun (m : M) (s : ℕ+) ↦ (ArchimedeanClass.mk m : ArchimedeanClass M)) x_2 x_4))
⊢ Eq.{u_2 + 1} (α := ArchimedeanClass M) ((fun (m : M) (s : ℕ+) ↦ (ArchimedeanClass.mk m : ArchimedeanClass M)) x_1 x_3)
    ((fun (m : M) (s : ℕ+) ↦ (ArchimedeanClass.mk m : ArchimedeanClass M)) x_2 x_4)

Tactic:
apply aux_archimedeanClassOrderHom_injective

Premises used: _private.0.DivisibleHull.aux_archimedeanClassOrderHom_injective
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
x : DivisibleHull M
x_1 x_2 : M
x_3 x_4 : ℕ+
h : Eq (α := DivisibleHull M) (mk x_1 x_3) (mk x_2 x_4)
⊢ Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk x_1 x_3)) (ArchimedeanClass.mk (mk x_2 x_4))

Tactic:
apply_fun ArchimedeanClass.mk at h

Premises used: ArchimedeanClass.mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
x : DivisibleHull M
x_1 x_2 : M
x_3 x_4 : ℕ+
h : Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk x_1 x_3)) (ArchimedeanClass.mk (mk x_2 x_4))
⊢ Eq (α := ArchimedeanClass (DivisibleHull M))
    ((archimedeanClassOrderHom M : (a : ArchimedeanClass M) → ArchimedeanClass (DivisibleHull M))
      ((fun (m : M) (s : ℕ+) ↦ (ArchimedeanClass.mk m : ArchimedeanClass M)) x_1 x_3))
    ((archimedeanClassOrderHom M : (a : ArchimedeanClass M) → ArchimedeanClass (DivisibleHull M))
      ((fun (m : M) (s : ℕ+) ↦ (ArchimedeanClass.mk m : ArchimedeanClass M)) x_2 x_4))

Tactic:
simpa [aux_archimedeanClassMk_mk] using h

Premises used: _private.0.DivisibleHull.aux_archimedeanClassMk_mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a b : DivisibleHull M
h : LE.le (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk a) (ArchimedeanClass.mk b)
mk :
  ∀ (num : M) (den : ℕ+)
    (h :
      LE.le (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (DivisibleHull.mk num den))
        (ArchimedeanClass.mk b)),
    LE.le.{u_2} (α := ArchimedeanClass M)
      ((fun (x : DivisibleHull M) ↦ (x.liftOn (fun (m : M) (s : ℕ+) ↦ ArchimedeanClass.mk m) ⋯ : ArchimedeanClass M))
        (DivisibleHull.mk num den))
      ((fun (x : DivisibleHull M) ↦ (x.liftOn (fun (m : M) (s : ℕ+) ↦ ArchimedeanClass.mk m) ⋯ : ArchimedeanClass M)) b)
⊢ LE.le.{u_2} (α := ArchimedeanClass M)
    ((fun (x : DivisibleHull M) ↦ (x.liftOn (fun (m : M) (s : ℕ+) ↦ ArchimedeanClass.mk m) ⋯ : ArchimedeanClass M)) a)
    ((fun (x : DivisibleHull M) ↦ (x.liftOn (fun (m : M) (s : ℕ+) ↦ ArchimedeanClass.mk m) ⋯ : ArchimedeanClass M)) b)

Tactic:
induction a with | mk _ _

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
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
b : DivisibleHull M
num : M
den : ℕ+
h :
  LE.le (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (DivisibleHull.mk num den))
    (ArchimedeanClass.mk b)
mk :
  ∀ (num_1 : M) (den_1 : ℕ+)
    (h :
      LE.le (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (DivisibleHull.mk num den))
        (ArchimedeanClass.mk (DivisibleHull.mk num_1 den_1))),
    LE.le.{u_2} (α := ArchimedeanClass M)
      ((fun (x : DivisibleHull M) ↦ (x.liftOn (fun (m : M) (s : ℕ+) ↦ ArchimedeanClass.mk m) ⋯ : ArchimedeanClass M))
        (DivisibleHull.mk num den))
      ((fun (x : DivisibleHull M) ↦ (x.liftOn (fun (m : M) (s : ℕ+) ↦ ArchimedeanClass.mk m) ⋯ : ArchimedeanClass M))
        (DivisibleHull.mk num_1 den_1))
⊢ LE.le.{u_2} (α := ArchimedeanClass M)
    ((fun (x : DivisibleHull M) ↦ (x.liftOn (fun (m : M) (s : ℕ+) ↦ ArchimedeanClass.mk m) ⋯ : ArchimedeanClass M))
      (DivisibleHull.mk num den))
    ((fun (x : DivisibleHull M) ↦ (x.liftOn (fun (m : M) (s : ℕ+) ↦ ArchimedeanClass.mk m) ⋯ : ArchimedeanClass M)) b)

Tactic:
induction b with | mk _ _

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
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
num : M
den : ℕ+
num_1 : M
den_1 : ℕ+
h :
  LE.le (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk num den))
    (ArchimedeanClass.mk (mk num_1 den_1))
⊢ LE.le (α := ArchimedeanClass (DivisibleHull M))
    ((archimedeanClassOrderHom M : (a : ArchimedeanClass M) → ArchimedeanClass (DivisibleHull M))
        (ArchimedeanClass.mk num) :
      ArchimedeanClass (DivisibleHull M))
    ((archimedeanClassOrderHom M : (a : ArchimedeanClass M) → ArchimedeanClass (DivisibleHull M))
        (ArchimedeanClass.mk num_1) :
      ArchimedeanClass (DivisibleHull M))

Tactic:
simp_rw [aux_archimedeanClassMk_mk] at h

Premises used: _private.0.DivisibleHull.aux_archimedeanClassMk_mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
num : M
den : ℕ+
num_1 : M
den_1 : ℕ+
h :
  LE.le (α := ArchimedeanClass (DivisibleHull M))
    ((archimedeanClassOrderHom M : (a : ArchimedeanClass M) → ArchimedeanClass (DivisibleHull M))
        (ArchimedeanClass.mk num) :
      ArchimedeanClass (DivisibleHull M))
    ((archimedeanClassOrderHom M : (a : ArchimedeanClass M) → ArchimedeanClass (DivisibleHull M))
        (ArchimedeanClass.mk num_1) :
      ArchimedeanClass (DivisibleHull M))
⊢ LE.le.{u_2} (α := ArchimedeanClass M)
    ((fun (x : DivisibleHull M) ↦ (x.liftOn (fun (m : M) (s : ℕ+) ↦ ArchimedeanClass.mk m) ⋯ : ArchimedeanClass M))
      (mk num den))
    ((fun (x : DivisibleHull M) ↦ (x.liftOn (fun (m : M) (s : ℕ+) ↦ ArchimedeanClass.mk m) ⋯ : ArchimedeanClass M))
      (mk num_1 den_1))

Tactic:
simpa using ((archimedeanClassOrderHom M).monotone.strictMono_of_injective
        aux_archimedeanClassOrderHom_injective).le_iff_le.mp h

Premises used: _private.0.DivisibleHull.archimedeanClassOrderHom, OrderHom.monotone, Monotone.strictMono_of_injective, Iff.mp, StrictMono.le_iff_le, _private.0.DivisibleHull.aux_archimedeanClassOrderHom_injective
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
h₁ :
  Eq (α := ArchimedeanClass (DivisibleHull M) →o ArchimedeanClass (DivisibleHull M))
    (OrderHom.comp (β := ArchimedeanClass M) (archimedeanClassOrderHom M) (archimedeanClassOrderHomInv M) :
      ArchimedeanClass (DivisibleHull M) →o ArchimedeanClass (DivisibleHull M))
    (OrderHom.id : ArchimedeanClass (DivisibleHull M) →o ArchimedeanClass (DivisibleHull M))
h₂ :
  Eq (α := ArchimedeanClass M →o ArchimedeanClass M)
    (OrderHom.comp (archimedeanClassOrderHomInv M) (archimedeanClassOrderHom M)) OrderHom.id
⊢ ArchimedeanClass M ≃o ArchimedeanClass (DivisibleHull M)

Tactic:
apply OrderIso.ofHomInv (archimedeanClassOrderHom M) (archimedeanClassOrderHomInv M)

Premises used: _private.0.DivisibleHull.archimedeanClassOrderHom, OrderIso.ofHomInv, _private.0.DivisibleHull.archimedeanClassOrderHomInv
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
h₁ :
  ∀ (a : ArchimedeanClass (DivisibleHull M)),
    Eq (α := ArchimedeanClass (DivisibleHull M))
      (((OrderHom.comp (β := ArchimedeanClass M) (archimedeanClassOrderHom M) (archimedeanClassOrderHomInv M) :
              ArchimedeanClass (DivisibleHull M) →o ArchimedeanClass (DivisibleHull M)) :
            (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass (DivisibleHull M))
          a :
        ArchimedeanClass (DivisibleHull M))
      ((OrderHom.id : (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass (DivisibleHull M)) a :
        ArchimedeanClass (DivisibleHull M))
⊢ Eq (α := ArchimedeanClass (DivisibleHull M) →o ArchimedeanClass (DivisibleHull M))
    (OrderHom.comp (β := ArchimedeanClass M) (archimedeanClassOrderHom M) (archimedeanClassOrderHomInv M) :
      ArchimedeanClass (DivisibleHull M) →o ArchimedeanClass (DivisibleHull M))
    (OrderHom.id : ArchimedeanClass (DivisibleHull M) →o ArchimedeanClass (DivisibleHull M))

Tactic:
ext a
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : ArchimedeanClass (DivisibleHull M)
h₁ :
  ∀ (a : DivisibleHull M),
    Eq (α := ArchimedeanClass (DivisibleHull M))
      (((OrderHom.comp (β := ArchimedeanClass M) (archimedeanClassOrderHom M) (archimedeanClassOrderHomInv M) :
              ArchimedeanClass (DivisibleHull M) →o ArchimedeanClass (DivisibleHull M)) :
            (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass (DivisibleHull M))
          (ArchimedeanClass.mk a) :
        ArchimedeanClass (DivisibleHull M))
      ((OrderHom.id : (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass (DivisibleHull M))
          (ArchimedeanClass.mk a) :
        ArchimedeanClass (DivisibleHull M))
⊢ Eq (α := ArchimedeanClass (DivisibleHull M))
    (((OrderHom.comp (β := ArchimedeanClass M) (archimedeanClassOrderHom M) (archimedeanClassOrderHomInv M) :
            ArchimedeanClass (DivisibleHull M) →o ArchimedeanClass (DivisibleHull M)) :
          (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass (DivisibleHull M))
        a :
      ArchimedeanClass (DivisibleHull M))
    ((OrderHom.id : (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass (DivisibleHull M)) a :
      ArchimedeanClass (DivisibleHull M))

Tactic:
induction a with | mk a

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
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : DivisibleHull M
h₁ :
  ∀ (m : M) (s : ℕ+),
    Eq (α := ArchimedeanClass (DivisibleHull M))
      (((OrderHom.comp (β := ArchimedeanClass M) (archimedeanClassOrderHom M) (archimedeanClassOrderHomInv M) :
              ArchimedeanClass (DivisibleHull M) →o ArchimedeanClass (DivisibleHull M)) :
            (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass (DivisibleHull M))
          (ArchimedeanClass.mk (mk m s)) :
        ArchimedeanClass (DivisibleHull M))
      ((OrderHom.id : (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass (DivisibleHull M))
          (ArchimedeanClass.mk (mk m s)) :
        ArchimedeanClass (DivisibleHull M))
⊢ Eq (α := ArchimedeanClass (DivisibleHull M))
    (((OrderHom.comp (β := ArchimedeanClass M) (archimedeanClassOrderHom M) (archimedeanClassOrderHomInv M) :
            ArchimedeanClass (DivisibleHull M) →o ArchimedeanClass (DivisibleHull M)) :
          (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass (DivisibleHull M))
        (ArchimedeanClass.mk a) :
      ArchimedeanClass (DivisibleHull M))
    ((OrderHom.id : (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass (DivisibleHull M))
        (ArchimedeanClass.mk a) :
      ArchimedeanClass (DivisibleHull M))

Tactic:
induction a with | mk m s

Premises used: DivisibleHull.mk