no goals
F : Type ?u.40275
α : Type u_1
β : Type ?u.40281
γ : Type ?u.40284
inst✝¹ : DecidableEq α
inst✝ : InvolutiveInv α
s : Finset α
⊢ ↑(preimage s Inv.inv (_ : Set.InjOn Inv.inv (Inv.inv ⁻¹' ↑s))) = ↑s⁻¹
rw [coe_preimage, Set.inv_preimage, coe_inv]