ι : Type ?u.1832713
𝕜 : Type ?u.1832716
E : Type ?u.1832719
F : Type ?u.1832722
A : Type ?u.1832725
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : ℝ → E
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b)
hφg : ∀ (x : ℝ), x ∈ Ioo a b → φ x ≤ g' x
⊢ -(g b - g a) ≤ -∫ (y : ℝ) in a..b, φ y
ι : Type ?u.1832713
𝕜 : Type ?u.1832716
E : Type ?u.1832719
F : Type ?u.1832722
A : Type ?u.1832725
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : ℝ → E
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b)
hφg : ∀ (x : ℝ), x ∈ Ioo a b → φ x ≤ g' x
⊢ (∫ (y : ℝ) in a..b, φ y) ≤ g b - g a
rw [← neg_le_neg_iff]
case h.e'_3
ι : Type ?u.1832713
𝕜 : Type ?u.1832716
E : Type ?u.1832719
F : Type ?u.1832722
A : Type ?u.1832725
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : ℝ → E
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b)
hφg : ∀ (x : ℝ), x ∈ Ioo a b → φ x ≤ g' x
⊢ -(g b - g a) = -g b - -g a

case h.e'_4
ι : Type ?u.1832713
𝕜 : Type ?u.1832716
E : Type ?u.1832719
F : Type ?u.1832722
A : Type ?u.1832725
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : ℝ → E
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b)
hφg : ∀ (x : ℝ), x ∈ Ioo a b → φ x ≤ g' x
⊢ (-∫ (y : ℝ) in a..b, φ y) = ∫ (y : ℝ) in a..b, (-φ) y
ι : Type ?u.1832713
𝕜 : Type ?u.1832716
E : Type ?u.1832719
F : Type ?u.1832722
A : Type ?u.1832725
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : ℝ → E
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b)
hφg : ∀ (x : ℝ), x ∈ Ioo a b → φ x ≤ g' x
⊢ -(g b - g a) ≤ -∫ (y : ℝ) in a..b, φ y
convert sub_le_integral_of_hasDeriv_right_of_le hab hcont.neg (fun x hx => (hderiv x hx).neg)
  φint.neg fun x hx => neg_le_neg (hφg x hx) using 1
no goals
case h.e'_3
ι : Type ?u.1832713
𝕜 : Type ?u.1832716
E : Type ?u.1832719
F : Type ?u.1832722
A : Type ?u.1832725
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : ℝ → E
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b)
hφg : ∀ (x : ℝ), x ∈ Ioo a b → φ x ≤ g' x
⊢ -(g b - g a) = -g b - -g a
abel
case h.e'_4
ι : Type ?u.1832713
𝕜 : Type ?u.1832716
E : Type ?u.1832719
F : Type ?u.1832722
A : Type ?u.1832725
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : ℝ → E
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b)
hφg : ∀ (x : ℝ), x ∈ Ioo a b → φ x ≤ g' x
⊢ (∫ (x : ℝ) in a..b, -φ x) = ∫ (y : ℝ) in a..b, (-φ) y
case h.e'_4
ι : Type ?u.1832713
𝕜 : Type ?u.1832716
E : Type ?u.1832719
F : Type ?u.1832722
A : Type ?u.1832725
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : ℝ → E
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b)
hφg : ∀ (x : ℝ), x ∈ Ioo a b → φ x ≤ g' x
⊢ (-∫ (y : ℝ) in a..b, φ y) = ∫ (y : ℝ) in a..b, (-φ) y
simp only [← integral_neg]
no goals
case h.e'_4
ι : Type ?u.1832713
𝕜 : Type ?u.1832716
E : Type ?u.1832719
F : Type ?u.1832722
A : Type ?u.1832725
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : ℝ → E
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b)
hφg : ∀ (x : ℝ), x ∈ Ioo a b → φ x ≤ g' x
⊢ (∫ (x : ℝ) in a..b, -φ x) = ∫ (y : ℝ) in a..b, (-φ) y
rfl