case h
α : Type u_3
α' : Type ?u.2388487
β : Type u_2
β' : Type ?u.2388493
γ✝ : Type ?u.2388496
E : Type ?u.2388499
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ✝
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ✝
inst✝² : NormedAddCommGroup E
γ : Type u_1
inst✝¹ : SigmaFinite ν
inst✝ : TopologicalSpace γ
f : α × β → γ
hf : AEStronglyMeasurable f (Measure.prod μ ν)
x : α
hx : ∀ᵐ (y : β) ∂ν, f (x, y) = AEStronglyMeasurable.mk f hf (x, y)
⊢ AEStronglyMeasurable (fun y => f (x, y)) ν
α : Type u_3
α' : Type ?u.2388487
β : Type u_2
β' : Type ?u.2388493
γ✝ : Type ?u.2388496
E : Type ?u.2388499
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ✝
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ✝
inst✝² : NormedAddCommGroup E
γ : Type u_1
inst✝¹ : SigmaFinite ν
inst✝ : TopologicalSpace γ
f : α × β → γ
hf : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ ∀ᵐ (x : α) ∂μ, AEStronglyMeasurable (fun y => f (x, y)) ν
filter_upwards [ae_ae_of_ae_prod hf.ae_eq_mk] with x hx
no goals
case h
α : Type u_3
α' : Type ?u.2388487
β : Type u_2
β' : Type ?u.2388493
γ✝ : Type ?u.2388496
E : Type ?u.2388499
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ✝
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ✝
inst✝² : NormedAddCommGroup E
γ : Type u_1
inst✝¹ : SigmaFinite ν
inst✝ : TopologicalSpace γ
f : α × β → γ
hf : AEStronglyMeasurable f (Measure.prod μ ν)
x : α
hx : ∀ᵐ (y : β) ∂ν, f (x, y) = AEStronglyMeasurable.mk f hf (x, y)
⊢ AEStronglyMeasurable (fun y => f (x, y)) ν
exact
  ⟨fun y => hf.mk f (x, y), hf.stronglyMeasurable_mk.comp_measurable measurable_prod_mk_left, hx⟩