[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
inst✝ : One 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
⊢ mulIndicator s f x = mulIndicator t g x
[PROOFSTEP]
simp only [*, hst.1 hxs, mulIndicator_of_mem]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
inst✝ : One 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
⊢ mulIndicator s f x = mulIndicator t g x
[PROOFSTEP]
simp only [mulIndicator_of_not_mem, hxs, mt hst.2 hxs]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
⊢ (fun i => mulIndicator (s i) f a) =ᶠ[atTop] fun x => mulIndicator (⋃ (i : ι), s i) f a
[PROOFSTEP]
classical exact hs.piecewise_eventually_eq_iUnion f 1 a
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
⊢ (fun i => mulIndicator (s i) f a) =ᶠ[atTop] fun x => mulIndicator (⋃ (i : ι), s i) f a
[PROOFSTEP]
exact hs.piecewise_eventually_eq_iUnion f 1 a
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Antitone s
f : α → β
a : α
⊢ (fun i => mulIndicator (s i) f a) =ᶠ[atTop] fun x => mulIndicator (⋂ (i : ι), s i) f a
[PROOFSTEP]
classical exact hs.piecewise_eventually_eq_iInter f 1 a
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Antitone s
f : α → β
a : α
⊢ (fun i => mulIndicator (s i) f a) =ᶠ[atTop] fun x => mulIndicator (⋂ (i : ι), s i) f a
[PROOFSTEP]
exact hs.piecewise_eventually_eq_iInter f 1 a
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
ι : Type u_5
inst✝ : One β
s : ι → Set α
f : α → β
a : α
⊢ (fun n => mulIndicator (⋃ (i : ι) (_ : i ∈ n), s i) f a) =ᶠ[atTop] fun x => mulIndicator (iUnion s) f a
[PROOFSTEP]
rw [iUnion_eq_iUnion_finset s]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
ι : Type u_5
inst✝ : One β
s : ι → Set α
f : α → β
a : α
⊢ (fun n => mulIndicator (⋃ (i : ι) (_ : i ∈ n), s i) f a) =ᶠ[atTop] fun x =>
    mulIndicator (⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), s i) f a
[PROOFSTEP]
apply Monotone.mulIndicator_eventuallyEq_iUnion
[GOAL]
case hs
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
ι : Type u_5
inst✝ : One β
s : ι → Set α
f : α → β
a : α
⊢ Monotone fun i => ⋃ (i_1 : ι) (_ : i_1 ∈ i), s i_1
[PROOFSTEP]
exact fun _ _ ↦ biUnion_subset_biUnion_left
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
inst✝ : One β
l : Filter α
f : α → β
s : Set α
hf : f =ᶠ[l] 1
⊢ mulIndicator s 1 =ᶠ[l] 1
[PROOFSTEP]
rw [mulIndicator_one']
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s t : Set α
h : mulIndicator s f =ᶠ[l] mulIndicator t f
⊢ s =ᶠ[l] t
[PROOFSTEP]
have : ∀ {s : Set α}, Function.mulSupport (s.mulIndicator f) =ᶠ[l] s := fun {s} ↦
  by
  rw [mulSupport_mulIndicator]
  exact (hf.mono fun x hx ↦ and_iff_left hx).set_eq
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s✝ t : Set α
h : mulIndicator s✝ f =ᶠ[l] mulIndicator t f
s : Set α
⊢ Function.mulSupport (mulIndicator s f) =ᶠ[l] s
[PROOFSTEP]
rw [mulSupport_mulIndicator]
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s✝ t : Set α
h : mulIndicator s✝ f =ᶠ[l] mulIndicator t f
s : Set α
⊢ s ∩ Function.mulSupport f =ᶠ[l] s
[PROOFSTEP]
exact (hf.mono fun x hx ↦ and_iff_left hx).set_eq
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
E : Type u_4
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s t : Set α
h : mulIndicator s f =ᶠ[l] mulIndicator t f
this : ∀ {s : Set α}, Function.mulSupport (mulIndicator s f) =ᶠ[l] s
⊢ s =ᶠ[l] t
[PROOFSTEP]
exact this.symm.trans <| h.mulSupport.trans this
