case inl
ι : Type ?u.16437814
𝕜 : Type ?u.16437817
E : Type u_1
F : Type ?u.16437823
A : Type ?u.16437826
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : a ≤ b
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ

case inr
ι : Type ?u.16437814
𝕜 : Type ?u.16437817
E : Type u_1
F : Type ?u.16437823
A : Type ?u.16437826
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : b ≤ a
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ
ι : Type ?u.16437814
𝕜 : Type ?u.16437817
E : Type u_1
F : Type ?u.16437823
A : Type ?u.16437826
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ
cases' le_total a b with hab hab
no goals
case inl
ι : Type ?u.16437814
𝕜 : Type ?u.16437817
E : Type u_1
F : Type ?u.16437823
A : Type ?u.16437826
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : a ≤ b
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ
rw [integral_of_le hab, ← integral_indicator measurableSet_Ioc, indicator_eq_self.2 h]
case inr
ι : Type ?u.16437814
𝕜 : Type ?u.16437817
E : Type u_1
F : Type ?u.16437823
A : Type ?u.16437826
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
h : f = 0
hab : b ≤ a
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ
case inr
ι : Type ?u.16437814
𝕜 : Type ?u.16437817
E : Type u_1
F : Type ?u.16437823
A : Type ?u.16437826
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : b ≤ a
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ
rw [Ioc_eq_empty hab.not_lt, subset_empty_iff, support_eq_empty_iff] at h
no goals
case inr
ι : Type ?u.16437814
𝕜 : Type ?u.16437817
E : Type u_1
F : Type ?u.16437823
A : Type ?u.16437826
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
h : f = 0
hab : b ≤ a
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ
simp [h]