case inr
ι : Type ?u.16200147
𝕜 : Type ?u.16200150
E : Type u_1
F : Type ?u.16200156
A : Type ?u.16200159
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
ha : IntegrableOn f (Iic a)
hb : IntegrableOn f (Iic b)
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Iic a) →
      IntegrableOn f (Iic b) →
        a ≤ b → ((∫ (x : ℝ) in Iic b, f x ∂μ) - ∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : ¬a ≤ b
⊢ ((∫ (x : ℝ) in Iic b, f x ∂μ) - ∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ

ι : Type ?u.16200147
𝕜 : Type ?u.16200150
E : Type u_1
F : Type ?u.16200156
A : Type ?u.16200159
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
ha : IntegrableOn f (Iic a)
hb : IntegrableOn f (Iic b)
hab : a ≤ b
⊢ ((∫ (x : ℝ) in Iic b, f x ∂μ) - ∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
ι : Type ?u.16200147
𝕜 : Type ?u.16200150
E : Type u_1
F : Type ?u.16200156
A : Type ?u.16200159
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
ha : IntegrableOn f (Iic a)
hb : IntegrableOn f (Iic b)
⊢ ((∫ (x : ℝ) in Iic b, f x ∂μ) - ∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
wlog hab : a ≤ b generalizing a b
case ht
ι : Type ?u.16200147
𝕜 : Type ?u.16200150
E : Type u_1
F : Type ?u.16200156
A : Type ?u.16200159
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
ha : IntegrableOn f (Iic a)
hb : IntegrableOn f (Iic b)
hab : a ≤ b
⊢ MeasurableSet (Ioc a b)

case hfs
ι : Type ?u.16200147
𝕜 : Type ?u.16200150
E : Type u_1
F : Type ?u.16200156
A : Type ?u.16200159
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
ha : IntegrableOn f (Iic a)
hb : IntegrableOn f (Iic b)
hab : a ≤ b
⊢ IntegrableOn (fun x => f x) (Iic a)

case hft
ι : Type ?u.16200147
𝕜 : Type ?u.16200150
E : Type u_1
F : Type ?u.16200156
A : Type ?u.16200159
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
ha : IntegrableOn f (Iic a)
hb : IntegrableOn f (Iic b)
hab : a ≤ b
⊢ IntegrableOn (fun x => f x) (Ioc a b)
ι : Type ?u.16200147
𝕜 : Type ?u.16200150
E : Type u_1
F : Type ?u.16200156
A : Type ?u.16200159
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
ha : IntegrableOn f (Iic a)
hb : IntegrableOn f (Iic b)
hab : a ≤ b
⊢ ((∫ (x : ℝ) in Iic b, f x ∂μ) - ∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
rw [sub_eq_iff_eq_add', integral_of_le hab, ← integral_union (Iic_disjoint_Ioc le_rfl),
  Iic_union_Ioc_eq_Iic hab]
no goals
case ht
ι : Type ?u.16200147
𝕜 : Type ?u.16200150
E : Type u_1
F : Type ?u.16200156
A : Type ?u.16200159
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
ha : IntegrableOn f (Iic a)
hb : IntegrableOn f (Iic b)
hab : a ≤ b
⊢ MeasurableSet (Ioc a b)

case hfs
ι : Type ?u.16200147
𝕜 : Type ?u.16200150
E : Type u_1
F : Type ?u.16200156
A : Type ?u.16200159
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
ha : IntegrableOn f (Iic a)
hb : IntegrableOn f (Iic b)
hab : a ≤ b
⊢ IntegrableOn (fun x => f x) (Iic a)

case hft
ι : Type ?u.16200147
𝕜 : Type ?u.16200150
E : Type u_1
F : Type ?u.16200156
A : Type ?u.16200159
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a✝ b✝ c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
a b : ℝ
ha : IntegrableOn f (Iic a)
hb : IntegrableOn f (Iic b)
hab : a ≤ b
⊢ IntegrableOn (fun x => f x) (Ioc a b)
exacts [measurableSet_Ioc, ha, hb.mono_set fun _ => And.right]
no goals
case inr
ι : Type ?u.16200147
𝕜 : Type ?u.16200150
E : Type u_1
F : Type ?u.16200156
A : Type ?u.16200159
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
ha : IntegrableOn f (Iic a)
hb : IntegrableOn f (Iic b)
this :
  ∀ {a b : ℝ},
    IntegrableOn f (Iic a) →
      IntegrableOn f (Iic b) →
        a ≤ b → ((∫ (x : ℝ) in Iic b, f x ∂μ) - ∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : ¬a ≤ b
⊢ ((∫ (x : ℝ) in Iic b, f x ∂μ) - ∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
rw [integral_symm, ← this hb ha (le_of_not_le hab), neg_sub]