G : Type ?u.2153121
α✝ : Type ?u.2153124
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m✝ : MeasurableSpace α✝
f✝ g✝ : α✝ → G
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
hm : m ≤ m0
f g : α → E
hf : Measurable f
hg : Measurable g
hfg : f =ᵐ[μ] g
⊢ MeasurableSet {a | ¬f a = g a}
G : Type ?u.2153121
α✝ : Type ?u.2153124
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m✝ : MeasurableSpace α✝
f✝ g✝ : α✝ → G
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
hm : m ≤ m0
f g : α → E
hf : Measurable f
hg : Measurable g
hfg : f =ᵐ[μ] g
⊢ f =ᵐ[Measure.trim μ hm] g
rwa [Filter.EventuallyEq, @ae_iff _ m, trim_measurableSet_eq hm _]
no goals
G : Type ?u.2153121
α✝ : Type ?u.2153124
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m✝ : MeasurableSpace α✝
f✝ g✝ : α✝ → G
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
hm : m ≤ m0
f g : α → E
hf : Measurable f
hg : Measurable g
hfg : f =ᵐ[μ] g
⊢ MeasurableSet {a | ¬f a = g a}
exact @MeasurableSet.compl α _ m (@measurableSet_eq_fun α m E _ _ _ _ _ _ hf hg)