rcases le_total a b with hab | hab
𝕂 : 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
h : Function.support f ⊆ Icc a b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
case inl
𝕂 : 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
h : Function.support f ⊆ Icc a b
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

case inr
𝕂 : 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
h : Function.support f ⊆ Icc a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ