no goals
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α Mul.mul LE.le
a : α
⊢ a⁻ = 1 ↔ 1 ≤ a
rw [le_antisymm_iff, neg_le_one_iff, inv_le_one', and_iff_left (one_le_neg _)]