case h
α : Type u_2
β : Type u_1
M : Type ?u.6683
E : Type ?u.6686
inst✝ : Zero β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
x : α
hx : f x = g x
⊢ Function.support f x = Function.support g x
α : Type u_2
β : Type u_1
M : Type ?u.6683
E : Type ?u.6686
inst✝ : Zero β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
⊢ Function.support f =ᶠ[l] Function.support g
filter_upwards [h]with x hx
case h
α : Type u_2
β : Type u_1
M : Type ?u.6683
E : Type ?u.6686
inst✝ : Zero β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
x : α
hx : f x = g x
⊢ Function.support f x ↔ Function.support g x
case h
α : Type u_2
β : Type u_1
M : Type ?u.6683
E : Type ?u.6686
inst✝ : Zero β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
x : α
hx : f x = g x
⊢ Function.support f x = Function.support g x
rw [eq_iff_iff]
case h
α : Type u_2
β : Type u_1
M : Type ?u.6683
E : Type ?u.6686
inst✝ : Zero β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
x : α
hx : f x = g x
⊢ f x ≠ 0 ↔ g x ≠ 0
case h
α : Type u_2
β : Type u_1
M : Type ?u.6683
E : Type ?u.6686
inst✝ : Zero β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
x : α
hx : f x = g x
⊢ Function.support f x ↔ Function.support g x
change f x ≠ 0 ↔ g x ≠ 0
no goals
case h
α : Type u_2
β : Type u_1
M : Type ?u.6683
E : Type ?u.6686
inst✝ : Zero β
f g : α → β
l : Filter α
h : f =ᶠ[l] g
x : α
hx : f x = g x
⊢ f x ≠ 0 ↔ g x ≠ 0
rw [hx]