awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
inl : ∀ (ab : a ≤ b), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
have inr : ∀ (ab : b ≤ a), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Tactic: obtain ab | ab := le_total a b
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
⊢ |a|ₘ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
have rw : a ≤ b ∧ a⁻¹ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
Tactic: rw [mabs_le', and_comm, inv_le']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
rw : a ≤ b ∧ a⁻¹ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
⊢ |a|ₘ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
have rw₁ : a⁻¹ ≤ b ∧ a ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
Tactic: rw [mabs_le', and_comm, inv_le']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
rw : a ≤ b ∧ a⁻¹ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
rw₁ : a⁻¹ ≤ b ∧ a ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
⊢ |a|ₘ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
have rw₂ : b⁻¹ ≤ a ∧ a ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
Tactic: rw [mabs_le', and_comm, inv_le']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
⊢ a ≤ |b|ₘ ↔ b ≤ a⁻¹ ∨ a ≤ b
have rw : a ≤ b ∨ a ≤ b⁻¹ ↔ b ≤ a⁻¹ ∨ a ≤ b
Tactic: rw [le_mabs, or_comm, le_inv']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
rw : a ≤ b ∨ a ≤ b⁻¹ ↔ b ≤ a⁻¹ ∨ a ≤ b
⊢ a ≤ |b|ₘ ↔ b ≤ a⁻¹ ∨ a ≤ b
have rw₁ : a ≤ b⁻¹ ∨ a ≤ b ↔ b ≤ a⁻¹ ∨ a ≤ b
Tactic: rw [le_mabs, or_comm, le_inv']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
rw : a ≤ b ∨ a ≤ b⁻¹ ↔ b ≤ a⁻¹ ∨ a ≤ b
rw₁ : a ≤ b⁻¹ ∨ a ≤ b ↔ b ≤ a⁻¹ ∨ a ≤ b
⊢ a ≤ |b|ₘ ↔ b ≤ a⁻¹ ∨ a ≤ b
have rw₂ : b ≤ a⁻¹ ∨ a ≤ b ↔ b ≤ a⁻¹ ∨ a ≤ b
Tactic: rw [le_mabs, or_comm, le_inv']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
⊢ |a / b|ₘ ≤ |a|ₘ * |b|ₘ
have rw : |a * b⁻¹|ₘ ≤ |a|ₘ * |b⁻¹|ₘ
Tactic: rw [div_eq_mul_inv, ← mabs_inv b]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
⊢ |a / b|ₘ ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
have rw : c⁻¹ ≤ a / b ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
Tactic: rw [mabs_le, inv_le_div_iff_le_mul, div_le_iff_le_mul', and_comm, div_le_iff_le_mul']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
rw : c⁻¹ ≤ a / b ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
⊢ |a / b|ₘ ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
have rw₁ : b ≤ a * c ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
Tactic: rw [mabs_le, inv_le_div_iff_le_mul, div_le_iff_le_mul', and_comm, div_le_iff_le_mul']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
rw : c⁻¹ ≤ a / b ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
rw₁ : b ≤ a * c ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
⊢ |a / b|ₘ ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
have rw₂ : b ≤ a * c ∧ a ≤ b * c ↔ a ≤ b * c ∧ b / a ≤ c
Tactic: rw [mabs_le, inv_le_div_iff_le_mul, div_le_iff_le_mul', and_comm, div_le_iff_le_mul']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
rw : c⁻¹ ≤ a / b ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
rw₁ : b ≤ a * c ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
rw₂ : b ≤ a * c ∧ a ≤ b * c ↔ a ≤ b * c ∧ b / a ≤ c
⊢ |a / b|ₘ ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
have rw₃ : a ≤ b * c ∧ b ≤ a * c ↔ a ≤ b * c ∧ b / a ≤ c
Tactic: rw [mabs_le, inv_le_div_iff_le_mul, div_le_iff_le_mul', and_comm, div_le_iff_le_mul']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
rw : c⁻¹ ≤ a / b ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
rw₁ : b ≤ a * c ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
rw₂ : b ≤ a * c ∧ a ≤ b * c ↔ a ≤ b * c ∧ b / a ≤ c
rw₃ : a ≤ b * c ∧ b ≤ a * c ↔ a ≤ b * c ∧ b / a ≤ c
⊢ |a / b|ₘ ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
have rw₄ : a ≤ b * c ∧ b ≤ a * c ↔ a ≤ b * c ∧ b ≤ a * c
Tactic: rw [mabs_le, inv_le_div_iff_le_mul, div_le_iff_le_mul', and_comm, div_le_iff_le_mul']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
⊢ |a / b|ₘ < c ↔ a / b < c ∧ b / a < c
have rw : c⁻¹ < a / b ∧ a / b < c ↔ a / b < c ∧ b / a < c
Tactic: rw [mabs_lt, inv_lt_div_iff_lt_mul', div_lt_iff_lt_mul', and_comm, div_lt_iff_lt_mul']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
rw : c⁻¹ < a / b ∧ a / b < c ↔ a / b < c ∧ b / a < c
⊢ |a / b|ₘ < c ↔ a / b < c ∧ b / a < c
have rw₁ : b < a * c ∧ a / b < c ↔ a / b < c ∧ b / a < c
Tactic: rw [mabs_lt, inv_lt_div_iff_lt_mul', div_lt_iff_lt_mul', and_comm, div_lt_iff_lt_mul']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
rw : c⁻¹ < a / b ∧ a / b < c ↔ a / b < c ∧ b / a < c
rw₁ : b < a * c ∧ a / b < c ↔ a / b < c ∧ b / a < c
⊢ |a / b|ₘ < c ↔ a / b < c ∧ b / a < c
have rw₂ : b < a * c ∧ a < b * c ↔ a < b * c ∧ b / a < c
Tactic: rw [mabs_lt, inv_lt_div_iff_lt_mul', div_lt_iff_lt_mul', and_comm, div_lt_iff_lt_mul']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
rw : c⁻¹ < a / b ∧ a / b < c ↔ a / b < c ∧ b / a < c
rw₁ : b < a * c ∧ a / b < c ↔ a / b < c ∧ b / a < c
rw₂ : b < a * c ∧ a < b * c ↔ a < b * c ∧ b / a < c
⊢ |a / b|ₘ < c ↔ a / b < c ∧ b / a < c
have rw₃ : a < b * c ∧ b < a * c ↔ a < b * c ∧ b / a < c
Tactic: rw [mabs_lt, inv_lt_div_iff_lt_mul', div_lt_iff_lt_mul', and_comm, div_lt_iff_lt_mul']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
rw : c⁻¹ < a / b ∧ a / b < c ↔ a / b < c ∧ b / a < c
rw₁ : b < a * c ∧ a / b < c ↔ a / b < c ∧ b / a < c
rw₂ : b < a * c ∧ a < b * c ↔ a < b * c ∧ b / a < c
rw₃ : a < b * c ∧ b < a * c ↔ a < b * c ∧ b / a < c
⊢ |a / b|ₘ < c ↔ a / b < c ∧ b / a < c
have rw₄ : a < b * c ∧ b < a * c ↔ a < b * c ∧ b < a * c
Tactic: rw [mabs_lt, inv_lt_div_iff_lt_mul', div_lt_iff_lt_mul', and_comm, div_lt_iff_lt_mul']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
⊢ |a|ₘ = |a / b * b|ₘ
have rw : |a|ₘ = |a|ₘ
Tactic: rw [div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
⊢ |b|ₘ / |a|ₘ ≤ |a / b|ₘ
have rw : |b|ₘ / |a|ₘ ≤ |b / a|ₘ
Tactic: rw [mabs_div_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_le_n : a ≤ n
one_le_b : 1 ≤ b
b_le_n : b ≤ n
⊢ |a / b|ₘ ≤ n
have rw : a ≤ n * b ∧ b ≤ n * a
Tactic: rw [mabs_div_le_iff, div_le_iff_le_mul, div_le_iff_le_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b n : G
one_le_a : 1 ≤ a
a_lt_n : a < n
one_le_b : 1 ≤ b
b_lt_n : b < n
⊢ |a / b|ₘ < n
have rw : a < n * b ∧ b < n * a
Tactic: rw [mabs_div_lt_iff, div_lt_iff_lt_mul, div_lt_iff_lt_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hb : 1 ≤ b
⊢ |a|ₘ = b ↔ a = b ∨ a = b⁻¹
have refine : a = b ∨ a = b⁻¹ → |a|ₘ = b
Tactic: refine ⟨eq_or_eq_inv_of_mabs_eq, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
⊢ |a / c|ₘ = |a / b * (b / c)|ₘ
have rw : |a / c|ₘ = |a / c|ₘ
Tactic: rw [div_mul_div_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
⊢ |b / d|ₘ ≤ max (c / d) (d / a)
have inl : ∀ (h : d ≤ b), |b / d|ₘ ≤ max (c / d) (d / a)
Tactic: rcases le_total d b with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
inl : ∀ (h : d ≤ b), |b / d|ₘ ≤ max (c / d) (d / a)
⊢ |b / d|ₘ ≤ max (c / d) (d / a)
have inr : ∀ (h : b ≤ d), |b / d|ₘ ≤ max (c / d) (d / a)
Tactic: rcases le_total d b with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : d ≤ b
⊢ |b / d|ₘ ≤ max (c / d) (d / a)
have inl : b / d ≤ max (c / d) (d / a)
Tactic: rw [mabs_of_one_le <| one_le_div'.mpr h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ |b / d|ₘ ≤ max (c / d) (d / a)
have inr : d / b ≤ max (c / d) (d / a)
Tactic: rw [mabs_of_le_one <| div_le_one'.mpr h, inv_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
⊢ |a * b * c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ
have grw : |a * b|ₘ * |c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ
Tactic: grw [mabs_mul_le, mabs_mul_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b c : G
grw : |a * b|ₘ * |c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ
⊢ |a * b * c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ
have grw₁ : |a|ₘ * |b|ₘ * |c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ
Tactic: grw [mabs_mul_le, mabs_mul_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
⊢ |a / a|ₘ ≤ 1
have rw : LE.le.{u_1} (α := G) |1|ₘ 1
Tactic: rw [div_self', mabs_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
rw : LE.le.{u_1} (α := G) |1|ₘ 1
⊢ |a / a|ₘ ≤ 1
have rw₁ : LE.le.{u_1} (α := G) 1 1
Tactic: rw [div_self', mabs_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
⊢ |a|ₘ = a ↔ 1 ≤ a
have rw : max a a⁻¹ = a ↔ 1 ≤ a
Tactic: rw [mabs_eq_max_inv, max_eq_left_iff, inv_le_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
rw : max a a⁻¹ = a ↔ 1 ≤ a
⊢ |a|ₘ = a ↔ 1 ≤ a
have rw₁ : a⁻¹ ≤ a ↔ 1 ≤ a
Tactic: rw [mabs_eq_max_inv, max_eq_left_iff, inv_le_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
rw : max a a⁻¹ = a ↔ 1 ≤ a
rw₁ : a⁻¹ ≤ a ↔ 1 ≤ a
⊢ |a|ₘ = a ↔ 1 ≤ a
have rw₂ : 1 ≤ a ↔ 1 ≤ a
Tactic: rw [mabs_eq_max_inv, max_eq_left_iff, inv_le_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
⊢ |a|ₘ = a⁻¹ ↔ a ≤ 1
have rw : max a a⁻¹ = a⁻¹ ↔ a ≤ 1
Tactic: rw [mabs_eq_max_inv, max_eq_right_iff, le_inv_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
rw : max a a⁻¹ = a⁻¹ ↔ a ≤ 1
⊢ |a|ₘ = a⁻¹ ↔ a ≤ 1
have rw₁ : a ≤ a⁻¹ ↔ a ≤ 1
Tactic: rw [mabs_eq_max_inv, max_eq_right_iff, le_inv_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
rw : max a a⁻¹ = a⁻¹ ↔ a ≤ 1
rw₁ : a ≤ a⁻¹ ↔ a ≤ 1
⊢ |a|ₘ = a⁻¹ ↔ a ≤ 1
have rw₂ : a ≤ 1 ↔ a ≤ 1
Tactic: rw [mabs_eq_max_inv, max_eq_right_iff, le_inv_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1
have inl : 1 ≤ a → |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1
Tactic: cases le_or_gt 1 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
inl : 1 ≤ a → |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1
have inr : a < 1 → |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1
Tactic: cases le_or_gt 1 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
⊢ max a 1 * max a⁻¹ 1 = |a|ₘ
have symm : |a|ₘ = max a 1 * max a⁻¹ 1
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
⊢ |a|ₘ = max a 1 * max a⁻¹ 1
have inl : ∀ (ha : 1 ≤ a), |a|ₘ = max a 1 * max a⁻¹ 1
Tactic: rcases le_total 1 a with (ha | ha)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a : G
inl : ∀ (ha : 1 ≤ a), |a|ₘ = max a 1 * max a⁻¹ 1
⊢ |a|ₘ = max a 1 * max a⁻¹ 1
have inr : ∀ (ha : a ≤ 1), |a|ₘ = max a 1 * max a⁻¹ 1
Tactic: rcases le_total 1 a with (ha | ha)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Action (goal)
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
⊢ a ≤ HPow.hPow (β := ℕ) g 0 • a
have zero : a ≤ HSMul.hSMul.{u_4, u_5, u_5} (α := G) 1 a
Tactic: rw [pow_zero, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Action (goal)
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
zero : a ≤ HSMul.hSMul.{u_4, u_5, u_5} (α := G) 1 a
⊢ a ≤ HPow.hPow (β := ℕ) g 0 • a
have zero₁ : a ≤ a
Tactic: rw [pow_zero, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Action (goal)
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
hn : a ≤ g ^ n • a
⊢ a ≤ g ^ (n + 1) • a
have succ : a ≤ g • g ^ n • a
Tactic: rw [pow_succ', mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Action (goal)
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
⊢ a ≤ g ^ n • a
have zero : a ≤ HPow.hPow (β := ℕ) g 0 • a
Tactic: induction n with
  | zero => rw [pow_zero, one_smul]
  | succ n hn =>
    rw [pow_succ', mul_smul]
    exact h.trans (smul_mono_right g hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Action (goal)
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
zero : a ≤ HPow.hPow (β := ℕ) g 0 • a
⊢ a ≤ g ^ n • a
have succ : ∀ (n : ℕ) (hn : a ≤ g ^ n • a), a ≤ g ^ (n + 1) • a
Tactic: induction n with
  | zero => rw [pow_zero, one_smul]
  | succ n hn =>
    rw [pow_succ', mul_smul]
    exact h.trans (smul_mono_right g hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Action (goal)
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
⊢ HPow.hPow (β := ℕ) g 0 • a ≤ a
have zero : HSMul.hSMul.{u_4, u_5, u_5} (α := G) 1 a ≤ a
Tactic: rw [pow_zero, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Action (goal)
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
zero : HSMul.hSMul.{u_4, u_5, u_5} (α := G) 1 a ≤ a
⊢ HPow.hPow (β := ℕ) g 0 • a ≤ a
have zero₁ : a ≤ a
Tactic: rw [pow_zero, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Action (goal)
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
hn : g ^ n • a ≤ a
⊢ g ^ (n + 1) • a ≤ a
have succ : g • g ^ n • a ≤ a
Tactic: rw [pow_succ', mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Action (goal)
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
⊢ g ^ n • a ≤ a
have zero : HPow.hPow (β := ℕ) g 0 • a ≤ a
Tactic: induction n with
  | zero => rw [pow_zero, one_smul]
  | succ n hn =>
    rw [pow_succ', mul_smul]
    exact (smul_mono_right g hn).trans h
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Action (goal)
Goal:
G : Type u_4
inst : Monoid G
α : Type u_5
inst_1 : Preorder α
g : G
a : α
inst_2 : MulAction G α
inst_3 : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
zero : HPow.hPow (β := ℕ) g 0 • a ≤ a
⊢ g ^ n • a ≤ a
have succ : ∀ (n : ℕ) (hn : g ^ n • a ≤ a), g ^ (n + 1) • a ≤ a
Tactic: induction n with
  | zero => rw [pow_zero, one_smul]
  | succ n hn =>
    rw [pow_succ', mul_smul]
    exact (smul_mono_right g hn).trans h
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : 1 < a
⊢ StrictMono.{0, u_1} (β := α) fun (n : ℤ) ↦ a ^ n
have refine : ∀ (n : ℤ), a ^ n < a ^ (n + 1)
Tactic: refine strictMono_int_of_lt_succ fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ (n + 1)
have rw : a ^ n < a ^ n * a
Tactic: rw [zpow_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : a < 1
⊢ StrictAnti.{0, u_1} (β := α) fun (n : ℤ) ↦ a ^ n
have refine : ∀ (n : ℤ), a ^ (n + 1) < a ^ n
Tactic: refine strictAnti_int_of_succ_lt fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : a < 1
n : ℤ
⊢ a ^ (n + 1) < a ^ n
have rw : a ^ n * a < a ^ n
Tactic: rw [zpow_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : 1 ≤ a
⊢ Monotone.{0, u_1} (β := α) fun (n : ℤ) ↦ a ^ n
have refine : ∀ (n : ℤ), a ^ n ≤ a ^ (n + 1)
Tactic: refine monotone_int_of_le_succ fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ (n + 1)
have rw : a ^ n ≤ a ^ n * a
Tactic: rw [zpow_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ LT.lt.{u_1} (α := α) ((fun (x : α) ↦ x ^ n) a) ((fun (x : α) ↦ x ^ n) b)
have rw : 1 < (b / a) ^ n
Tactic: rw [← one_lt_div', ← div_zpow]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ LE.le.{u_1} (α := α) ((fun (x : α) ↦ x ^ n) a) ((fun (x : α) ↦ x ^ n) b)
have rw : 1 ≤ (b / a) ^ n
Tactic: rw [← one_le_div', ← div_zpow]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
⊢ False
have rcases : ∀ (a : α) (ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x), False
Tactic: rcases exists_zpow_surjective α with ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
⊢ False
have inl : ∀ (hlt : a < 1), False
Tactic: rcases lt_trichotomy a 1 with hlt | rfl | hlt
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
inl : ∀ (hlt : a < 1), False
⊢ False
have inr : ∀ (ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ HPow.hPow (α := α) 1 x), False
Tactic: rcases lt_trichotomy a 1 with hlt | rfl | hlt
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
inl : ∀ (hlt : a < 1), False
inr : ∀ (ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ HPow.hPow (α := α) 1 x), False
⊢ False
have inr₁ : ∀ (hlt : 1 < a), False
Tactic: rcases lt_trichotomy a 1 with hlt | rfl | hlt
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : a < 1
⊢ False
have inl : ∀ (b : α) (hab : a < b) (hb : b < 1), False
Tactic: rcases exists_between hlt with ⟨b, hab, hb⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : a < 1
b : α
hab : a < b
hb : b < 1
⊢ False
have inl : ∀ (k : ℤ) (hab : a < (fun (x : ℤ) ↦ a ^ x) k) (hb : LT.lt.{u_1} (α := α) ((fun (x : ℤ) ↦ a ^ x) k) 1), False
Tactic: rcases ha b with ⟨k, rfl⟩
Cleared hypotheses: b, hab, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : a < 1
k : ℤ
hab : a < (fun (x : ℤ) ↦ a ^ x) k
hb : LT.lt.{u_1} (α := α) ((fun (x : ℤ) ↦ a ^ x) k) 1
⊢ False
have inl : 0 < k ∧ k < 1
Tactic: suffices 0 < k ∧ k < 1 by lia