Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: case inr
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
M : AntitoneOn f [[a, b]]
hab : b < a
⊢ IntegrableOn g (Icc (f a) (f b)) volume ↔ IntervalIntegrable g volume (f a) (f b)

pp: case inr.hf
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
M : AntitoneOn f [[a, b]]
hab : b < a
⊢ ContinuousOn f (Icc b a)

pp: case inr.hff'
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
M : AntitoneOn f [[a, b]]
hab : b < a
⊢ ∀ x ∈ Ioo b a, HasDerivAt f (f' x) x

pp: case inr.hf'
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
M : AntitoneOn f [[a, b]]
hab : b < a
⊢ ∀ x ∈ Ioo b a, f' x ≤ 0

pp: case inr.hab
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
M : AntitoneOn f [[a, b]]
hab : b < a
⊢ b ≤ a

Tactic:
intervalIntegrable_iff_integrableOn_Icc_of_le

Goal state after:
case inr
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
M : AntitoneOn f [[a, b]]
hab : b < a
⊢ IntegrableOn g (Icc (f a) (f b)) volume ↔ IntegrableOn g (Icc (f a) (f b)) volume

case inr
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
M : AntitoneOn f [[a, b]]
hab : b < a
⊢ f a ≤ f b

case inr.hf
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
M : AntitoneOn f [[a, b]]
hab : b < a
⊢ ContinuousOn f (Icc b a)

case inr.hff'
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
M : AntitoneOn f [[a, b]]
hab : b < a
⊢ ∀ x ∈ Ioo b a, HasDerivAt f (f' x) x

case inr.hf'
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
M : AntitoneOn f [[a, b]]
hab : b < a
⊢ ∀ x ∈ Ioo b a, f' x ≤ 0

case inr.hab
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
M : AntitoneOn f [[a, b]]
hab : b < a
⊢ b ≤ a