rw [← setIntegral_indicator ht, indicator_eq_self.2 h]
𝕂 : Type u_1
inst✝² : _root_.RCLike 𝕂
μ : Measure ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set ℝ
f : ℝ → E
h : Function.support f ⊆ t
ht : MeasurableSet t
⊢ ∫ (x : ℝ) in s, f x ∂μ = ∫ (x : ℝ) in s ∩ t, f x ∂μ
no goals