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 : α
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)
⊢ HPow.hPow (β := ℕ) (a ⊓ b) 2 = a * b / |b / a|ₘ
have rw₈ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = HPow.hPow (β := ℕ) (a ⊓ b) 2
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]
-- 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 α
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ
have rw : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ
Tactic: 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 α
⊢ (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)))
have 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)|ₘ
Tactic: rw [sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)]
-- 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 α
⊢ (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))
have 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))
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]
-- 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 α
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))
⊢ (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))
have 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))
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]
-- 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 α
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))
⊢ (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))
have 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))
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]
-- 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 α
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))
⊢ (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))
have 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))
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]
-- 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 α
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))
⊢ (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))
have 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))
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]
-- 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 α
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))
⊢ (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))
have 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))
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]
-- 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 α
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))
⊢ (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))
have 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))
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]
-- 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 α
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))
⊢ (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))
have 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))
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]
-- 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 α
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))
⊢ (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))
have 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))
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]
-- 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 α
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))
⊢ (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))
have 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)))
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]
-- 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 α
⊢ (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c))
have 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))
Tactic: rw [div_mul_div_comm]
-- 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 α
⊢ (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)
have rw : ((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]
-- 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 α
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)
have rw₁ : (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]
-- 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 α
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)
⊢ (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)
have rw₂ : (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]
-- 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 α
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)
⊢ (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)
have rw₃ : (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]
-- 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 α
⊢ (b ⊔ a) * c / ((b ⊓ a) * c) = (b ⊔ a) / (b ⊓ a)
have rw : (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]
-- 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 α
rw : (b ⊔ a) * c * ((b ⊓ a) * c)⁻¹ = (b ⊔ a) / (b ⊓ a)
⊢ (b ⊔ a) * c / ((b ⊓ a) * c) = (b ⊔ a) / (b ⊓ a)
have rw₁ : (b ⊔ a) * c * (c⁻¹ * (b ⊓ a)⁻¹) = (b ⊔ a) / (b ⊓ a)
Tactic: rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
-- 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 α
rw : (b ⊔ a) * c * ((b ⊓ a) * c)⁻¹ = (b ⊔ a) / (b ⊓ a)
rw₁ : (b ⊔ a) * c * (c⁻¹ * (b ⊓ a)⁻¹) = (b ⊔ a) / (b ⊓ a)
⊢ (b ⊔ a) * c / ((b ⊓ a) * c) = (b ⊔ a) / (b ⊓ a)
have rw₂ : (b ⊔ a) * (c * (c⁻¹ * (b ⊓ a)⁻¹)) = (b ⊔ a) / (b ⊓ a)
Tactic: rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
-- 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 α
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)
⊢ (b ⊔ a) * c / ((b ⊓ a) * c) = (b ⊔ a) / (b ⊓ a)
have rw₃ : (b ⊔ a) * (b ⊓ a)⁻¹ = (b ⊔ a) / (b ⊓ a)
Tactic: rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
-- 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 α
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)
⊢ (b ⊔ a) * c / ((b ⊓ a) * c) = (b ⊔ a) / (b ⊓ a)
have rw₄ : (b ⊔ a) / (b ⊓ a) = (b ⊔ a) / (b ⊓ a)
Tactic: rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
-- 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 α
⊢ (b ⊔ a) / (b ⊓ a) = |a / b|ₘ
have rw : |a / b|ₘ = |a / b|ₘ
Tactic: 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 α
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ
have c₁ : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ 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)|ₘ
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ
have 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: 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]