F : Type ?u.441163
α : Type u_2
β : Type u_1
γ : Type ?u.441172
δ : Type ?u.441175
ε : Type ?u.441178
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
⊢ (fun x x_1 => x • x_1) 0 ⁻¹' s ∈ g
F : Type ?u.441163
α : Type u_2
β : Type u_1
γ : Type ?u.441172
δ : Type ?u.441175
ε : Type ?u.441178
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
⊢ 0 • g ≤ 0
refine' fun s hs => mem_smul_filter.2 _
case h.e'_4
F : Type ?u.441163
α : Type u_2
β : Type u_1
γ : Type ?u.441172
δ : Type ?u.441175
ε : Type ?u.441178
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
⊢ (fun x x_1 => x • x_1) 0 ⁻¹' s = univ
F : Type ?u.441163
α : Type u_2
β : Type u_1
γ : Type ?u.441172
δ : Type ?u.441175
ε : Type ?u.441178
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
⊢ (fun x x_1 => x • x_1) 0 ⁻¹' s ∈ g
convert @univ_mem _ g
case h.e'_4
F : Type ?u.441163
α : Type u_2
β : Type u_1
γ : Type ?u.441172
δ : Type ?u.441175
ε : Type ?u.441178
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
a : β
⊢ a ∈ (fun x x_1 => x • x_1) 0 ⁻¹' s
case h.e'_4
F : Type ?u.441163
α : Type u_2
β : Type u_1
γ : Type ?u.441172
δ : Type ?u.441175
ε : Type ?u.441178
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
⊢ (fun x x_1 => x • x_1) 0 ⁻¹' s = univ
refine' eq_univ_iff_forall.2 fun a => _
case h.e'_4
F : Type ?u.441163
α : Type u_2
β : Type u_1
γ : Type ?u.441172
δ : Type ?u.441175
ε : Type ?u.441178
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
a : β
⊢ a ∈ (fun x => 0 • x) ⁻¹' s
case h.e'_4
F : Type ?u.441163
α : Type u_2
β : Type u_1
γ : Type ?u.441172
δ : Type ?u.441175
ε : Type ?u.441178
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
a : β
⊢ a ∈ (fun x x_1 => x • x_1) 0 ⁻¹' s
dsimp only
no goals
case h.e'_4
F : Type ?u.441163
α : Type u_2
β : Type u_1
γ : Type ?u.441172
δ : Type ?u.441175
ε : Type ?u.441178
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
a : β
⊢ a ∈ (fun x => 0 • x) ⁻¹' s
rwa [mem_preimage, zero_smul]