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

State before:
𝕂 : Type u_1
inst✝² : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
f : ℝ → E
h : Function.support f ⊆ Icc a b
hs : Icc a b ⊆ s
⊢ ∫ (x : ℝ) in s, f x ∂μ = ∫ (x : ℝ) in Icc a b, f x ∂μ
Tactic:
rw [SetIntegral.integral_eq_integral_inter_of_support_subset h measurableSet_Icc,
    inter_eq_self_of_subset_right hs]
State after:
no goals