F : Type ?u.443848
α : Type u_2
β : Type u_1
γ : Type ?u.443857
δ : Type ?u.443860
ε : Type ?u.443863
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
hg : NeBot g
s : Set β
hs : s ∈ g
⊢ {0} ∈ 0
F : Type ?u.443848
α : Type u_2
β : Type u_1
γ : Type ?u.443857
δ : Type ?u.443860
ε : Type ?u.443863
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
hg : NeBot g
s : Set β
hs : s ∈ g
⊢ (fun x x_1 => x • x_1) 0 '' s ∈ 0
simp_rw [zero_smul, (hg.nonempty_of_mem hs).image_const]
no goals
F : Type ?u.443848
α : Type u_2
β : Type u_1
γ : Type ?u.443857
δ : Type ?u.443860
ε : Type ?u.443863
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
hg : NeBot g
s : Set β
hs : s ∈ g
⊢ {0} ∈ 0
exact zero_mem_zero