α : Type u_1
β : Type u_2
γ : Type ?u.1049718
γ₂ : Type ?u.1049721
δ : Type ?u.1049724
ι : Sort y
s t u : Set α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : MeasurableSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
⊢ Prod.instMeasurableSpace ≤ borel (α × β)
α : Type u_1
β : Type u_2
γ : Type ?u.1049718
γ₂ : Type ?u.1049721
δ : Type ?u.1049724
ι : Sort y
s t u : Set α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : MeasurableSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
⊢ Prod.instMeasurableSpace ≤ borel (α × β)
rw [‹BorelSpace α›.measurable_eq, ‹BorelSpace β›.measurable_eq]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.1049718
γ₂ : Type ?u.1049721
δ : Type ?u.1049724
ι : Sort y
s t u : Set α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : MeasurableSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
⊢ MeasurableSpace.comap Prod.fst (borel α) ≤ borel (α × β)

case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.1049718
γ₂ : Type ?u.1049721
δ : Type ?u.1049724
ι : Sort y
s t u : Set α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : MeasurableSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
⊢ MeasurableSpace.comap Prod.snd (borel β) ≤ borel (α × β)
α : Type u_1
β : Type u_2
γ : Type ?u.1049718
γ₂ : Type ?u.1049721
δ : Type ?u.1049724
ι : Sort y
s t u : Set α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : MeasurableSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
⊢ Prod.instMeasurableSpace ≤ borel (α × β)
refine' sup_le _ _
no goals
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.1049718
γ₂ : Type ?u.1049721
δ : Type ?u.1049724
ι : Sort y
s t u : Set α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : MeasurableSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
⊢ MeasurableSpace.comap Prod.fst (borel α) ≤ borel (α × β)
exact comap_le_iff_le_map.mpr continuous_fst.borel_measurable
no goals
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.1049718
γ₂ : Type ?u.1049721
δ : Type ?u.1049724
ι : Sort y
s t u : Set α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : MeasurableSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
⊢ MeasurableSpace.comap Prod.snd (borel β) ≤ borel (α × β)
exact comap_le_iff_le_map.mpr continuous_snd.borel_measurable