Theorem: SetIntegral.integral_eq_integral_inter_of_support_subset (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : 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 ∂μ
Tactic:
rw [← setIntegral_indicator ht, indicator_eq_self.2 h]
State after:
no goals