α : Type u_2
α' : Type ?u.4498752
β : Type u_1
β' : Type ?u.4498758
γ : Type ?u.4498761
E : Type ?u.4498764
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν✝
inst✝ : SigmaFinite μ
ν : Measure β
⊢ (bind 0 fun x => map (Prod.mk x) ν) = 0
α : Type u_2
α' : Type ?u.4498752
β : Type u_1
β' : Type ?u.4498758
γ : Type ?u.4498761
E : Type ?u.4498764
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν✝
inst✝ : SigmaFinite μ
ν : Measure β
⊢ Measure.prod 0 ν = 0
rw [Measure.prod]
no goals
α : Type u_2
α' : Type ?u.4498752
β : Type u_1
β' : Type ?u.4498758
γ : Type ?u.4498761
E : Type ?u.4498764
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν✝
inst✝ : SigmaFinite μ
ν : Measure β
⊢ (bind 0 fun x => map (Prod.mk x) ν) = 0
exact bind_zero_left _