no goals
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ max a 1 / max a⁻¹ 1 = a
rcases le_total a 1 with (h | h) <;> simp [h]