awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
c₁ : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ
c₂ :
  (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ =
    (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c)))
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ
have c₃ : (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
  (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
Tactic: calc
    |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ =
        (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ := by
        rw [sup_div_inf_eq_mabs_div]
    _ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) := by
        rw [sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)]
    _ = (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) := by
        rw [← sup_inf_right, ← inf_sup_right, sup_assoc, sup_comm c (a ⊔ c), sup_right_idem,
          sup_assoc, inf_assoc, inf_comm c (a ⊓ c), inf_right_idem, inf_assoc]
    _ = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) := by rw [div_mul_div_comm]
    _ = (b ⊔ a) * c / ((b ⊓ a) * c) := by
        rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
    _ = (b ⊔ a) / (b ⊓ a) := by
        rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
    _ = |a / b|ₘ := by rw [sup_div_inf_eq_mabs_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
c₁ : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ
c₂ :
  (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ =
    (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c)))
c₃ :
  (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ
have c₄ : (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c))
Tactic: calc
    |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ =
        (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ := by
        rw [sup_div_inf_eq_mabs_div]
    _ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) := by
        rw [sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)]
    _ = (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) := by
        rw [← sup_inf_right, ← inf_sup_right, sup_assoc, sup_comm c (a ⊔ c), sup_right_idem,
          sup_assoc, inf_assoc, inf_comm c (a ⊓ c), inf_right_idem, inf_assoc]
    _ = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) := by rw [div_mul_div_comm]
    _ = (b ⊔ a) * c / ((b ⊓ a) * c) := by
        rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
    _ = (b ⊔ a) / (b ⊓ a) := by
        rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
    _ = |a / b|ₘ := by rw [sup_div_inf_eq_mabs_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
c₁ : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ
c₂ :
  (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ =
    (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c)))
c₃ :
  (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
c₄ :
  (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c))
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ
have c₅ : (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)
Tactic: calc
    |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ =
        (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ := by
        rw [sup_div_inf_eq_mabs_div]
    _ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) := by
        rw [sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)]
    _ = (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) := by
        rw [← sup_inf_right, ← inf_sup_right, sup_assoc, sup_comm c (a ⊔ c), sup_right_idem,
          sup_assoc, inf_assoc, inf_comm c (a ⊓ c), inf_right_idem, inf_assoc]
    _ = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) := by rw [div_mul_div_comm]
    _ = (b ⊔ a) * c / ((b ⊓ a) * c) := by
        rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
    _ = (b ⊔ a) / (b ⊓ a) := by
        rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
    _ = |a / b|ₘ := by rw [sup_div_inf_eq_mabs_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
c₁ : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ
c₂ :
  (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ =
    (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c)))
c₃ :
  (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
c₄ :
  (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c))
c₅ : (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ
have c₆ : (b ⊔ a) * c / ((b ⊓ a) * c) = (b ⊔ a) / (b ⊓ a)
Tactic: calc
    |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ =
        (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ := by
        rw [sup_div_inf_eq_mabs_div]
    _ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) := by
        rw [sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)]
    _ = (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) := by
        rw [← sup_inf_right, ← inf_sup_right, sup_assoc, sup_comm c (a ⊔ c), sup_right_idem,
          sup_assoc, inf_assoc, inf_comm c (a ⊓ c), inf_right_idem, inf_assoc]
    _ = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) := by rw [div_mul_div_comm]
    _ = (b ⊔ a) * c / ((b ⊓ a) * c) := by
        rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
    _ = (b ⊔ a) / (b ⊓ a) := by
        rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
    _ = |a / b|ₘ := by rw [sup_div_inf_eq_mabs_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
c₁ : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ
c₂ :
  (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ =
    (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c)))
c₃ :
  (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
c₄ :
  (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c))
c₅ : (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)
c₆ : (b ⊔ a) * c / ((b ⊓ a) * c) = (b ⊔ a) / (b ⊓ a)
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ
have c₇ : (b ⊔ a) / (b ⊓ a) = |a / b|ₘ
Tactic: calc
    |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ =
        (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ := by
        rw [sup_div_inf_eq_mabs_div]
    _ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) := by
        rw [sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)]
    _ = (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) := by
        rw [← sup_inf_right, ← inf_sup_right, sup_assoc, sup_comm c (a ⊔ c), sup_right_idem,
          sup_assoc, inf_assoc, inf_comm c (a ⊓ c), inf_right_idem, inf_assoc]
    _ = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) := by rw [div_mul_div_comm]
    _ = (b ⊔ a) * c / ((b ⊓ a) * c) := by
        rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
    _ = (b ⊔ a) / (b ⊓ a) := by
        rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
    _ = |a / b|ₘ := by rw [sup_div_inf_eq_mabs_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ ≤ |a / b|ₘ
have apply : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ
Tactic: apply le_of_mul_le_of_one_le_left _ (one_le_mabs _)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ
have rw : |a / b|ₘ ≤ |a / b|ₘ
Tactic: rw [mabs_div_sup_mul_mabs_div_inf]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
⊢ |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ
have apply : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ
Tactic: apply le_of_mul_le_of_one_le_right _ (one_le_mabs _)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
a b : α
⊢ |a|ₘ = |b|ₘ ↔ a = b ∨ a = b⁻¹
have refine : ∀ (h : |a|ₘ = |b|ₘ), a = b ∨ a = b⁻¹
Tactic: refine ⟨fun h ↦ ?_, by rintro (h | h) <;> simp [h]⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
a b : α
h : |a|ₘ = |b|ₘ
⊢ a = b ∨ a = b⁻¹
have inl : ∀ (h : |(|b|ₘ)|ₘ = |b|ₘ), |b|ₘ = b ∨ |b|ₘ = b⁻¹
Tactic: obtain rfl | rfl := eq_or_eq_inv_of_mabs_eq h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
a b : α
h : |a|ₘ = |b|ₘ
inl : ∀ (h : |(|b|ₘ)|ₘ = |b|ₘ), |b|ₘ = b ∨ |b|ₘ = b⁻¹
⊢ a = b ∨ a = b⁻¹
have inr : ∀ (h : ||b|ₘ⁻¹|ₘ = |b|ₘ), |b|ₘ⁻¹ = b ∨ |b|ₘ⁻¹ = b⁻¹
Tactic: obtain rfl | rfl := eq_or_eq_inv_of_mabs_eq h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
β : Type u_2
F : Type u_3
inst_2 : Group β
inst_3 : LinearOrder β
inst_4 : FunLike F α β
inst_5 : OrderHomClass F α β
inst_6 : MonoidHomClass F α β
f : F
a : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) |a|ₘ : β) (|(f : (a : α) → β) a|ₘ : β)
have rw : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (max a a⁻¹) : β) (|(f : (a : α) → β) a|ₘ : β)
Tactic: rw [mabs, mabs, (OrderHomClass.mono f).map_max, map_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
β : Type u_2
F : Type u_3
inst_2 : Group β
inst_3 : LinearOrder β
inst_4 : FunLike F α β
inst_5 : OrderHomClass F α β
inst_6 : MonoidHomClass F α β
f : F
a : α
rw : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (max a a⁻¹) : β) (|(f : (a : α) → β) a|ₘ : β)
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) |a|ₘ : β) (|(f : (a : α) → β) a|ₘ : β)
have rw₁ : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (max a a⁻¹) : β) (max ((f : (a : α) → β) a) ((f : (a : α) → β) a)⁻¹ : β)
Tactic: rw [mabs, mabs, (OrderHomClass.mono f).map_max, map_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
β : Type u_2
F : Type u_3
inst_2 : Group β
inst_3 : LinearOrder β
inst_4 : FunLike F α β
inst_5 : OrderHomClass F α β
inst_6 : MonoidHomClass F α β
f : F
a : α
rw : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (max a a⁻¹) : β) (|(f : (a : α) → β) a|ₘ : β)
rw₁ : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (max a a⁻¹) : β) (max ((f : (a : α) → β) a) ((f : (a : α) → β) a)⁻¹ : β)
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) |a|ₘ : β) (|(f : (a : α) → β) a|ₘ : β)
have rw₂ : Eq.{u_2 + 1} (α := β) (max ((f : (a : α) → β) a) ((f : (a : α) → β) a⁻¹) : β)
  (max ((f : (a : α) → β) a) ((f : (a : α) → β) a)⁻¹ : β)
Tactic: rw [mabs, mabs, (OrderHomClass.mono f).map_max, map_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
β : Type u_2
F : Type u_3
inst_2 : Group β
inst_3 : LinearOrder β
inst_4 : FunLike F α β
inst_5 : OrderHomClass F α β
inst_6 : MonoidHomClass F α β
f : F
a : α
rw : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (max a a⁻¹) : β) (|(f : (a : α) → β) a|ₘ : β)
rw₁ : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (max a a⁻¹) : β) (max ((f : (a : α) → β) a) ((f : (a : α) → β) a)⁻¹ : β)
rw₂ :
  Eq.{u_2 + 1} (α := β) (max ((f : (a : α) → β) a) ((f : (a : α) → β) a⁻¹) : β)
    (max ((f : (a : α) → β) a) ((f : (a : α) → β) a)⁻¹ : β)
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) |a|ₘ : β) (|(f : (a : α) → β) a|ₘ : β)
have rw₃ : Eq.{u_2 + 1} (α := β) (max ((f : (a : α) → β) a) ((f : (a : α) → β) a)⁻¹ : β)
  (max ((f : (a : α) → β) a) ((f : (a : α) → β) a)⁻¹ : β)
Tactic: rw [mabs, mabs, (OrderHomClass.mono f).map_max, map_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
⊢ 1 < |a|ₘ ↔ a ≠ 1
have inl : ∀ (ha : a < 1), 1 < |a|ₘ ↔ a ≠ 1
Tactic: obtain ha | rfl | ha := lt_trichotomy a 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
inl : ∀ (ha : a < 1), 1 < |a|ₘ ↔ a ≠ 1
⊢ 1 < |a|ₘ ↔ a ≠ 1
have inr : LT.lt.{u_1} (α := α) 1 |1|ₘ ↔ Ne.{u_1 + 1} (α := α) 1 1
Tactic: obtain ha | rfl | ha := lt_trichotomy a 1
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
inl : ∀ (ha : a < 1), 1 < |a|ₘ ↔ a ≠ 1
inr : LT.lt.{u_1} (α := α) 1 |1|ₘ ↔ Ne.{u_1 + 1} (α := α) 1 1
⊢ 1 < |a|ₘ ↔ a ≠ 1
have inr₁ : ∀ (ha : 1 < a), 1 < |a|ₘ ↔ a ≠ 1
Tactic: obtain ha | rfl | ha := lt_trichotomy a 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
⊢ |a|ₘ⁻¹ ≤ a
have inl : ∀ (h : 1 ≤ a), |a|ₘ⁻¹ ≤ a
Tactic: obtain h | h := le_total 1 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
inl : ∀ (h : 1 ≤ a), |a|ₘ⁻¹ ≤ a
⊢ |a|ₘ⁻¹ ≤ a
have inr : ∀ (h : a ≤ 1), |a|ₘ⁻¹ ≤ a
Tactic: obtain h | h := le_total 1 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
⊢ 1 ≤ a * |a|ₘ
have grw : a * a⁻¹ ≤ a * |a|ₘ
Tactic: grw [← mul_inv_cancel a, inv_le_mabs a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
grw : a * a⁻¹ ≤ a * |a|ₘ
⊢ 1 ≤ a * |a|ₘ
have grw₁ : a * |a|ₘ ≤ a * |a|ₘ
Tactic: grw [← mul_inv_cancel a, inv_le_mabs a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
inst_3 : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
⊢ |a|ₘ ≤ |b|ₘ
have rw : a⁻¹ ≤ b⁻¹
Tactic: rw [mabs_of_le_one ha, mabs_of_le_one (hab.trans ha)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
inst_3 : MulRightMono α
⊢ a⁻¹ < b ∧ a < b ↔ b⁻¹ < a ∧ a < b
have rw : b⁻¹ < a ∧ a < b ↔ b⁻¹ < a ∧ a < b
Tactic: rw [inv_lt']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
⊢ max a b / min a b = |a / b|ₘ
have inl : ∀ (ab : a ≤ b), max a b / min a b = |a / b|ₘ
Tactic: rcases le_total a b with ab | ba
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
inl : ∀ (ab : a ≤ b), max a b / min a b = |a / b|ₘ
⊢ max a b / min a b = |a / b|ₘ
have inr : ∀ (ba : b ≤ a), max a b / min a b = |a / b|ₘ
Tactic: rcases le_total a b with ab | ba
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
ab : a ≤ b
⊢ max a b / min a b = |a / b|ₘ
have inl : a / b ≤ 1
Tactic: rw [max_eq_right ab, min_eq_left ab, mabs_of_le_one, inv_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
ba : b ≤ a
⊢ max a b / min a b = |a / b|ₘ
have inr : 1 ≤ a / b
Tactic: rw [max_eq_left ba, min_eq_right ba, mabs_of_one_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
⊢ max a b / min a b = |b / a|ₘ
have rw : max a b / min a b = |a / b|ₘ
Tactic: rw [mabs_div_comm, max_div_min_eq_mabs']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
rw : max a b / min a b = |a / b|ₘ
⊢ max a b / min a b = |b / a|ₘ
have rw₁ : |a / b|ₘ = |a / b|ₘ
Tactic: rw [mabs_div_comm, max_div_min_eq_mabs']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a : α
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a
have rw : a * a⁻¹ ≤ a * 1 ↔ 1 ≤ a
Tactic: rw [← mul_le_mul_iff_left a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a : α
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1
have rw : a * 1 ≤ a * a⁻¹ ↔ a ≤ 1
Tactic: rw [← mul_le_mul_iff_left a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
⊢ b ≤ a⁻¹ * c ↔ a * b ≤ c
have rw : a * b ≤ a * (a⁻¹ * c) ↔ a * b ≤ c
Tactic: rw [← mul_le_mul_iff_left a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
⊢ b⁻¹ * a ≤ c ↔ a ≤ b * c
have rw : b * (b⁻¹ * a) ≤ b * c ↔ a ≤ b * c
Tactic: rw [← mul_le_mul_iff_left b, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
rw : b * (b⁻¹ * a) ≤ b * c ↔ a ≤ b * c
⊢ b⁻¹ * a ≤ c ↔ a ≤ b * c
have rw₁ : a ≤ b * c ↔ a ≤ b * c
Tactic: rw [← mul_le_mul_iff_left b, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b : α
⊢ a * a⁻¹ ≤ a * b ↔ 1 ≤ a * b
have rw : 1 ≤ a * b ↔ 1 ≤ a * b
Tactic: rw [mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b : α
⊢ b * a ≤ b * b⁻¹ ↔ b * a ≤ 1
have rw : b * a ≤ 1 ↔ b * a ≤ 1
Tactic: rw [mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b : α
⊢ 1 ≤ b⁻¹ * a ↔ b ≤ a
have rw : b * 1 ≤ b * (b⁻¹ * a) ↔ b ≤ a
Tactic: rw [← mul_le_mul_iff_left b, mul_one, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b : α
rw : b * 1 ≤ b * (b⁻¹ * a) ↔ b ≤ a
⊢ 1 ≤ b⁻¹ * a ↔ b ≤ a
have rw₁ : b ≤ b * (b⁻¹ * a) ↔ b ≤ a
Tactic: rw [← mul_le_mul_iff_left b, mul_one, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b : α
rw : b * 1 ≤ b * (b⁻¹ * a) ↔ b ≤ a
rw₁ : b ≤ b * (b⁻¹ * a) ↔ b ≤ a
⊢ 1 ≤ b⁻¹ * a ↔ b ≤ a
have rw₂ : b ≤ a ↔ b ≤ a
Tactic: rw [← mul_le_mul_iff_left b, mul_one, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b : α
⊢ b ≤ a * 1 ↔ b ≤ a
have rw : b ≤ a ↔ b ≤ a
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a : α
⊢ 1 < a⁻¹ ↔ a < 1
have rw : a * 1 < a * a⁻¹ ↔ a < 1
Tactic: rw [← mul_lt_mul_iff_left a, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a : α
rw : a * 1 < a * a⁻¹ ↔ a < 1
⊢ 1 < a⁻¹ ↔ a < 1
have rw₁ : a * 1 < 1 ↔ a < 1
Tactic: rw [← mul_lt_mul_iff_left a, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a : α
rw : a * 1 < a * a⁻¹ ↔ a < 1
rw₁ : a * 1 < 1 ↔ a < 1
⊢ 1 < a⁻¹ ↔ a < 1
have rw₂ : a < 1 ↔ a < 1
Tactic: rw [← mul_lt_mul_iff_left a, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a : α
⊢ a⁻¹ < 1 ↔ 1 < a
have rw : a * a⁻¹ < a * 1 ↔ 1 < a
Tactic: rw [← mul_lt_mul_iff_left a, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a : α
rw : a * a⁻¹ < a * 1 ↔ 1 < a
⊢ a⁻¹ < 1 ↔ 1 < a
have rw₁ : 1 < a * 1 ↔ 1 < a
Tactic: rw [← mul_lt_mul_iff_left a, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a : α
rw : a * a⁻¹ < a * 1 ↔ 1 < a
rw₁ : 1 < a * 1 ↔ 1 < a
⊢ a⁻¹ < 1 ↔ 1 < a
have rw₂ : 1 < a ↔ 1 < a
Tactic: rw [← mul_lt_mul_iff_left a, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
⊢ b < a⁻¹ * c ↔ a * b < c
have rw : a * b < a * (a⁻¹ * c) ↔ a * b < c
Tactic: rw [← mul_lt_mul_iff_left a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
⊢ b⁻¹ * a < c ↔ a < b * c
have rw : b * (b⁻¹ * a) < b * c ↔ a < b * c
Tactic: rw [← mul_lt_mul_iff_left b, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Basic (goal)
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
rw : b * (b⁻¹ * a) < b * c ↔ a < b * c
⊢ b⁻¹ * a < c ↔ a < b * c
have rw₁ : a < b * c ↔ a < b * c
Tactic: rw [← mul_lt_mul_iff_left b, mul_inv_cancel_left]