have : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ := by
  rw [ ← integral_indicator (by simp), indicator_eq_self.2 h]
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
⊢ 0 = ∫ (x : ℝ), f x ∂μ
case pos
𝕂 : Type u_1
inst✝⁴ : _root_.RCLike 𝕂
a b : ℝ
μ : Measure ℝ
inst✝³ : NoAtoms μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hab : b ≤ a
hab2 : b = a
h : Function.support f ⊆ {a}
this : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ
⊢ 0 = ∫ (x : ℝ), f x ∂μ