awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
a₁ : a * b ≤ |a|ₘ * |b|ₘ
a₂ : (a * b)⁻¹ ≤ |a|ₘ * |b|ₘ
⊢ |a * b|ₘ ≤ |a|ₘ * |b|ₘ

Tactic:
apply sup_le

Premises used: sup_le
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ a * b ≤ |a|ₘ * |b|ₘ

Tactic:
mul_le_mul' (le_mabs_self a) (le_mabs_self b)

Premises used: le_mabs_self, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ a * b ≤ |a|ₘ * |b|ₘ

Tactic:
exact mul_le_mul' (le_mabs_self a) (le_mabs_self b)

Premises used: le_mabs_self, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
a₁ : a⁻¹ * b⁻¹ ≤ |a|ₘ * |b|ₘ
⊢ (a * b)⁻¹ ≤ |a|ₘ * |b|ₘ

Tactic:
rw [mul_inv]

Premises used: mul_inv
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ a⁻¹ * b⁻¹ ≤ |a|ₘ * |b|ₘ

Tactic:
mul_le_mul' (inv_le_mabs _) (inv_le_mabs _)

Premises used: inv_le_mabs, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ a⁻¹ * b⁻¹ ≤ |a|ₘ * |b|ₘ

Tactic:
exact mul_le_mul' (inv_le_mabs _) (inv_le_mabs _)

Premises used: inv_le_mabs, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : |a|ₘ / |b|ₘ ≤ |a / b|ₘ ∧ (|a|ₘ / |b|ₘ)⁻¹ ≤ |a / b|ₘ
⊢ ||a|ₘ / |b|ₘ|ₘ ≤ |a / b|ₘ

Tactic:
rw [mabs, sup_le_iff]

Premises used: sup_le_iff, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
left : |a|ₘ / |b|ₘ ≤ |a / b|ₘ
right : (|a|ₘ / |b|ₘ)⁻¹ ≤ |a / b|ₘ
⊢ |a|ₘ / |b|ₘ ≤ |a / b|ₘ ∧ (|a|ₘ / |b|ₘ)⁻¹ ≤ |a / b|ₘ

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
left : |a|ₘ ≤ |a / b|ₘ * |b|ₘ
⊢ |a|ₘ / |b|ₘ ≤ |a / b|ₘ

Tactic:
apply div_le_iff_le_mul.2

Premises used: Iff.mpr, div_le_iff_le_mul
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ |a / b * b|ₘ ≤ |a / b|ₘ * |b|ₘ

Tactic:
mabs_mul_le (a / b) b

Premises used: mabs_mul_le, HDiv.hDiv
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
h : a = a / b * b
⊢ |a|ₘ ≤ |a / b|ₘ * |b|ₘ

Tactic:
convert! mabs_mul_le (a / b) b

Premises used: mabs_mul_le, HDiv.hDiv
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
h h₁ : a = a
⊢ a = a / b * b

Tactic:
rw [div_mul_cancel]

Premises used: div_mul_cancel
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
right : |b|ₘ ≤ |b / a|ₘ * |a|ₘ
⊢ (|a|ₘ / |b|ₘ)⁻¹ ≤ |a / b|ₘ

Tactic:
rw [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_le_iff_le_mul, mabs_div_comm]

Premises used: mabs_div_comm, mul_inv_le_iff_le_mul, div_eq_mul_inv, inv_inv, mul_inv_rev
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ |b / a * a|ₘ ≤ |b / a|ₘ * |a|ₘ

Tactic:
mabs_mul_le (b / a) a

Premises used: mabs_mul_le, HDiv.hDiv
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
h : b = b / a * a
⊢ |b|ₘ ≤ |b / a|ₘ * |a|ₘ

Tactic:
convert! mabs_mul_le (b / a) a

Premises used: mabs_mul_le, HDiv.hDiv
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
h h₁ : b = b
⊢ b = b / a * a

Tactic:
rw [div_mul_cancel]

Premises used: div_mul_cancel
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
simp_rw : a / b ⊔ b / a ⊔ 1 = |b / a|ₘ
⊢ (a ⊔ b) / (a ⊓ b) = |b / a|ₘ

Tactic:
simp_rw [sup_div, div_inf, div_self', sup_comm, sup_sup_sup_comm, sup_idem]

Premises used: sup_sup_sup_comm, sup_idem, div_inf, div_self', sup_comm, sup_div
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : 1 ≤ |b / a|ₘ
⊢ a / b ⊔ b / a ⊔ 1 = |b / a|ₘ

Tactic:
rw [← inv_div, sup_comm (b := _ / _), ← mabs, sup_eq_left]

Premises used: HDiv.hDiv, sup_eq_left, sup_comm, inv_div, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ 1 ≤ |b / a|ₘ

Tactic:
one_le_mabs _

Premises used: one_le_mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ 1 ≤ |b / a|ₘ

Tactic:
exact one_le_mabs _

Premises used: one_le_mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * |b / a|ₘ
rw₁ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))
rw₂ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)
rw₃ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * (a ⊔ b) * (a ⊓ b)⁻¹
rw₄ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * (a ⊔ b) * (a ⊔ b))
rw₅ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * ((a ⊔ b) * (a ⊔ b)))
rw₆ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * HPow.hPow (β := ℕ) (a ⊔ b) 2)
rw₇ rw₈ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = HPow.hPow (β := ℕ) (a ⊔ b) 2
⊢ HPow.hPow (β := ℕ) (a ⊔ b) 2 = a * b * |b / a|ₘ

Tactic:
rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, ← mul_assoc, mul_comm,
     mul_assoc, ← pow_two, inv_mul_cancel_left]

Premises used: sup_div_inf_eq_mabs_div, pow_two, inv_mul_cancel_left, mul_assoc, div_eq_mul_inv, mul_comm, inf_mul_sup
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / |b / a|ₘ
rw₁ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / ((a ⊔ b) / (a ⊓ b))
rw₂ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))⁻¹
rw₃ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)⁻¹
rw₄ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊓ b)⁻¹⁻¹ * (a ⊔ b)⁻¹)
rw₅ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊓ b) * (a ⊔ b)⁻¹)
rw₆ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * ((a ⊔ b) * ((a ⊓ b) * (a ⊔ b)⁻¹))
rw₇ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊓ b)
rw₈ rw₉ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = HPow.hPow (β := ℕ) (a ⊓ b) 2
⊢ HPow.hPow (β := ℕ) (a ⊓ b) 2 = a * b / |b / a|ₘ

Tactic:
rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev,
    inv_inv, mul_assoc, mul_inv_cancel_comm_assoc, ← pow_two]

Premises used: sup_div_inf_eq_mabs_div, pow_two, mul_assoc, div_eq_mul_inv, mul_inv_cancel_comm_assoc, inv_inv, mul_inv_rev, inf_mul_sup
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
rw rw₁ : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ

Tactic:
rw [sup_div_inf_eq_mabs_div]

Premises used: sup_div_inf_eq_mabs_div
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
rw rw₁ :
  (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ =
    (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ 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)))

Tactic:
rw [sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)]

Premises used: sup_div_inf_eq_mabs_div, Min.min
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
rw :
  (b ⊔ c ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
rw₁ :
  (b ⊔ c ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
rw₂ :
  (b ⊔ (c ⊔ (a ⊔ c))) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
rw₃ :
  (b ⊔ (a ⊔ c ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
rw₄ :
  (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
rw₅ :
  (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
rw₆ :
  (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ (c ⊓ (a ⊓ c)))) =
    (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
rw₇ :
  (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))
rw₈ :
  (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ (a ⊓ c))) =
    (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
rw₉ rw₁₀ :
  (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ (a ⊓ c))) =
    (b ⊔ (a ⊔ c)) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ (a ⊓ 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:
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]

Premises used: sup_inf_right, sup_right_idem, sup_assoc, inf_comm, inf_sup_right, sup_comm, Max.max, inf_right_idem, inf_assoc, Min.min
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
rw rw₁ :
  (b ⊔ a ⊔ 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) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c))

Tactic:
rw [div_mul_div_comm]

Premises used: div_mul_div_comm
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
rw : ((b ⊔ a) ⊓ c) * (b ⊔ a ⊔ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)
rw₁ : (b ⊔ a) * c / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)
rw₂ : (b ⊔ a) * c / ((b ⊓ a ⊓ c) * (b ⊓ a ⊔ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)
rw₃ rw₄ : (b ⊔ a) * 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 / ((b ⊓ a) * c)

Tactic:
rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]

Premises used: Max.max, mul_comm, inf_mul_sup, Min.min
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
rw : (b ⊔ a) * c * ((b ⊓ a) * c)⁻¹ = (b ⊔ a) / (b ⊓ a)
rw₁ : (b ⊔ a) * c * (c⁻¹ * (b ⊓ a)⁻¹) = (b ⊔ a) / (b ⊓ a)
rw₂ : (b ⊔ a) * (c * (c⁻¹ * (b ⊓ a)⁻¹)) = (b ⊔ a) / (b ⊓ a)
rw₃ : (b ⊔ a) * (b ⊓ a)⁻¹ = (b ⊔ a) / (b ⊓ a)
rw₄ rw₅ : (b ⊔ a) / (b ⊓ a) = (b ⊔ a) / (b ⊓ a)
⊢ (b ⊔ a) * c / ((b ⊓ a) * c) = (b ⊔ a) / (b ⊓ a)

Tactic:
rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]

Premises used: mul_assoc, div_eq_mul_inv, mul_inv_rev, mul_inv_cancel_left
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
this : DistribLattice α := CommGroup.toDistribLattice α
rw rw₁ : |a / b|ₘ = |a / b|ₘ
⊢ (b ⊔ a) / (b ⊓ a) = |a / b|ₘ

Tactic:
rw [sup_div_inf_eq_mabs_div]

Premises used: sup_div_inf_eq_mabs_div
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
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)
c₇ : (b ⊔ a) / (b ⊓ a) = |a / b|ₘ
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |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]

Premises used: HMul.hMul, HDiv.hDiv, Max.max, Min.min
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
apply : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ ≤ |a / b|ₘ

Tactic:
apply le_of_mul_le_of_one_le_left _ (one_le_mabs _)

Premises used: le_of_mul_le_of_one_le_left
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
rw rw₁ : |a / b|ₘ ≤ |a / b|ₘ
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ

Tactic:
rw [mabs_div_sup_mul_mabs_div_inf]

Premises used: mabs_div_sup_mul_mabs_div_inf
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b c : α
apply : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ
⊢ |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ

Tactic:
apply le_of_mul_le_of_one_le_right _ (one_le_mabs _)

Premises used: le_of_mul_le_of_one_le_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
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|ₘ

Tactic:
sup_le (mabs_sup_div_sup_le_mabs a b c) (mabs_inf_div_inf_le_mabs a b c)

Premises used: mabs_inf_div_inf_le_mabs, sup_le, mabs_sup_div_sup_le_mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
x : α
⊢ |x|ₘ = x ∨ |x|ₘ = x⁻¹

Tactic:
max_choice _ _

Premises used: max_choice, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
a b : α
⊢ a ≤ |b|ₘ ↔ a ≤ b ∨ a ≤ b⁻¹

Tactic:
le_max_iff

Premises used: le_max_iff, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
a : α
⊢ |a|ₘ = max a a⁻¹

Tactic:
rfl

Premises used: rfl, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
a b : α
⊢ a < |b|ₘ ↔ a < b ∨ a < b⁻¹

Tactic:
lt_max_iff

Premises used: lt_max_iff, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
a : α
P : α → Prop
h1 : P a
h2 : P a⁻¹
⊢ P |a|ₘ

Tactic:
sup_ind _ _ h1 h2

Premises used: sup_ind, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
a b : α
h : |a|ₘ = b
⊢ a = b ∨ a = b⁻¹

Tactic:
simpa only [← h, eq_comm (a := |a|ₘ), inv_eq_iff_eq_inv] using mabs_choice a

Premises used: eq_comm, mabs_choice, inv_eq_iff_eq_inv
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
a b : α
h : a = b
⊢ |a|ₘ = |b|ₘ

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
a b : α
h : a = b⁻¹
⊢ |a|ₘ = |b|ₘ

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
a b : α
refine : ∀ (h : |a|ₘ = |b|ₘ), a = b ∨ a = b⁻¹
⊢ |a|ₘ = |b|ₘ ↔ a = b ∨ a = b⁻¹

Tactic:
refine ⟨fun h ↦ ?_, by rintro (h | h) <;> simp [h]⟩
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
a b : α
h : |a|ₘ = |b|ₘ
inl : ∀ (h : |(|b|ₘ)|ₘ = |b|ₘ), |b|ₘ = b ∨ |b|ₘ = b⁻¹
inr : ∀ (h : ||b|ₘ⁻¹|ₘ = |b|ₘ), |b|ₘ⁻¹ = b ∨ |b|ₘ⁻¹ = b⁻¹
⊢ a = b ∨ a = b⁻¹

Tactic:
obtain rfl | rfl := eq_or_eq_inv_of_mabs_eq h

Premises used: eq_or_eq_inv_of_mabs_eq, rfl
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
b : α
h : |(|b|ₘ)|ₘ = |b|ₘ
⊢ |b|ₘ = b ∨ |b|ₘ = b⁻¹

Tactic:
simpa only [inv_eq_iff_eq_inv (a := |b|ₘ), inv_inv, inv_inj, or_comm] using mabs_choice b

Premises used: inv_inj, inv_inv, mabs_choice, or_comm, inv_eq_iff_eq_inv
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
b : α
h : ||b|ₘ⁻¹|ₘ = |b|ₘ
⊢ |b|ₘ⁻¹ = b ∨ |b|ₘ⁻¹ = b⁻¹

Tactic:
simpa only [inv_eq_iff_eq_inv (a := |b|ₘ), inv_inv, inv_inj, or_comm] using mabs_choice b

Premises used: inv_inj, inv_inv, mabs_choice, or_comm, inv_eq_iff_eq_inv
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
a : α
⊢ IsSquare |a|ₘ ↔ IsSquare a

Tactic:
mabs_by_cases (IsSquare · ↔ _) Iff.rfl isSquare_inv

Premises used: Iff.rfl, isSquare_inv, mabs_by_cases, Iff, IsSquare
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
a b : α
⊢ |a|ₘ < b → a < b

Tactic:
(le_mabs_self _).trans_lt

Premises used: le_mabs_self, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
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)⁻¹ : β)
rw₃ 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|ₘ : β)

Tactic:
rw [mabs, mabs, (OrderHomClass.mono f).map_max, map_inv]

Premises used: map_inv, Monotone.map_max, OrderHomClass.mono, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
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
inr₁ : ∀ (ha : 1 < a), 1 < |a|ₘ ↔ a ≠ 1
⊢ 1 < |a|ₘ ↔ a ≠ 1

Tactic:
obtain ha | rfl | ha := lt_trichotomy a 1

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
ha : a < 1
⊢ 1 < |a|ₘ ↔ a ≠ 1

Tactic:
simp [mabs_of_lt_one ha, ha.ne, ha]

Premises used: mabs_of_lt_one, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
⊢ LT.lt.{u_1} (α := α) 1 |1|ₘ ↔ Ne.{u_1 + 1} (α := α) 1 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
ha : 1 < a
⊢ 1 < |a|ₘ ↔ a ≠ 1

Tactic:
simp [mabs_of_one_lt ha, ha, ha.ne']

Premises used: LT.lt.ne', mabs_of_one_lt
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
h : 1 < a
⊢ 1 < |a|ₘ

Tactic:
one_lt_mabs.2 h.ne'

Premises used: Iff.mpr, one_lt_mabs, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
h : a < 1
⊢ 1 < |a|ₘ

Tactic:
one_lt_mabs.2 h.ne

Premises used: Iff.mpr, one_lt_mabs, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
inl : ∀ (h : 1 ≤ a), |a|ₘ⁻¹ ≤ a
inr : ∀ (h : a ≤ 1), |a|ₘ⁻¹ ≤ a
⊢ |a|ₘ⁻¹ ≤ a

Tactic:
obtain h | h := le_total 1 a

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
h : 1 ≤ a
⊢ |a|ₘ⁻¹ ≤ a

Tactic:
simpa [mabs_of_one_le h] using (inv_le_one'.2 h).trans h

Premises used: Iff.mpr, inv_le_one', mabs_of_one_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
h : a ≤ 1
⊢ |a|ₘ⁻¹ ≤ a

Tactic:
simp [mabs_of_le_one h]

Premises used: mabs_of_le_one
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
grw : a * a⁻¹ ≤ a * |a|ₘ
grw₁ grw₂ : a * |a|ₘ ≤ a * |a|ₘ
⊢ 1 ≤ a * |a|ₘ

Tactic:
grw [← mul_inv_cancel a, inv_le_mabs a]

Premises used: inv_le_mabs, mul_inv_cancel
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
⊢ |a|ₘ⁻¹ ≤ a⁻¹

Tactic:
simpa using inv_mabs_le a⁻¹

Premises used: inv_mabs_le, Inv.inv
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
inst_3 : MulRightMono α
⊢ |a|ₘ ≠ 1 ↔ a ≠ 1

Tactic:
(one_le_mabs a).lt_iff_ne'.symm.trans one_lt_mabs

Premises used: one_lt_mabs, Iff.trans, one_le_mabs, LE.le.lt_iff_ne', Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
inst_3 : MulRightMono α
⊢ |a|ₘ = 1 ↔ a = 1

Tactic:
not_iff_not.1 mabs_ne_one

Premises used: not_iff_not, mabs_ne_one, Iff.mp