α : Type u
inst✝¹ : Lattice α
inst✝ : CommGroup α
a : α
h : 1 ≤ a⁻¹
⊢ a⁻¹⁺ = a⁻¹
α : Type u
inst✝¹ : Lattice α
inst✝ : CommGroup α
a : α
h : 1 ≤ a⁻¹
⊢ a⁻ = a⁻¹
rw [neg_eq_pos_inv]
no goals
α : Type u
inst✝¹ : Lattice α
inst✝ : CommGroup α
a : α
h : 1 ≤ a⁻¹
⊢ a⁻¹⁺ = a⁻¹
exact pos_of_one_le _ h