-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
/-- A continuous function with compact support on a product space is strongly measurable for the
product sigma-algebra. The subtlety is that we do not assume that the spaces are separable, so the
product of the Borel sigma algebras might not contain all open sets, but still it contains enough
of them to approximate compactly supported continuous functions. -/
lemma _root_.HasCompactSupport.stronglyMeasurable_of_prod {X Y : Type*} [Zero α]
    [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y]
    [OpensMeasurableSpace X] [OpensMeasurableSpace Y] [TopologicalSpace α] [PseudoMetrizableSpace α]
    {f : X × Y → α} (hf : Continuous f) (h'f : HasCompactSupport f) :
    StronglyMeasurable f

Proof state:
α : Type u_1
X : Type u_5
Y : Type u_6
inst✝⁸ : Zero α
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetrizableSpace α
f : X × Y → α
hf : Continuous f
h'f : HasCompactSupport f
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ IsSeparable (range f)

Tactic:
letI : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α

Result:
α : Type u_1
X : Type u_5
Y : Type u_6
inst✝⁸ : Zero α
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetrizableSpace α
f : X × Y → α
hf : Continuous f
h'f : HasCompactSupport f
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
⊢ IsSeparable (range f)

Proof state:
α : Type u_1
X : Type u_5
Y : Type u_6
inst✝⁸ : Zero α
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetrizableSpace α
f : X × Y → α
hf : Continuous f
h'f : HasCompactSupport f
⊢ StronglyMeasurable f

Tactic:
borelize α

Result:
α : Type u_1
X : Type u_5
Y : Type u_6
inst✝⁸ : Zero α
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetrizableSpace α
f : X × Y → α
hf : Continuous f
h'f : HasCompactSupport f
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ StronglyMeasurable f

Proof state:
α : Type u_1
X : Type u_5
Y : Type u_6
inst✝⁸ : Zero α
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetrizableSpace α
f : X × Y → α
hf : Continuous f
h'f : HasCompactSupport f
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ StronglyMeasurable f

Tactic:
apply stronglyMeasurable_iff_measurable_separable.2 ⟨h'f.measurable_of_prod hf, ?_⟩

Result:
α : Type u_1
X : Type u_5
Y : Type u_6
inst✝⁸ : Zero α
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetrizableSpace α
f : X × Y → α
hf : Continuous f
h'f : HasCompactSupport f
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ IsSeparable (range f)

Proof state:
α : Type u_1
X : Type u_5
Y : Type u_6
inst✝⁸ : Zero α
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetrizableSpace α
f : X × Y → α
hf : Continuous f
h'f : HasCompactSupport f
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
⊢ IsSeparable (range f)

Tactic:
exact IsCompact.isSeparable (s := range f) (h'f.isCompact_range hf)

Result:
no goals