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