case inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : Set.Countable s
Hc : ContinuousOn f [[a, b]]
Hd : ∀ (x : ℝ), x ∈ Set.Ioo (min a b) (max a b) \ s → HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
hab : a ≤ b
⊢ (∫ (x : ℝ) in a..b, f' x) = f b - f a

case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : Set.Countable s
Hc : ContinuousOn f [[a, b]]
Hd : ∀ (x : ℝ), x ∈ Set.Ioo (min a b) (max a b) \ s → HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
⊢ (∫ (x : ℝ) in a..b, f' x) = f b - f a
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : Set.Countable s
Hc : ContinuousOn f [[a, b]]
Hd : ∀ (x : ℝ), x ∈ Set.Ioo (min a b) (max a b) \ s → HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
⊢ (∫ (x : ℝ) in a..b, f' x) = f b - f a
cases' le_total a b with hab hab
case inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : Set.Countable s
Hi : IntervalIntegrable f' volume a b
hab : a ≤ b
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : ℝ), x ∈ Set.Ioo a b \ s → HasDerivAt f (f' x) x
⊢ (∫ (x : ℝ) in a..b, f' x) = f b - f a
case inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : Set.Countable s
Hc : ContinuousOn f [[a, b]]
Hd : ∀ (x : ℝ), x ∈ Set.Ioo (min a b) (max a b) \ s → HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
hab : a ≤ b
⊢ (∫ (x : ℝ) in a..b, f' x) = f b - f a
simp only [uIcc_of_le hab, min_eq_left hab, max_eq_right hab] at *
no goals
case inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : Set.Countable s
Hi : IntervalIntegrable f' volume a b
hab : a ≤ b
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ (x : ℝ), x ∈ Set.Ioo a b \ s → HasDerivAt f (f' x) x
⊢ (∫ (x : ℝ) in a..b, f' x) = f b - f a
exact integral_eq_of_hasDerivWithinAt_off_countable_of_le f f' hab hs Hc Hd Hi
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : Set.Countable s
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
Hc : ContinuousOn f (Set.Icc b a)
Hd : ∀ (x : ℝ), x ∈ Set.Ioo b a \ s → HasDerivAt f (f' x) x
⊢ (∫ (x : ℝ) in a..b, f' x) = f b - f a
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : Set.Countable s
Hc : ContinuousOn f [[a, b]]
Hd : ∀ (x : ℝ), x ∈ Set.Ioo (min a b) (max a b) \ s → HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
⊢ (∫ (x : ℝ) in a..b, f' x) = f b - f a
simp only [uIcc_of_ge hab, min_eq_right hab, max_eq_left hab] at *
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : Set.Countable s
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
Hc : ContinuousOn f (Set.Icc b a)
Hd : ∀ (x : ℝ), x ∈ Set.Ioo b a \ s → HasDerivAt f (f' x) x
⊢ (∫ (x : ℝ) in b..a, f' x) = f a - f b
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : Set.Countable s
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
Hc : ContinuousOn f (Set.Icc b a)
Hd : ∀ (x : ℝ), x ∈ Set.Ioo b a \ s → HasDerivAt f (f' x) x
⊢ (∫ (x : ℝ) in a..b, f' x) = f b - f a
rw [intervalIntegral.integral_symm, neg_eq_iff_eq_neg, neg_sub]
no goals
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : Set.Countable s
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
Hc : ContinuousOn f (Set.Icc b a)
Hd : ∀ (x : ℝ), x ∈ Set.Ioo b a \ s → HasDerivAt f (f' x) x
⊢ (∫ (x : ℝ) in b..a, f' x) = f a - f b
exact integral_eq_of_hasDerivWithinAt_off_countable_of_le f f' hab hs Hc Hd Hi.symm