α : Type u_2
β : Type u_1
γ : Type ?u.342741
ι : Type ?u.342744
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f✝ g✝ : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ {a | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {a | f a < g a}
α : Type u_2
β : Type u_1
γ : Type ?u.342741
ι : Type ?u.342744
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f✝ g✝ : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ NullMeasurableSet {a | f a < g a}
apply
  (hf.stronglyMeasurable_mk.measurableSet_lt hg.stronglyMeasurable_mk).nullMeasurableSet.congr
case h
α : Type u_2
β : Type u_1
γ : Type ?u.342741
ι : Type ?u.342744
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f✝ g✝ : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ setOf (fun a => AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a) x = setOf (fun a => f a < g a) x
α : Type u_2
β : Type u_1
γ : Type ?u.342741
ι : Type ?u.342744
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f✝ g✝ : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ {a | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {a | f a < g a}
filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx
case h
α : Type u_2
β : Type u_1
γ : Type ?u.342741
ι : Type ?u.342744
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f✝ g✝ : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ (AEStronglyMeasurable.mk f hf x < AEStronglyMeasurable.mk g hg x) = (f x < g x)
case h
α : Type u_2
β : Type u_1
γ : Type ?u.342741
ι : Type ?u.342744
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f✝ g✝ : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ setOf (fun a => AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a) x = setOf (fun a => f a < g a) x
change (hf.mk f x < hg.mk g x) = (f x < g x)
no goals
case h
α : Type u_2
β : Type u_1
γ : Type ?u.342741
ι : Type ?u.342744
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f✝ g✝ : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ (AEStronglyMeasurable.mk f hf x < AEStronglyMeasurable.mk g hg x) = (f x < g x)
simp only [hfx, hgx]