no goals
F : Type ?u.626033
α : Type u_1
β : Type ?u.626039
γ : Type ?u.626042
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