no goals
F : Type ?u.682735
α : Type u_1
β : Type ?u.682741
γ : Type ?u.682744
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage 1 ((fun x x_1 => x * x_1) a⁻¹)
      (_ : Set.InjOn ((fun x x_1 => x * x_1) a⁻¹) ((fun x x_1 => x * x_1) a⁻¹ ⁻¹' ↑1)) =
    {a}
rw [preimage_mul_left_one, inv_inv]