no goals
F : Type ?u.622921
α : Type u_1
β : Type ?u.622927
γ : Type ?u.622930
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ image (fun b => a⁻¹ * b) t =
    preimage t (fun b => a * b) (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun b => a * b) ⁻¹' ↑t))
simp