no goals
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type ?u.20040
δ : Type ?u.20043
ε : Type ?u.20046
inst✝² : One α
f : Filter α
s : Set α
inst✝¹ : One β
inst✝ : OneHomClass F α β
φ : F
⊢ map (↑φ) 1 = 1
rw [Filter.map_one', map_one, pure_one]