no goals
F : Type ?u.557283
α : Type u_1
β : Type ?u.557289
γ : Type ?u.557292
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DivisionMonoid α
s t : Finset α
⊢ s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
simp_rw [← coe_inj, coe_mul, coe_one, Set.mul_eq_one_iff, coe_singleton]