case inl
ι : Type ?u.1842380
𝕜 : Type ?u.1842383
E : Type u_1
F : Type ?u.1842389
A : Type ?u.1842392
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hint : IntervalIntegrable f' volume a b
hab : a ≤ b
⊢ (∫ (y : ℝ) in a..b, f' y) = f b - f a

case inr
ι : Type ?u.1842380
𝕜 : Type ?u.1842383
E : Type u_1
F : Type ?u.1842389
A : Type ?u.1842392
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hint : IntervalIntegrable f' volume a b
hab : b ≤ a
⊢ (∫ (y : ℝ) in a..b, f' y) = f b - f a
ι : Type ?u.1842380
𝕜 : Type ?u.1842383
E : Type u_1
F : Type ?u.1842389
A : Type ?u.1842392
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hint : IntervalIntegrable f' volume a b
⊢ (∫ (y : ℝ) in a..b, f' y) = f b - f a
cases' le_total a b with hab hab
case inl
ι : Type ?u.1842380
𝕜 : Type ?u.1842383
E : Type u_1
F : Type ?u.1842389
A : Type ?u.1842392
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hint : IntervalIntegrable f' volume a b
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt f (f' x) (Ioi x) x
⊢ (∫ (y : ℝ) in a..b, f' y) = f b - f a
case inl
ι : Type ?u.1842380
𝕜 : Type ?u.1842383
E : Type u_1
F : Type ?u.1842389
A : Type ?u.1842392
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hint : IntervalIntegrable f' volume a b
hab : a ≤ b
⊢ (∫ (y : ℝ) in a..b, f' y) = f b - f a
simp only [uIcc_of_le, min_eq_left, max_eq_right, hab] at hcont hderiv hint
no goals
case inl
ι : Type ?u.1842380
𝕜 : Type ?u.1842383
E : Type u_1
F : Type ?u.1842389
A : Type ?u.1842392
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hint : IntervalIntegrable f' volume a b
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt f (f' x) (Ioi x) x
⊢ (∫ (y : ℝ) in a..b, f' y) = f b - f a
apply integral_eq_sub_of_hasDeriv_right_of_le hab hcont hderiv hint
case inr
ι : Type ?u.1842380
𝕜 : Type ?u.1842383
E : Type u_1
F : Type ?u.1842389
A : Type ?u.1842392
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hint : IntervalIntegrable f' volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ (x : ℝ), x ∈ Ioo b a → HasDerivWithinAt f (f' x) (Ioi x) x
⊢ (∫ (y : ℝ) in a..b, f' y) = f b - f a
case inr
ι : Type ?u.1842380
𝕜 : Type ?u.1842383
E : Type u_1
F : Type ?u.1842389
A : Type ?u.1842392
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hint : IntervalIntegrable f' volume a b
hab : b ≤ a
⊢ (∫ (y : ℝ) in a..b, f' y) = f b - f a
simp only [uIcc_of_ge, min_eq_right, max_eq_left, hab] at hcont hderiv
no goals
case inr
ι : Type ?u.1842380
𝕜 : Type ?u.1842383
E : Type u_1
F : Type ?u.1842389
A : Type ?u.1842392
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hint : IntervalIntegrable f' volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ (x : ℝ), x ∈ Ioo b a → HasDerivWithinAt f (f' x) (Ioi x) x
⊢ (∫ (y : ℝ) in a..b, f' y) = f b - f a
rw [integral_symm, integral_eq_sub_of_hasDeriv_right_of_le hab hcont hderiv hint.symm, neg_sub]