no goals
F : Type ?u.673903
α : Type u_1
β : Type ?u.673909
γ : Type ?u.673912
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage {b} (fun x => x * a) (_ : Set.InjOn (fun x => x * a) ((fun x => x * a) ⁻¹' ↑{b})) = {b * a⁻¹}
classical rw [← image_mul_right', image_singleton]
no goals
F : Type ?u.673903
α : Type u_1
β : Type ?u.673909
γ : Type ?u.673912
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage {b} (fun x => x * a) (_ : Set.InjOn (fun x => x * a) ((fun x => x * a) ⁻¹' ↑{b})) = {b * a⁻¹}
rw [← image_mul_right', image_singleton]