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