G : Type ?u.2047564
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m : MeasurableSpace α
f✝ g✝ : α → G
μ : MeasureTheory.Measure α
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
⊢ {x | AEMeasurable.mk f hf x = AEMeasurable.mk g hg x} =ᵐ[μ] {x | f x = g x}
G : Type ?u.2047564
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m : MeasurableSpace α
f✝ g✝ : α → G
μ : MeasureTheory.Measure α
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
⊢ NullMeasurableSet {x | f x = g x}
apply (measurableSet_eq_fun hf.measurable_mk hg.measurable_mk).nullMeasurableSet.congr
case h
G : Type ?u.2047564
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m : MeasurableSpace α
f✝ g✝ : α → G
μ : MeasureTheory.Measure α
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
x : α
hfx : f x = AEMeasurable.mk f hf x
hgx : g x = AEMeasurable.mk g hg x
⊢ setOf (fun x => AEMeasurable.mk f hf x = AEMeasurable.mk g hg x) x = setOf (fun x => f x = g x) x
G : Type ?u.2047564
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m : MeasurableSpace α
f✝ g✝ : α → G
μ : MeasureTheory.Measure α
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
⊢ {x | AEMeasurable.mk f hf x = AEMeasurable.mk g hg x} =ᵐ[μ] {x | f x = g x}
filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk]with x hfx hgx
case h
G : Type ?u.2047564
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m : MeasurableSpace α
f✝ g✝ : α → G
μ : MeasureTheory.Measure α
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
x : α
hfx : f x = AEMeasurable.mk f hf x
hgx : g x = AEMeasurable.mk g hg x
⊢ (AEMeasurable.mk f hf x = AEMeasurable.mk g hg x) = (f x = g x)
case h
G : Type ?u.2047564
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m : MeasurableSpace α
f✝ g✝ : α → G
μ : MeasureTheory.Measure α
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
x : α
hfx : f x = AEMeasurable.mk f hf x
hgx : g x = AEMeasurable.mk g hg x
⊢ setOf (fun x => AEMeasurable.mk f hf x = AEMeasurable.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
G : Type ?u.2047564
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m : MeasurableSpace α
f✝ g✝ : α → G
μ : MeasureTheory.Measure α
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
x : α
hfx : f x = AEMeasurable.mk f hf x
hgx : g x = AEMeasurable.mk g hg x
⊢ (AEMeasurable.mk f hf x = AEMeasurable.mk g hg x) = (f x = g x)
simp only [hfx, hgx]