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