α : Type u_1
β : Type ?u.141288
γ : Type ?u.141291
δ : Type ?u.141294
ι : Type ?u.141297
R : Type ?u.141300
R' : Type ?u.141303
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
hs : MeasurableSet s
ht : ↑↑(ν + μ) t ≠ ⊤
⊢ ↑↑ν (toMeasurable (ν + μ) t ∩ s) = ↑↑ν (t ∩ s)
α : Type u_1
β : Type ?u.141288
γ : Type ?u.141291
δ : Type ?u.141294
ι : Type ?u.141297
R : Type ?u.141300
R' : Type ?u.141303
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
hs : MeasurableSet s
ht : ↑↑(μ + ν) t ≠ ⊤
⊢ ↑↑ν (toMeasurable (μ + ν) t ∩ s) = ↑↑ν (t ∩ s)
rw [add_comm] at ht⊢
no goals
α : Type u_1
β : Type ?u.141288
γ : Type ?u.141291
δ : Type ?u.141294
ι : Type ?u.141297
R : Type ?u.141300
R' : Type ?u.141303
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
hs : MeasurableSet s
ht : ↑↑(ν + μ) t ≠ ⊤
⊢ ↑↑ν (toMeasurable (ν + μ) t ∩ s) = ↑↑ν (t ∩ s)
exact measure_toMeasurable_add_inter_left hs ht