α : Type u_2
β : Type ?u.341986
γ : Type ?u.341989
ι : Type ?u.341992
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ {x | AEStronglyMeasurable.mk f hf x = AEStronglyMeasurable.mk g hg x} =ᶠ[ae μ] {x | f x = g x}
α : Type u_2
β : Type ?u.341986
γ : Type ?u.341989
ι : Type ?u.341992
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ NullMeasurableSet {x | f x = g x}
apply
  (hf.stronglyMeasurable_mk.measurableSet_eq_fun
        hg.stronglyMeasurable_mk).nullMeasurableSet.congr
case h
α : Type u_2
β : Type ?u.341986
γ : Type ?u.341989
ι : Type ?u.341992
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
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 x => AEStronglyMeasurable.mk f hf x = AEStronglyMeasurable.mk g hg x) x = setOf (fun x => f x = g x) x
α : Type u_2
β : Type ?u.341986
γ : Type ?u.341989
ι : Type ?u.341992
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ {x | AEStronglyMeasurable.mk f hf x = AEStronglyMeasurable.mk g hg x} =ᶠ[ae μ] {x | f x = g x}
filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx
case h
α : Type u_2
β : Type ?u.341986
γ : Type ?u.341989
ι : Type ?u.341992
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
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.341986
γ : Type ?u.341989
ι : Type ?u.341992
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
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 x => AEStronglyMeasurable.mk f hf x = AEStronglyMeasurable.mk g hg x) x = setOf (fun x => f x = g x) x
change (hf.mk f x = hg.mk g x) = (f x = g x)
no goals
case h
α : Type u_2
β : Type ?u.341986
γ : Type ?u.341989
ι : Type ?u.341992
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
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]