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), f' x ≤ 0
M : AntitoneOn f [[a, b]]
hab : b < a
inr : f a ≤ f b
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_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
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, f' x ≤ 0
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
inr₁ : ContinuousOn f (Icc b a)
inr₂ : ∀ x ∈ Ioo b a, HasDerivAt f (f' x) x
inr₃ : ∀ x ∈ Ioo b a, 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 inr₄ : 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]
-- 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
⊢ 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), f' x ≤ 0) (M : AntitoneOn 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), f' x ≤ 0
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) volume a b ↔
    IntervalIntegrable g volume (f a) (f b)
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]]
⊢ 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), f' x ≤ 0
M : AntitoneOn 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), 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)
⊢ 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), f' x ≤ 0
M : AntitoneOn 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 b ≤ f a
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]
-- 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
⊢ 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_nonpos,
      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
M : AntitoneOn f [[a, b]]
hab : a ≤ b
inl : f b ≤ f a
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_nonpos,
      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
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
⊢ 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, f' x ≤ 0
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]
-- 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
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)
have inr : f a ≤ f b
Tactic: rw [IntervalIntegrable.symm_iff, intervalIntegrable_iff_integrableOn_Icc_of_le hab.le,
      integrableOn_Icc_deriv_smul_iff_of_deriv_nonpos,
      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
M : AntitoneOn f [[a, b]]
hab : b < a
inr : 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₁ : 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_nonpos,
      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
M : AntitoneOn f [[a, b]]
hab : b < a
inr : f a ≤ f b
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_nonpos,
      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
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
⊢ 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, f' x ≤ 0
Tactic: rw [IntervalIntegrable.symm_iff, intervalIntegrable_iff_integrableOn_Icc_of_le hab.le,
      integrableOn_Icc_deriv_smul_iff_of_deriv_nonpos,
      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
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
⊢ 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_nonpos,
      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 g' : ℝ → E
inst_2 : CompleteSpace E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g [[f a, f b]]
hgg' : ∀ x ∈ Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Ioi x) x
hg' : ContinuousOn g' (f '' [[a, b]])
⊢ ∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a
have rw : g (f b) - g (f a) = (g ∘ f) b - (g ∘ f) a
Tactic: rw [integral_deriv_smul_comp'' hf hff' hf' hg',
    integral_eq_sub_of_hasDeriv_right hg hgg' (hg'.mono _).intervalIntegrable]
-- 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 g' : ℝ → E
inst_2 : CompleteSpace E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g [[f a, f b]]
hgg' : ∀ x ∈ Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Ioi x) x
hg' : ContinuousOn g' (f '' [[a, b]])
rw : g (f b) - g (f a) = (g ∘ f) b - (g ∘ f) a
⊢ ∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a
have rw₁ : [[f a, f b]] ⊆ f '' [[a, b]]
Tactic: rw [integral_deriv_smul_comp'' hf hff' hf' hg',
    integral_eq_sub_of_hasDeriv_right hg hgg' (hg'.mono _).intervalIntegrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts (hypothesis)
Goal:
a b : ℝ
f f' g : ℝ → ℝ
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' [[a, b]]) volume
hg2 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (g ∘ f) x * f' x) [[a, b]] volume
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, (g ∘ f) x * f' x) (∫ (u : ℝ) in f a..f b, g u)
have hg2' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
Tactic: have hg2' : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) [[a, b]] := by simpa [mul_comm] using hg2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (hypothesis)
Goal:
f : ℝ → ℝ
hf : LocallyIntegrable f volume
⊢ ∀ᵐ (x : ℝ), ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
have hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
Tactic: have hg (x y : ℝ) : IntervalIntegrable f volume x y :=
    intervalIntegrable_iff.mpr <|
      (hf.integrableOn_isCompact isCompact_uIcc).mono_set uIoc_subset_uIcc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (hypothesis)
Goal:
f : ℝ → ℝ
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
⊢ ∀ᵐ (x : ℝ), ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
have LDT : ∀ᵐ (x : ℝ),
  Tendsto (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
    (𝓝 (f x))
Tactic: have LDT := (vitaliFamily volume 1).ae_tendsto_average hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (hypothesis)
Goal:
f : ℝ → ℝ
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT :
  ∀ᵐ (x : ℝ),
    Tendsto (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
      (𝓝 (f x))
⊢ ∀ᵐ (x : ℝ), ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
have this : ∀ {a b : ℝ},
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (t : ℝ) ↦ f t)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (t : ℝ) ↦ f t)
Tactic: have {a b : ℝ} : ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t :=
    integral_Icc_eq_integral_Ioc (x := a) (y := b) (X := ℝ) |>.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
Goal:
f : ℝ → ℝ
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT :
  ∀ᵐ (x : ℝ),
    Tendsto (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
      (𝓝 (f x))
this :
  ∀ {a b : ℝ},
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (t : ℝ) ↦ f t)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (t : ℝ) ↦ f t)
⊢ ∀ᵐ (x : ℝ), ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
have h : ∀ (x : ℝ)
  (hx :
    Tendsto (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
      (𝓝 (f x)))
  (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
Tactic: filter_upwards [LDT] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
Goal:
f : ℝ → ℝ
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT :
  ∀ᵐ (x : ℝ),
    Tendsto (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
      (𝓝 (f x))
this :
  ∀ {a b : ℝ},
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (t : ℝ) ↦ f t)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (t : ℝ) ↦ f t)
x : ℝ
hx :
  Tendsto (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
    (𝓝 (f x))
c : ℝ
⊢ HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
have h : Tendsto (slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[<] x) (𝓝 (f x)) ∧
  Tendsto (slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[>] x) (𝓝 (f x))
Tactic: rw [hasDerivAt_iff_tendsto_slope_left_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
Goal:
f : ℝ → ℝ
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT :
  ∀ᵐ (x : ℝ),
    Tendsto (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
      (𝓝 (f x))
this :
  ∀ {a b : ℝ},
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (t : ℝ) ↦ f t)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (t : ℝ) ↦ f t)
x : ℝ
hx :
  Tendsto (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
    (𝓝 (f x))
c : ℝ
⊢ Tendsto (slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[<] x) (𝓝 (f x)) ∧
    Tendsto (slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[>] x) (𝓝 (f x))
have h : Tendsto (slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[<] x) (𝓝 (f x))
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
Goal:
f : ℝ → ℝ
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT :
  ∀ᵐ (x : ℝ),
    Tendsto (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
      (𝓝 (f x))
this :
  ∀ {a b : ℝ},
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (t : ℝ) ↦ f t)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (t : ℝ) ↦ f t)
x : ℝ
hx :
  Tendsto (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
    (𝓝 (f x))
c : ℝ
h : Tendsto (slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[<] x) (𝓝 (f x))
⊢ Tendsto (slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[<] x) (𝓝 (f x)) ∧
    Tendsto (slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[>] x) (𝓝 (f x))
have h₁ : Tendsto (slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[>] x) (𝓝 (f x))
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
Goal:
f : ℝ → ℝ
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT :
  ∀ᵐ (x : ℝ),
    Tendsto (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
      (𝓝 (f x))
this :
  ∀ {a b : ℝ},
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (t : ℝ) ↦ f t)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (t : ℝ) ↦ f t)
x : ℝ
hx :
  Tendsto (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
    (𝓝 (f x))
c : ℝ
⊢ Tendsto (slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[<] x) (𝓝 (f x))
have h : slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x =ᶠ[𝓝[<] x]
  (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) ∘ fun (y : ℝ) ↦ Icc y x
Tactic: refine Filter.tendsto_congr' ?_ |>.mpr (hx.comp x.tendsto_Icc_vitaliFamily_left)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
Goal:
f : ℝ → ℝ
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT :
  ∀ᵐ (x : ℝ),
    Tendsto (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
      (𝓝 (f x))
this :
  ∀ {a b : ℝ},
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (t : ℝ) ↦ f t)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (t : ℝ) ↦ f t)
x : ℝ
hx :
  Tendsto (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)
    (𝓝 (f x))
c : ℝ
⊢ slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x =ᶠ[𝓝[<] x]
    (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) ∘ fun (y : ℝ) ↦ Icc y x
have h : ∀ (y : ℝ) (hy : y ∈ Iio x),
  slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x y =
    ((fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) ∘ fun (y : ℝ) ↦ Icc y x) y
Tactic: filter_upwards [self_mem_nhdsWithin] with y hy