awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 x y
⊢ 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_right)

Premises used: Iff.mpr, Filter.Tendsto.comp, Filter.tendsto_congr', Real.tendsto_Icc_vitaliFamily_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 :
  ∀ (y : ℝ) (hy : y ∈ Ioi x),
    slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x y =
      ((fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) ∘ fun (y : ℝ) ↦ Icc x y) y
⊢ slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x =ᶠ[𝓝[>] x]
    (fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) ∘ fun (y : ℝ) ↦ Icc x y

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 ∈ Ioi x
⊢ x ≤ y

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 ∈ Ioi x
⊢ x ≤ y

Tactic:
replace hy : x ≤ y := 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 : x ≤ y
⊢ slope (PE := ℝ) (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) x y =
    ((fun (a : Set ℝ) ↦ ⨍ (y : ℝ) in a, f y) ∘ fun (y : ℝ) ↦ Icc x y) y

Tactic:
simp [slope, average, intervalIntegral.integral_interval_sub_left, hg,
        intervalIntegral.integral_of_le, hy, this]

Premises used: MeasureTheory.average, slope, intervalIntegral.integral_of_le, intervalIntegral.integral_interval_sub_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
inr :
  ∀
    (this :
      ∀ {f : ℝ → ℝ} {a b : ℝ} (hf : IntervalIntegrable f volume a b) (hab : a ≤ b),
        ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x)
    (hab : ¬a ≤ b), ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
wlog :
  ∀ {f : ℝ → ℝ} {a b : ℝ} (hf : IntervalIntegrable f volume a b) (hab : a ≤ b),
    ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

Tactic:
wlog hab : a ≤ b
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
this :
  ∀ {f : ℝ → ℝ} {a b : ℝ} (hf : IntervalIntegrable f volume a b) (hab : a ≤ b),
    ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
hab : ¬a ≤ b
linarith : a < b → b - a + (a - b) = 0
⊢ b ≤ a

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
this :
  ∀ {f : ℝ → ℝ} {a b : ℝ} (hf : IntervalIntegrable f volume a b) (hab : a ≤ b),
    ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
hab : ¬a ≤ b
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

Tactic:
exact uIcc_comm b a ▸ @this f b a hf.symm (by linarith)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
rw : ∀ᵐ (x : ℝ), x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

Tactic:
rw [uIcc_of_le hab]

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
⊢ ∀ᵐ (x : ℝ), x ≠ a

Tactic:
simp [ae_iff, measure_singleton]

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
⊢ ∀ᵐ (x : ℝ), x ≠ a

Tactic:
have h₁ : ∀ᵐ x, x ≠ a := by simp [ae_iff, measure_singleton]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
⊢ ∀ᵐ (x : ℝ), x ≠ b

Tactic:
simp [ae_iff, measure_singleton]

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
⊢ ∀ᵐ (x : ℝ), x ≠ b

Tactic:
have h₂ : ∀ᵐ x, x ≠ b := by simp [ae_iff, measure_singleton]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
⊢ EqOn g f (Ioc a b)

Tactic:
grind [EqOn]

Premises used: Set.EqOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
⊢ MeasurableSet (Ioc a b)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
⊢ ∀ x ∉ Ioc a b, g x = 0

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
⊢ LocallyIntegrable g volume

Tactic:
have hg : LocallyIntegrable g volume :=
    integrableOn_congr_fun (by grind [EqOn]) (by simp) |>.mpr hf.left
      |>.integrable_of_forall_notMem_eq_zero (by grind) |>.locallyIntegrable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h : x ≠ a → x ≠ b → x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
⊢ x ≠ a → x ≠ b → x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h_1 : x ≠ a
h : x ≠ b → x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
⊢ x ≠ b → x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h_1 : x ≠ a
h_2 : x ≠ b
h : x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
⊢ x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
h :
  ∀ (x : ℝ) (hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x),
    x ≠ a → x ≠ b → x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
⊢ ∀ᵐ (x : ℝ), x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

Tactic:
filter_upwards [LocallyIntegrable.ae_hasDerivAt_integral hg, h₁, h₂] with x hx _ _ _

Premises used: LocallyIntegrable.ae_hasDerivAt_integral
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h : x ≠ a
h_1 : x ≠ b
h_2 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
⊢ a < x

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h : x ≠ a
h_1 : x ≠ b
h_2 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
⊢ x < b

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h_1 : x ≠ a
h_2 : x ≠ b
h_3 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
h : HasDerivWithinAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) (Ioo a b) x
⊢ HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

Tactic:
refine HasDerivWithinAt.hasDerivAt (s := Ioo a b) ?_ <|
    Ioo_mem_nhds (by grind) (by grind)

Premises used: Ioo_mem_nhds, HasDerivWithinAt.hasDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h : x ≠ a
h_1 : x ≠ b
h_2 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
⊢ f x = g x

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h_1 : x ≠ a
h_2 : x ≠ b
h_3 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
h : HasDerivWithinAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (g x) (Ioo a b) x
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) (Ioo a b) x

Tactic:
rw [show f x = g x by grind]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h : x ≠ a
h_1 : x ≠ b
h_2 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (g x) (Ioo a b) x

Tactic:
(hx c).hasDerivWithinAt.congr (fun y hy ↦ ?_) ?_

Premises used: HasDerivAt.hasDerivWithinAt, HasDerivWithinAt.congr
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h_1 : x ≠ a
h_2 : x ≠ b
h_3 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
h : ∀ (y : ℝ) (hy : y ∈ Ioo a b), Eq (α := ℝ) (∫ (t : ℝ) in c..y, f t) (∫ (t : ℝ) in c..y, g t)
h₃ : Eq (α := ℝ) (∫ (t : ℝ) in c..x, f t) (∫ (t : ℝ) in c..x, g t)
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (g x) (Ioo a b) x

Tactic:
refine (hx c).hasDerivWithinAt.congr (fun y hy ↦ ?_) ?_

Premises used: HasDerivAt.hasDerivWithinAt, HasDerivWithinAt.congr
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h_1 : x ≠ a
h_2 : x ≠ b
h_3 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
y : ℝ
hy : y ∈ Ioo a b
h : ∀ᵐ (x : ℝ), x ∈ Ioc c y → f x = g x
h₃ : ∀ᵐ (x : ℝ), x ∈ Ioc y c → f x = g x
⊢ Eq (α := ℝ) (∫ (t : ℝ) in c..y, f t) (∫ (t : ℝ) in c..y, g t)

Tactic:
apply intervalIntegral.integral_congr_ae'

Premises used: intervalIntegral.integral_congr_ae'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h_1 : x ≠ a
h_2 : x ≠ b
h_3 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
y : ℝ
hy : y ∈ Ioo a b
h : ∀ a ∈ Ioc c y, f a = g a
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc c y → f x = g x

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h_1 : x ≠ a
h_2 : x ≠ b
h_3 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
y : ℝ
hy : y ∈ Ioo a b
h : ∀ a ∈ Ioc y c, f a = g a
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc y c → f x = g x

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h : x ≠ a
h_1 : x ≠ b
h_2 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
y : ℝ
hy : y ∈ Ioo a b
⊢ ∀ a ∈ Ioc c y, f a = g a

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h : x ≠ a
h_1 : x ≠ b
h_2 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
y : ℝ
hy : y ∈ Ioo a b
⊢ ∀ a ∈ Ioc y c, f a = g a

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h_1 : x ≠ a
h_2 : x ≠ b
h_3 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
h : ∀ᵐ (x_1 : ℝ), x_1 ∈ Ioc c x → f x_1 = g x_1
h₃ : ∀ᵐ (x_1 : ℝ), x_1 ∈ Ioc x c → f x_1 = g x_1
⊢ Eq (α := ℝ) (∫ (t : ℝ) in c..x, f t) (∫ (t : ℝ) in c..x, g t)

Tactic:
apply intervalIntegral.integral_congr_ae'

Premises used: intervalIntegral.integral_congr_ae'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h_1 : x ≠ a
h_2 : x ≠ b
h_3 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
h : ∀ a ∈ Ioc c x, f a = g a
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Ioc c x → f x_1 = g x_1

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h_1 : x ≠ a
h_2 : x ≠ b
h_3 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
h : ∀ a ∈ Ioc x c, f a = g a
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Ioc x c → f x_1 = g x_1

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h : x ≠ a
h_1 : x ≠ b
h_2 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
⊢ ∀ a ∈ Ioc c x, f a = g a

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ if x ∈ Ioc a b then f x else 0
hg : LocallyIntegrable g volume
x : ℝ
hx : ∀ (c : ℝ), HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, g t) (g x) x
h : x ≠ a
h_1 : x ≠ b
h_2 : x ∈ Icc a b
c : ℝ
hc : c ∈ Icc a b
⊢ ∀ a ∈ Ioc x c, f a = g a

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
pos : ∀ (h : a = b), ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
neg : ∀ (h : ¬a = b), ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
by_cases h : a = b
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : a = b
pos :
  ∀ (hf : ContinuousOn f [[a, a]]) (hg : IntervalIntegrable g μ a a) (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a a), 0 ≤ g x),
    ∃ c ∈ [[a, a]], ∫ (x : ℝ) in a..a, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..a, g x ∂μ
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
subst h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, a]]
hg : IntervalIntegrable g μ a a
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a a), 0 ≤ g x
⊢ a ∈ [[a, a]]

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, a]]
hg : IntervalIntegrable g μ a a
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a a), 0 ≤ g x
⊢ ∫ (x : ℝ) in a..a, f x * g x ∂μ = f a * ∫ (x : ℝ) in a..a, g x ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, a]]
hg : IntervalIntegrable g μ a a
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a a), 0 ≤ g x
⊢ ∃ c ∈ [[a, a]], ∫ (x : ℝ) in a..a, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..a, g x ∂μ

Tactic:
exact ⟨a, by simp, by simp⟩