awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : a ≤ b
inl inl₁ inl₂ inl₃ :
  ∀ (hf : ContinuousOn f (Icc 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), 0 ≤ f' x) (M : MonotoneOn f [[a, b]]) (hab : a ≤ b), ContinuousOn f (Icc a b)
⊢ ContinuousOn f (Icc a b)

Tactic:
rwa [uIcc_of_le hab] at hf

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : a ≤ b
⊢ ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : a ≤ b
⊢ ∀ x ∈ Ioo a b, 0 ≤ f' x

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : a ≤ b
⊢ a ≤ b

Tactic:
hab
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : a ≤ b
⊢ a ≤ b

Tactic:
exact hab
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
inr : f b ≤ f a
inr₁ : ContinuousOn f (Icc b a)
inr₂ : ∀ x ∈ Ioo b a, HasDerivAt f (f' x) x
inr₃ : ∀ x ∈ Ioo b a, 0 ≤ f' x
inr₄ : b ≤ a
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
rw [integral_of_ge hab.le, ← integral_Icc_eq_integral_Ioc,
      integral_Icc_deriv_smul_of_deriv_nonneg, integral_of_ge, ← integral_Icc_eq_integral_Ioc]

Premises used: MeasureTheory.integral_Icc_deriv_smul_of_deriv_nonneg, LT.lt.le, intervalIntegral.integral_of_ge, MeasureTheory.integral_Icc_eq_integral_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
⊢ f b ≤ f a

Tactic:
apply M right_mem_uIcc left_mem_uIcc hab.le

Premises used: Set.right_mem_uIcc, LT.lt.le, Set.left_mem_uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
inr inr₁ inr₂ inr₃ :
  ∀ (hf : ContinuousOn f (Icc b a)) (hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x)
    (hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x) (M : MonotoneOn f [[a, b]]) (hab : b < a), ContinuousOn f (Icc b a)
⊢ ContinuousOn f (Icc b a)

Tactic:
rwa [uIcc_of_ge hab.le] at hf

Premises used: Set.uIcc_of_ge, LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
⊢ ∀ x ∈ Ioo b a, HasDerivAt f (f' x) x

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
⊢ ∀ x ∈ Ioo b a, 0 ≤ f' x

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
⊢ b ≤ a

Tactic:
hab.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
⊢ b ≤ a

Tactic:
exact hab.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
simp :
  IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) volume a b ↔
    IntervalIntegrable g volume (f a) (f b)

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
inl :
  ∀ (hab : a ≤ b),
    IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔
      IntervalIntegrable g volume (f a) (f b)
inr :
  ∀ (hab : b < a),
    IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔
      IntervalIntegrable g volume (f a) (f b)
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)

Tactic:
rcases le_or_gt a b with hab | hab

Premises used: le_or_gt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : a ≤ b
inl : f a ≤ f b
inl₁ : ContinuousOn f (Icc a b)
inl₂ : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
inl₃ : ∀ x ∈ Ioo a b, 0 ≤ f' x
inl₄ : a ≤ b
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le hab,
      integrableOn_Icc_deriv_smul_iff_of_deriv_nonneg,
      intervalIntegrable_iff_integrableOn_Icc_of_le]

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, MeasureTheory.integrableOn_Icc_deriv_smul_iff_of_deriv_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
inr : f b ≤ f a
inr₁ : ContinuousOn f (Icc b a)
inr₂ : ∀ x ∈ Ioo b a, HasDerivAt f (f' x) x
inr₃ : ∀ x ∈ Ioo b a, 0 ≤ f' x
inr₄ : b ≤ a
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)

Tactic:
rw [IntervalIntegrable.symm_iff, intervalIntegrable_iff_integrableOn_Icc_of_le hab.le,
      integrableOn_Icc_deriv_smul_iff_of_deriv_nonneg,
      IntervalIntegrable.symm_iff, intervalIntegrable_iff_integrableOn_Icc_of_le]

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, LT.lt.le, MeasureTheory.integrableOn_Icc_deriv_smul_iff_of_deriv_nonneg, IntervalIntegrable.symm_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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
hf'₁ : DifferentiableOn ℝ f (interior [[a, b]])
hf'_nonpos : ∀ x ∈ interior [[a, b]], deriv f x ≤ 0
⊢ AntitoneOn f [[a, b]]

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_uIcc a b) hf

Premises used: convex_uIcc, antitoneOn_of_deriv_nonpos
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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
hf'₁ : DifferentiableOn ℝ f (Ioo (min a b) (max a b))
⊢ DifferentiableOn ℝ f (interior [[a, b]])

Tactic:
rw [uIcc, interior_Icc]

Premises used: interior_Icc, Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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
⊢ DifferentiableOn ℝ f (Ioo (min a b) (max a b))

Tactic:
fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt

Premises used: HasDerivAt.differentiableAt, DifferentiableAt.differentiableWithinAt, DifferentiableOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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
⊢ DifferentiableOn ℝ f (Ioo (min a b) (max a b))

Tactic:
exact fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt

Premises used: HasDerivAt.differentiableAt, DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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
hf'_nonpos : ∀ x ∈ Ioo (min a b) (max a b), deriv f x ≤ 0
⊢ ∀ x ∈ interior [[a, b]], deriv f x ≤ 0

Tactic:
rw [uIcc, interior_Icc]

Premises used: interior_Icc, Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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
z : ℝ
hz : z ∈ Ioo (min a b) (max a b)
⊢ deriv f z ≤ 0

Tactic:
simpa [(hff' z hz).deriv] using hf' z hz

Premises used: HasDerivAt.deriv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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
⊢ AntitoneOn f [[a, b]]

Tactic:
have M : AntitoneOn f (uIcc a b) := by
    apply antitoneOn_of_deriv_nonpos (convex_uIcc a b) hf
    · rw [uIcc, interior_Icc]
      exact fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt
    · rw [uIcc, interior_Icc]
      intro z hz
      simpa [(hff' z hz).deriv] using hf' z hz
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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]]
simp : Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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]]
inl : ∀ (hab : a ≤ b), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
inr : ∀ (hab : b < a), Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
rcases le_or_gt a b with hab | hab

Premises used: le_or_gt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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 : a ≤ b
inl : f b ≤ f a
inl₁ : ContinuousOn f (Icc a b)
inl₂ : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
inl₃ : ∀ x ∈ Ioo a b, f' x ≤ 0
inl₄ : a ≤ b
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
rw [integral_of_le hab, ← integral_Icc_eq_integral_Ioc,
      integral_Icc_deriv_smul_of_deriv_nonpos, integral_of_ge, ← integral_Icc_eq_integral_Ioc]

Premises used: intervalIntegral.integral_of_ge, intervalIntegral.integral_of_le, MeasureTheory.integral_Icc_deriv_smul_of_deriv_nonpos, MeasureTheory.integral_Icc_eq_integral_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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 : a ≤ b
⊢ f b ≤ f a

Tactic:
apply M left_mem_uIcc right_mem_uIcc hab

Premises used: Set.right_mem_uIcc, Set.left_mem_uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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 : a ≤ b
inl inl₁ inl₂ inl₃ :
  ∀ (hf : ContinuousOn f (Icc 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 : a ≤ b), ContinuousOn f (Icc a b)
⊢ ContinuousOn f (Icc a b)

Tactic:
rwa [uIcc_of_le hab] at hf

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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 : a ≤ b
⊢ ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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 : a ≤ b
⊢ ∀ x ∈ Ioo a b, f' x ≤ 0

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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 : a ≤ b
⊢ a ≤ b

Tactic:
hab
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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 : a ≤ b
⊢ a ≤ b

Tactic:
exact hab
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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
inr : f a ≤ f b
inr₁ : ContinuousOn f (Icc b a)
inr₂ : ∀ x ∈ Ioo b a, HasDerivAt f (f' x) x
inr₃ : ∀ x ∈ Ioo b a, f' x ≤ 0
inr₄ : b ≤ a
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
rw [integral_of_ge hab.le, ← integral_Icc_eq_integral_Ioc,
      integral_Icc_deriv_smul_of_deriv_nonpos, integral_of_le, ← integral_Icc_eq_integral_Ioc,
      neg_neg]

Premises used: neg_neg, LT.lt.le, intervalIntegral.integral_of_ge, intervalIntegral.integral_of_le, MeasureTheory.integral_Icc_deriv_smul_of_deriv_nonpos, MeasureTheory.integral_Icc_eq_integral_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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

Tactic:
apply M right_mem_uIcc left_mem_uIcc hab.le

Premises used: Set.right_mem_uIcc, LT.lt.le, Set.left_mem_uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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
inr inr₁ inr₂ inr₃ :
  ∀ (hf : ContinuousOn f (Icc b a)) (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)
⊢ ContinuousOn f (Icc b a)

Tactic:
rwa [uIcc_of_ge hab.le] at hf

Premises used: Set.uIcc_of_ge, LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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:
hab.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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:
exact hab.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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]]
simp :
  IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) volume a b ↔
    IntervalIntegrable g volume (f a) (f b)

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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]]
inl :
  ∀ (hab : a ≤ b),
    IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔
      IntervalIntegrable g volume (f a) (f b)
inr :
  ∀ (hab : b < a),
    IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔
      IntervalIntegrable g volume (f a) (f b)
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)

Tactic:
rcases le_or_gt a b with hab | hab

Premises used: le_or_gt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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 : a ≤ b
inl : f b ≤ f a
inl₁ : ContinuousOn f (Icc a b)
inl₂ : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
inl₃ : ∀ x ∈ Ioo a b, f' x ≤ 0
inl₄ : a ≤ b
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le hab,
      integrableOn_Icc_deriv_smul_iff_of_deriv_nonpos,
      IntervalIntegrable.symm_iff, intervalIntegrable_iff_integrableOn_Icc_of_le]

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, MeasureTheory.integrableOn_Icc_deriv_smul_iff_of_deriv_nonpos, IntervalIntegrable.symm_iff