α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ abs a = a ⊔ a⁻¹ ⊔ 1
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ abs a = a⁺ * a⁻
rw [m_pos_part_def, sup_mul, one_mul, m_neg_part_def, mul_sup, mul_one, mul_inv_self, sup_assoc,
  ← @sup_assoc _ _ a, sup_eq_right.2 le_sup_right]
no goals
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ abs a = a ⊔ a⁻¹ ⊔ 1
exact (sup_eq_left.2 <| one_le_abs a).symm