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