case inl
ι : Type ?u.1879888
𝕜 : Type ?u.1879891
E : Type ?u.1879894
F : Type ?u.1879897
A : Type ?u.1879900
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivAt g (g' x) x
hpos : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → 0 ≤ g' x
hab : a ≤ b
⊢ IntervalIntegrable g' volume a b

case inr
ι : Type ?u.1879888
𝕜 : Type ?u.1879891
E : Type ?u.1879894
F : Type ?u.1879897
A : Type ?u.1879900
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivAt g (g' x) x
hpos : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → 0 ≤ g' x
hab : b ≤ a
⊢ IntervalIntegrable g' volume a b
ι : Type ?u.1879888
𝕜 : Type ?u.1879891
E : Type ?u.1879894
F : Type ?u.1879897
A : Type ?u.1879900
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivAt g (g' x) x
hpos : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → 0 ≤ g' x
⊢ IntervalIntegrable g' volume a b
cases' le_total a b with hab hab
case inl
ι : Type ?u.1879888
𝕜 : Type ?u.1879891
E : Type ?u.1879894
F : Type ?u.1879897
A : Type ?u.1879900
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hpos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
⊢ IntegrableOn g' (Ioc a b)
case inl
ι : Type ?u.1879888
𝕜 : Type ?u.1879891
E : Type ?u.1879894
F : Type ?u.1879897
A : Type ?u.1879900
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivAt g (g' x) x
hpos : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → 0 ≤ g' x
hab : a ≤ b
⊢ IntervalIntegrable g' volume a b
simp only [uIcc_of_le, min_eq_left, max_eq_right, hab, IntervalIntegrable, hab,
  Ioc_eq_empty_of_le, integrableOn_empty, and_true_iff] at hcont hderiv hpos ⊢
no goals
case inl
ι : Type ?u.1879888
𝕜 : Type ?u.1879891
E : Type ?u.1879894
F : Type ?u.1879897
A : Type ?u.1879900
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hpos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
⊢ IntegrableOn g' (Ioc a b)
exact integrableOn_deriv_of_nonneg hcont hderiv hpos
case inr
ι : Type ?u.1879888
𝕜 : Type ?u.1879891
E : Type ?u.1879894
F : Type ?u.1879897
A : Type ?u.1879900
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : b ≤ a
hcont : ContinuousOn g (Icc b a)
hderiv : ∀ (x : ℝ), x ∈ Ioo b a → HasDerivAt g (g' x) x
hpos : ∀ (x : ℝ), x ∈ Ioo b a → 0 ≤ g' x
⊢ IntegrableOn g' (Ioc b a)
case inr
ι : Type ?u.1879888
𝕜 : Type ?u.1879891
E : Type ?u.1879894
F : Type ?u.1879897
A : Type ?u.1879900
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivAt g (g' x) x
hpos : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → 0 ≤ g' x
hab : b ≤ a
⊢ IntervalIntegrable g' volume a b
simp only [uIcc_of_ge, min_eq_right, max_eq_left, hab, IntervalIntegrable, Ioc_eq_empty_of_le,
  integrableOn_empty, true_and_iff] at hcont hderiv hpos ⊢
no goals
case inr
ι : Type ?u.1879888
𝕜 : Type ?u.1879891
E : Type ?u.1879894
F : Type ?u.1879897
A : Type ?u.1879900
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : b ≤ a
hcont : ContinuousOn g (Icc b a)
hderiv : ∀ (x : ℝ), x ∈ Ioo b a → HasDerivAt g (g' x) x
hpos : ∀ (x : ℝ), x ∈ Ioo b a → 0 ≤ g' x
⊢ IntegrableOn g' (Ioc b a)
exact integrableOn_deriv_of_nonneg hcont hderiv hpos