awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
have inr : f b ≤ f a
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
have inr₁ : ContinuousOn f (Icc b a)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
have inr₂ : ∀ x ∈ Ioo b a, HasDerivAt f (f' x) x
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
have inr₃ : ∀ x ∈ Ioo b a, 0 ≤ f' x
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
have inr₄ : b ≤ a
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ ContinuousOn f (Icc b a)
have 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)
Tactic: rwa [uIcc_of_ge hab.le] at hf
Cleared hypotheses: hf, hff', hf', M, hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (hypothesis)
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
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) volume a b ↔
    IntervalIntegrable g volume (f a) (f b)
have M : MonotoneOn f [[a, b]]
Tactic: have M : MonotoneOn f (uIcc a b) := by
    apply monotoneOn_of_deriv_nonneg (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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]]
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) volume a b ↔
    IntervalIntegrable g volume (f a) (f b)
have simp : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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]]
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)
have 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)
Tactic: rcases le_or_gt a b with hab | hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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)
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)
have 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)
Tactic: rcases le_or_gt a b with hab | hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)
have inl : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)
have inl₁ : ContinuousOn f (Icc a b)
Tactic: rw [intervalIntegrable_iff_integrableOn_Icc_of_le hab,
      integrableOn_Icc_deriv_smul_iff_of_deriv_nonneg,
      intervalIntegrable_iff_integrableOn_Icc_of_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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)
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)
have inl₂ : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
Tactic: rw [intervalIntegrable_iff_integrableOn_Icc_of_le hab,
      integrableOn_Icc_deriv_smul_iff_of_deriv_nonneg,
      intervalIntegrable_iff_integrableOn_Icc_of_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)
have inl₃ : ∀ x ∈ Ioo a b, 0 ≤ f' x
Tactic: rw [intervalIntegrable_iff_integrableOn_Icc_of_le hab,
      integrableOn_Icc_deriv_smul_iff_of_deriv_nonneg,
      intervalIntegrable_iff_integrableOn_Icc_of_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)
have inr : f b ≤ f a
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)
have inr₁ : ContinuousOn f (Icc b a)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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)
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)
have inr₂ : ∀ x ∈ Ioo b a, HasDerivAt f (f' x) x
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)
have inr₃ : ∀ x ∈ Ioo b a, 0 ≤ f' x
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)
have inr₄ : b ≤ a
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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]]
have hf'₁ : DifferentiableOn ℝ f (interior [[a, b]])
Tactic: apply antitoneOn_of_deriv_nonpos (convex_uIcc a b) hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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]])
⊢ AntitoneOn f [[a, b]]
have hf'_nonpos : ∀ x ∈ interior [[a, b]], deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (convex_uIcc a b) hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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 (interior [[a, b]])
have hf'₁ : DifferentiableOn ℝ f (Ioo (min a b) (max a b))
Tactic: rw [uIcc, interior_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ ∀ x ∈ interior [[a, b]], deriv f x ≤ 0
have hf'_nonpos : ∀ x ∈ Ioo (min a b) (max a b), deriv f x ≤ 0
Tactic: rw [uIcc, interior_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)
have M : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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]]
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)
have simp : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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]]
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
have 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)
Tactic: rcases le_or_gt a b with hab | hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
have 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)
Tactic: rcases le_or_gt a b with hab | hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
have inl : f b ≤ f a
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
have inl₁ : ContinuousOn f (Icc a b)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
have inl₂ : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
have inl₃ : ∀ x ∈ Ioo a b, f' x ≤ 0
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ ContinuousOn f (Icc a b)
have 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)
Tactic: rwa [uIcc_of_le hab] at hf
Cleared hypotheses: hf, hff', hf', M, hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
have inr : f a ≤ f b
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (goal)
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
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • g (f x)) (∫ (u : ℝ) in f a..f b, g u)
have inr₁ : ContinuousOn f (Icc b a)
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]