no goals
F : Type ?u.671388
α : Type u_1
β : Type ?u.671394
γ : Type ?u.671397
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage {b} ((fun x x_1 => x * x_1) a)
      (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun x x_1 => x * x_1) a ⁻¹' ↑{b})) =
    {a⁻¹ * b}
classical rw [← image_mul_left', image_singleton]
no goals
F : Type ?u.671388
α : Type u_1
β : Type ?u.671394
γ : Type ?u.671397
inst✝ : Group α
s t : Finset α
a b : α
⊢ preimage {b} ((fun x x_1 => x * x_1) a)
      (_ : Set.InjOn ((fun x x_1 => x * x_1) a) ((fun x x_1 => x * x_1) a ⁻¹' ↑{b})) =
    {a⁻¹ * b}
rw [← image_mul_left', image_singleton]