α : Type u_1
β : Type ?u.58569
γ : Type ?u.58572
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ∃ a_1, a_1 ∈ a ∧ a_1⁻¹ = ma⁻¹
α : Type u_1
β : Type ?u.58569
γ : Type ?u.58572
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ma⁻¹ ∈ a⁻¹
simp [inv_def]
no goals
α : Type u_1
β : Type ?u.58569
γ : Type ?u.58572
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ∃ a_1, a_1 ∈ a ∧ a_1⁻¹ = ma⁻¹
aesop