no goals
F : Type ?u.7176
α : Type u_1
β : Type ?u.7182
γ : Type ?u.7185
inst✝ : InvolutiveInv α
s✝ t : Set α
a✝ a : α
s : Set α
⊢ (insert a s)⁻¹ = insert a⁻¹ s⁻¹
rw [insert_eq, union_inv, inv_singleton, insert_eq]