no goals
F : Type ?u.613237
α : Type u_1
β : Type ?u.613243
γ : Type ?u.613246
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
f : F
s t : Finset α
a b : α
⊢ IsUnit s ↔ ∃ a, s = {a}
simp only [isUnit_iff, Group.isUnit, and_true_iff]