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 : AddCommMonoid M
inst_2 : LinearOrder M
inst_3 : IsOrderedCancelAddMonoid M
a : ℚ≥0
ha : 0 < a
c : DivisibleHull M
mb : M
sb : ℕ+
h : mk mb sb < c
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk mb sb) < a • c
have mk : ∀ (mc : M) (sc : ℕ+) (h : LT.lt (α := DivisibleHull M) (mk mb sb) (mk mc sc)),
  HSMul.hSMul (β := DivisibleHull M) a (mk mb sb) < HSMul.hSMul (β := DivisibleHull M) a (mk mc sc)
Tactic: induction c with | mk mc sc
Cleared hypotheses: c, 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
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : LT.lt (α := DivisibleHull M) (mk mb sb) (mk mc sc)
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk mb sb) < HSMul.hSMul (β := DivisibleHull M) a (mk mc sc)
have h₁ : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
Tactic: simp_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
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
⊢ HSMul.hSMul (β := DivisibleHull M) a (mk mb sb) < HSMul.hSMul (β := DivisibleHull M) a (mk mc sc)
have mk : ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry) : ℕ) * (↑sc : ℕ) * a.num) • mb <
  ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry) : ℕ) * (↑sb : ℕ) * a.num) • mc
Tactic: simp_rw [nnqsmul_mk, mk_lt_mk, smul_smul, PNat.mul_coe]
-- 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
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : (↑sc : ℕ) • mb < (↑sb : ℕ) • mc
⊢ ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯) : ℕ) * (↑sc : ℕ) * a.num) • mb <
    ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den ⋯) : ℕ) * (↑sb : ℕ) * a.num) • mc
have mk : ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry) : ℕ) * a.num) • (↑sc : ℕ) • mb <
  ((↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.den sorry) : ℕ) * a.num) • (↑sb : ℕ) • mc
Tactic: simp_rw [mul_right_comm _ _ a.num, mul_smul _ _ mc, mul_smul _ _ mb]
-- 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
ha : 0 < a
b c : ℚ≥0
h : b < c
⊢ b • a < c • a
have mk : ∀ (m : M) (s : ℕ+) (ha : LT.lt (α := DivisibleHull M) 0 (mk m s)),
  HSMul.hSMul (β := DivisibleHull M) b (mk m s) < HSMul.hSMul (β := DivisibleHull M) c (mk m s)
Tactic: induction a with | mk m s
Cleared hypotheses: a, ha
-- 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 : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : LT.lt (α := DivisibleHull M) 0 (mk m s)
⊢ HSMul.hSMul (β := DivisibleHull M) b (mk m s) < HSMul.hSMul (β := DivisibleHull M) c (mk m s)
have mk : (c.den * (↑s : ℕ) * b.num) • m < (b.den * (↑s : ℕ) * c.num) • m
Tactic: simp_rw [nnqsmul_mk, mk_lt_mk, smul_smul, PNat.mul_coe, PNat.mk_coe]
-- 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 : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : LT.lt (α := DivisibleHull M) 0 (mk m s)
⊢ (c.den * (↑s : ℕ) * b.num) • m < (b.den * (↑s : ℕ) * c.num) • m
have mk : c.den * (↑s : ℕ) * b.num < b.den * (↑s : ℕ) * c.num
Tactic: refine smul_lt_smul_of_pos_right ?_ ?_
-- 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 : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : LT.lt (α := DivisibleHull M) 0 (DivisibleHull.mk m s)
mk : c.den * (↑s : ℕ) * b.num < b.den * (↑s : ℕ) * c.num
⊢ (c.den * (↑s : ℕ) * b.num) • m < (b.den * (↑s : ℕ) * c.num) • m
have mk₁ : 0 < m
Tactic: refine smul_lt_smul_of_pos_right ?_ ?_
-- 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 : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : LT.lt (α := DivisibleHull M) 0 (mk m s)
⊢ c.den * (↑s : ℕ) * b.num < b.den * (↑s : ℕ) * c.num
have h₁ : c.den * (↑s : ℕ) * b.num = b.num * c.den * (↑s : ℕ)
Tactic: convert! mul_lt_mul_of_pos_right (NNRat.lt_def.mp h) (show 0 < s.val by simp) 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 : 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 : ℕ)
⊢ c.den * (↑s : ℕ) * b.num < b.den * (↑s : ℕ) * c.num
have h₂ : b.den * (↑s : ℕ) * c.num = c.num * b.den * (↑s : ℕ)
Tactic: convert! mul_lt_mul_of_pos_right (NNRat.lt_def.mp h) (show 0 < s.val by simp) using 1
-- 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
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : LT.lt (α := DivisibleHull M) 0 (mk m s)
⊢ 0 < m
have ha₁ : HSMul.hSMul (β := M) (↑s : ℕ) 0 < (↑1 : ℕ) • m
Tactic: rw [← mk_zero 1, mk_lt_mk] at ha
Cleared hypotheses: ha
-- 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
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : ℚ
ha : 0 < a
b c : DivisibleHull M
h : b < c
⊢ a • b < a • c
have simp_rw : Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a sorry • b < Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) a sorry • c
Tactic: simp_rw [qsmul_of_nonneg ha.le]
-- 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
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
⊢ b • a < c • a
have a₁ : 0 < c • a - b • a
Tactic: apply lt_of_sub_pos
-- 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
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
⊢ 0 < c • a - b • a
have a₁ : 0 < (c - b) • a
Tactic: rw [← sub_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
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
⊢ 0 < (c - b) • a
have a₁ : 0 < Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (c - b) sorry • a
Tactic: simp_rw [qsmul_of_nonneg (sub_pos_of_lt h).le]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (hypothesis)
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 (mk m s)) (ArchimedeanClass.mk (mk m s'))
have 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')))
Tactic: apply_fun ArchimedeanClass.mk at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (hypothesis)
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 (mk m s'))
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
m : M
s s' : ℕ+
⊢ Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m s)) (ArchimedeanClass.mk (mk m s'))
have suffices : HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s : ℕ) : ℤ) (mk m s) =
  HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s' : ℕ) : ℤ) (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
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
m : M
s s' : ℕ+
⊢ HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s : ℕ) : ℤ) (mk m s) =
    HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s' : ℕ) : ℤ) (mk m s')
have simp_rw : Eq (α := DivisibleHull M) (mk (HSMul.hSMul (α := ℤ) (↑(↑s : ℕ) : ℤ) m) s)
  (mk (HSMul.hSMul (α := ℤ) (↑(↑s' : ℕ) : ℤ) m) s')
Tactic: simp_rw [zsmul_mk, mk_eq_mk_iff_smul_eq_smul, natCast_zsmul, smul_smul, mul_comm s'.val]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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')
⊢ HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s : ℕ) : ℤ) (mk m s) =
    HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s' : ℕ) : ℤ) (mk m s')
have simp_rw₁ : (↑s' : ℕ) • HSMul.hSMul (α := ℤ) (↑(↑s : ℕ) : ℤ) m = (↑s : ℕ) • HSMul.hSMul (α := ℤ) (↑(↑s' : ℕ) : ℤ) m
Tactic: simp_rw [zsmul_mk, mk_eq_mk_iff_smul_eq_smul, natCast_zsmul, smul_smul, mul_comm s'.val]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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
⊢ HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s : ℕ) : ℤ) (mk m s) =
    HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s' : ℕ) : ℤ) (mk m s')
have simp_rw₂ : (↑s' : ℕ) • (↑s : ℕ) • m = (↑s : ℕ) • (↑s' : ℕ) • m
Tactic: simp_rw [zsmul_mk, mk_eq_mk_iff_smul_eq_smul, natCast_zsmul, smul_smul, mul_comm s'.val]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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
⊢ HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s : ℕ) : ℤ) (mk m s) =
    HSMul.hSMul (α := ℤ) (β := DivisibleHull M) (↑(↑s' : ℕ) : ℤ) (mk m s')
have simp_rw₃ : ((↑s' : ℕ) * (↑s : ℕ)) • m = ((↑s : ℕ) * (↑s' : ℕ)) • m
Tactic: simp_rw [zsmul_mk, mk_eq_mk_iff_smul_eq_smul, natCast_zsmul, smul_smul, mul_comm s'.val]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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))
    ((archimedeanClassOrderHom M : (a : ArchimedeanClass M) → ArchimedeanClass (DivisibleHull M))
      (ArchimedeanClass.mk m))
have rw : Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m s)) (ArchimedeanClass.mk (↑m : DivisibleHull M))
Tactic: rw [archimedeanClassOrderHom, ArchimedeanClass.orderHom_mk, coeOrderAddMonoidHom_apply]
-- 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
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.{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)
have 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))
Tactic: apply aux_archimedeanClassOrderHom_injective
-- 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 : 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))
    ((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))
have h₁ : 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
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 : 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)
⊢ 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)
have mk : ∀ (num : M) (den : ℕ+)
  (h : LE.le (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (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) sorry : ArchimedeanClass M))
      (mk num den))
    ((fun (x : DivisibleHull M) ↦ (x.liftOn (fun (m : M) (s : ℕ+) ↦ ArchimedeanClass.mk m) sorry : ArchimedeanClass M)) b)
Tactic: induction a with | mk _ _
Cleared hypotheses: a, 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
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
b : DivisibleHull M
num : M
den : ℕ+
h : LE.le (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (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))
      (mk num den))
    ((fun (x : DivisibleHull M) ↦ (x.liftOn (fun (m : M) (s : ℕ+) ↦ ArchimedeanClass.mk m) ⋯ : ArchimedeanClass M)) b)
have mk : ∀ (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.{u_2} (α := ArchimedeanClass M)
    ((fun (x : DivisibleHull M) ↦ (x.liftOn (fun (m : M) (s : ℕ+) ↦ ArchimedeanClass.mk m) sorry : ArchimedeanClass M))
      (mk num den))
    ((fun (x : DivisibleHull M) ↦ (x.liftOn (fun (m : M) (s : ℕ+) ↦ ArchimedeanClass.mk m) sorry : ArchimedeanClass M))
      (mk num_1 den_1))
Tactic: induction b with | mk _ _
Cleared hypotheses: b, 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 : 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.{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))
have 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))
Tactic: simp_rw [aux_archimedeanClassMk_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 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
⊢ ArchimedeanClass M ≃o ArchimedeanClass (DivisibleHull M)
have 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))
Tactic: apply OrderIso.ofHomInv (archimedeanClassOrderHom M) (archimedeanClassOrderHomInv M)
-- 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
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))
⊢ ArchimedeanClass M ≃o ArchimedeanClass (DivisibleHull M)
have h₂ : Eq (α := ArchimedeanClass M →o ArchimedeanClass M)
  (OrderHom.comp (archimedeanClassOrderHomInv M) (archimedeanClassOrderHom M)) OrderHom.id
Tactic: apply OrderIso.ofHomInv (archimedeanClassOrderHom M) (archimedeanClassOrderHomInv M)
-- 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
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid 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))
have 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))
Tactic: ext 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 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
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))
have 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))
Tactic: induction a with | mk a
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 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
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))
have 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))
Tactic: induction a with | mk m s
Cleared hypotheses: a