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), 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
⊢ 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_nonpos,
      intervalIntegrable_iff_integrableOn_Icc_of_le]

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, MeasureTheory.integrableOn_Icc_deriv_smul_iff_of_deriv_nonpos, LT.lt.le, 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 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
rw₁ : [[f a, f b]] ⊆ f '' [[a, b]]
⊢ ∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (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]

Premises used: intervalIntegral.integral_eq_sub_of_hasDeriv_right, ContinuousOn.mono, ContinuousOn.intervalIntegrable, intervalIntegral.integral_deriv_smul_comp''
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
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]])
⊢ g (f b) - g (f a) = (g ∘ f) b - (g ∘ f) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
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]])
⊢ [[f a, f b]] ⊆ f '' [[a, b]]

Tactic:
intermediate_value_uIcc hf

Premises used: intermediate_value_uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
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]])
⊢ g (f b) - g (f a) = (g ∘ f) b - (g ∘ f) a

Tactic:
exacts [rfl, intermediate_value_uIcc hf]

Premises used: intermediate_value_uIcc, rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g g' : ℝ → E
inst_2 : CompleteSpace E
hf : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x
hg : ∀ x ∈ [[a, b]], HasDerivAt g (g' (f x)) (f x)
hf' : ContinuousOn f' [[a, b]]
hg' : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g'
⊢ ∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a

Tactic:
integral_eq_sub_of_hasDerivAt (fun x hx ↦ (hg x hx).scomp x <| hf x hx)
    (hf'.smul (hg'.comp_continuousOn <| HasDerivAt.continuousOn hf)).intervalIntegrable

Premises used: HasDerivAt.continuousOn, Continuous.comp_continuousOn, intervalIntegral.integral_eq_sub_of_hasDerivAt, HasDerivAt.scomp, ContinuousOn.smul, ContinuousOn.intervalIntegrable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume

Tactic:
simpa [mul_comm] using hg2

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
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
hg2' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) [[a, b]] volume
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, (g ∘ f) x * f' x) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
simpa [mul_comm] using integral_deriv_smul_comp''' hf hff' hg_cont hg1 hg2'

Premises used: mul_comm, intervalIntegral.integral_deriv_smul_comp'''
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
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
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g (f '' [[a, b]])
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, (g ∘ f) x * f' x) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
simpa [mul_comm] using integral_deriv_smul_comp'' hf hff' hf' hg

Premises used: mul_comm, intervalIntegral.integral_deriv_smul_comp''
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
f f' g : ℝ → ℝ
h : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x
h' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g (f '' [[a, b]])
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, (g ∘ f) x * f' x) (∫ (x : ℝ) in f a..f b, g x)

Tactic:
simpa [mul_comm] using integral_deriv_smul_comp' h h' hg

Premises used: intervalIntegral.integral_deriv_smul_comp', mul_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
f f' g : ℝ → ℝ
h : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x
h' : ContinuousOn f' [[a, b]]
hg : Continuous g
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, (g ∘ f) x * f' x) (∫ (x : ℝ) in f a..f b, g x)

Tactic:
integral_comp_mul_deriv' h h' hg.continuousOn

Premises used: Continuous.continuousOn, intervalIntegral.integral_comp_mul_deriv'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
f f' g : ℝ → ℝ
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
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, (g ∘ f) x * f' x) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
simpa [mul_comm] using integral_deriv_smul_comp_of_deriv_nonneg hf hff' hf'

Premises used: mul_comm, intervalIntegral.integral_deriv_smul_comp_of_deriv_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
f f' g : ℝ → ℝ
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 (α := ℝ) (∫ (x : ℝ) in a..b, (g ∘ f) x * f' x) (∫ (u : ℝ) in f a..f b, g u)

Tactic:
simpa [mul_comm] using integral_deriv_smul_comp_of_deriv_nonpos hf hff' hf'

Premises used: intervalIntegral.integral_deriv_smul_comp_of_deriv_nonpos, mul_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
f f' g : ℝ → ℝ
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 (ε := ℝ) (fun (x : ℝ) ↦ (g ∘ f) x * f' x) volume a b ↔ IntervalIntegrable g volume (f a) (f b)

Tactic:
simpa [mul_comm] using integrable_deriv_smul_comp_iff_of_deriv_nonneg hf hff' hf'

Premises used: mul_comm, intervalIntegral.integrable_deriv_smul_comp_iff_of_deriv_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
f f' g : ℝ → ℝ
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 (ε := ℝ) (fun (x : ℝ) ↦ (g ∘ f) x * f' x) volume a b ↔ IntervalIntegrable g volume (f a) (f b)

Tactic:
simpa [mul_comm] using integrable_deriv_smul_comp_iff_of_deriv_nonpos hf hff' hf'

Premises used: intervalIntegral.integrable_deriv_smul_comp_iff_of_deriv_nonpos, mul_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
f f' g g' : ℝ → ℝ
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, (g' ∘ f) x * f' x = (g ∘ f) b - (g ∘ f) a

Tactic:
simpa [mul_comm] using integral_deriv_smul_deriv_comp' hf hff' hf' hg hgg' hg'

Premises used: mul_comm, intervalIntegral.integral_deriv_smul_deriv_comp'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
f f' g g' : ℝ → ℝ
hf : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x
hg : ∀ x ∈ [[a, b]], HasDerivAt g (g' (f x)) (f x)
hf' : ContinuousOn f' [[a, b]]
hg' : Continuous g'
⊢ ∫ (x : ℝ) in a..b, (g' ∘ f) x * f' x = (g ∘ f) b - (g ∘ f) a

Tactic:
simpa [mul_comm] using integral_deriv_smul_deriv_comp hf hg hf' hg'

Premises used: intervalIntegral.integral_deriv_smul_deriv_comp, mul_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
hf : LocallyIntegrable f volume
⊢ ∀ (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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
⊢ ∀ᵐ (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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
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))
⊢ ∀ {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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
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)
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
⊢ ∀ᵐ (x : ℝ), ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

Tactic:
filter_upwards [LDT] with x hx
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
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))
⊢ HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

Tactic:
rw [hasDerivAt_iff_tendsto_slope_left_right]

Premises used: hasDerivAt_iff_tendsto_slope_left_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
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))
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))

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
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))

Tactic:
Filter.tendsto_congr' ?_ |>.mpr (hx.comp x.tendsto_Icc_vitaliFamily_left)

Premises used: Iff.mpr, Real.tendsto_Icc_vitaliFamily_left, Filter.Tendsto.comp, Filter.tendsto_congr'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
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 :
  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
⊢ Tendsto (slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x) (𝓝[<] x) (𝓝 (f x))

Tactic:
refine Filter.tendsto_congr' ?_ |>.mpr (hx.comp x.tendsto_Icc_vitaliFamily_left)

Premises used: Iff.mpr, Real.tendsto_Icc_vitaliFamily_left, Filter.Tendsto.comp, Filter.tendsto_congr'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
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 :
  ∀ (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
⊢ 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:
filter_upwards [self_mem_nhdsWithin] with y hy

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
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 y : ℝ
hy : y ∈ Iio x
⊢ y ≤ x

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
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 y : ℝ
hy : y ∈ Iio x
⊢ y ≤ x

Tactic:
replace hy : y ≤ x := by grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
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 y : ℝ
hy : y ≤ x
h :
  -((y - x)⁻¹ *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc y x)) fun (t : ℝ) ↦ f t) =
    (x - y)⁻¹ * @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc y x)) fun (t : ℝ) ↦ f t
⊢ 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:
simp [slope, average, intervalIntegral.integral_interval_sub_left, hg,
        intervalIntegral.integral_of_ge, hy, this]

Premises used: MeasureTheory.average, slope, intervalIntegral.integral_of_ge, intervalIntegral.integral_interval_sub_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
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 y : ℝ
hy : y ≤ x
⊢ -((y - x)⁻¹ *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc y x)) fun (t : ℝ) ↦ f t) =
    (x - y)⁻¹ * @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc y x)) fun (t : ℝ) ↦ f t

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
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))

Tactic:
Filter.tendsto_congr' ?_ |>.mpr (hx.comp x.tendsto_Icc_vitaliFamily_right)

Premises used: Iff.mpr, Filter.Tendsto.comp, Filter.tendsto_congr', Real.tendsto_Icc_vitaliFamily_right