no goals
α : Type u_1
β : Type ?u.51
M : Type u_2
E : Type ?u.57
inst✝ : Zero M
s t : Set α
f g : α → M
a : α
l : Filter α
hf : f =ᶠ[l ⊓ 𝓟 s] g
hs : s =ᶠ[l] t
x : α
hst : x ∈ s ↔ x ∈ t
hfg : x ∈ s → f x = g x
hxs : x ∈ s
⊢ indicator s f x = indicator t g x
simp only [*, hst.1 hxs, indicator_of_mem]
no goals
α : Type u_1
β : Type ?u.51
M : Type u_2
E : Type ?u.57
inst✝ : Zero M
s t : Set α
f g : α → M
a : α
l : Filter α
hf : f =ᶠ[l ⊓ 𝓟 s] g
hs : s =ᶠ[l] t
x : α
hst : x ∈ s ↔ x ∈ t
hfg : x ∈ s → f x = g x
hxs : ¬x ∈ s
⊢ indicator s f x = indicator t g x
simp only [indicator_of_not_mem hxs, indicator_of_not_mem (mt hst.2 hxs)]