case inl
ι : Type ?u.10052960
𝕜 : Type ?u.10052963
E : Type u_1
F : Type ?u.10052969
A : Type ?u.10052972
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ✝ : MeasureTheory.Measure ℝ
f : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
h : a ≤ b
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = 1 • ∫ (x : ℝ) in Ι a b, f x ∂μ

case inr
ι : Type ?u.10052960
𝕜 : Type ?u.10052963
E : Type u_1
F : Type ?u.10052969
A : Type ?u.10052972
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ✝ : MeasureTheory.Measure ℝ
f : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
h : ¬a ≤ b
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = -1 • ∫ (x : ℝ) in Ι a b, f x ∂μ
ι : Type ?u.10052960
𝕜 : Type ?u.10052963
E : Type u_1
F : Type ?u.10052969
A : Type ?u.10052972
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ✝ : MeasureTheory.Measure ℝ
f : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ
split_ifs with h
no goals
case inl
ι : Type ?u.10052960
𝕜 : Type ?u.10052963
E : Type u_1
F : Type ?u.10052969
A : Type ?u.10052972
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ✝ : MeasureTheory.Measure ℝ
f : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
h : a ≤ b
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = 1 • ∫ (x : ℝ) in Ι a b, f x ∂μ
simp only [integral_of_le h, uIoc_of_le h, one_smul]
no goals
case inr
ι : Type ?u.10052960
𝕜 : Type ?u.10052963
E : Type u_1
F : Type ?u.10052969
A : Type ?u.10052972
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ : ℝ
f✝ g : ℝ → E
μ✝ : MeasureTheory.Measure ℝ
f : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
h : ¬a ≤ b
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = -1 • ∫ (x : ℝ) in Ι a b, f x ∂μ
simp only [integral_of_ge (not_le.1 h).le, uIoc_of_lt (not_le.1 h), neg_one_smul]