no goals
F : Type ?u.318482
α : Type u_1
β : Type ?u.318488
γ : Type ?u.318491
δ : Type ?u.318494
ε : Type ?u.318497
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
⊢ IsUnit f ↔ ∃ a, f = pure a
simp only [isUnit_iff, Group.isUnit, and_true_iff]