awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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
⊢ 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
have hy₁ : y ≤ x
Tactic: replace hy : y ≤ x := by grind
Cleared hypotheses: hy
-- 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 y : ℝ
hy : y ≤ 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
have 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
Tactic: simp [slope, average, intervalIntegral.integral_interval_sub_left, hg,
        intervalIntegral.integral_of_ge, hy, this]
-- 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 x y
Tactic: refine Filter.tendsto_congr' ?_ |>.mpr (hx.comp x.tendsto_Icc_vitaliFamily_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 : ℝ
⊢ 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
have 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
Tactic: filter_upwards [self_mem_nhdsWithin] with y hy
-- 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))
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
⊢ 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
have hy₁ : x ≤ y
Tactic: replace hy : x ≤ y := by grind
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
have 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
Tactic: wlog hab : a ≤ b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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
⊢ ∀ᵐ (x : ℝ), x ∈ uIcc a b → ∀ c ∈ uIcc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
have 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
Tactic: wlog hab : a ≤ b
Cleared hypotheses: f, a, b, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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
⊢ b ≤ a
have linarith : a < b → b - a + (a - b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
Goal:
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
have rw : ∀ᵐ (x : ℝ), x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
Tactic: rw [uIcc_of_le hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
⊢ ∀ᵐ (x : ℝ), x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
have h₁ : ∀ᵐ (x : ℝ), x ≠ a
Tactic: have h₁ : ∀ᵐ x, x ≠ a := by simp [ae_iff, measure_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hab : a ≤ b
h₁ : ∀ᵐ (x : ℝ), x ≠ a
⊢ ∀ᵐ (x : ℝ), x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
have h₂ : ∀ᵐ (x : ℝ), x ≠ b
Tactic: have h₂ : ∀ᵐ x, x ≠ b := by simp [ae_iff, measure_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (hypothesis)
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 : ℝ), x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
have hg : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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 : ℝ), x ∈ Icc a b → ∀ c ∈ Icc a b, HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
have 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
Tactic: filter_upwards [LocallyIntegrable.ae_hasDerivAt_integral hg, h₁, h₂] with x hx _ _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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
⊢ HasDerivAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
have h : HasDerivWithinAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (f x) (Ioo a b) x
Tactic: refine HasDerivWithinAt.hasDerivAt (s := Ioo a b) ?_ <|
    Ioo_mem_nhds (by grind) (by grind)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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) (f x) (Ioo a b) x
have h : HasDerivWithinAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (g x) (Ioo a b) x
Tactic: rw [show f x = g x by grind]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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
have h : ∀ (y : ℝ) (hy : y ∈ Ioo a b), Eq (α := ℝ) (∫ (t : ℝ) in c..y, f t) (∫ (t : ℝ) in c..y, g t)
Tactic: refine (hx c).hasDerivWithinAt.congr (fun y hy ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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)
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ ∫ (t : ℝ) in c..x, f t) (g x) (Ioo a b) x
have h₃ : Eq (α := ℝ) (∫ (t : ℝ) in c..x, f t) (∫ (t : ℝ) in c..x, g t)
Tactic: refine (hx c).hasDerivWithinAt.congr (fun y hy ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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
⊢ Eq (α := ℝ) (∫ (t : ℝ) in c..y, f t) (∫ (t : ℝ) in c..y, g t)
have h : ∀ᵐ (x : ℝ), x ∈ Ioc c y → f x = g x
Tactic: apply intervalIntegral.integral_congr_ae'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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
⊢ Eq (α := ℝ) (∫ (t : ℝ) in c..y, f t) (∫ (t : ℝ) in c..y, g t)
have h₃ : ∀ᵐ (x : ℝ), x ∈ Ioc y c → f x = g x
Tactic: apply intervalIntegral.integral_congr_ae'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc c y → f x = g x
have h : ∀ a ∈ Ioc c y, f a = g a
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc y c → f x = g x
have h : ∀ a ∈ Ioc y c, f a = g a
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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
⊢ Eq (α := ℝ) (∫ (t : ℝ) in c..x, f t) (∫ (t : ℝ) in c..x, g t)
have h : ∀ᵐ (x_1 : ℝ), x_1 ∈ Ioc c x → f x_1 = g x_1
Tactic: apply intervalIntegral.integral_congr_ae'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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
⊢ Eq (α := ℝ) (∫ (t : ℝ) in c..x, f t) (∫ (t : ℝ) in c..x, g t)
have h₃ : ∀ᵐ (x_1 : ℝ), x_1 ∈ Ioc x c → f x_1 = g x_1
Tactic: apply intervalIntegral.integral_congr_ae'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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_1 : ℝ), x_1 ∈ Ioc c x → f x_1 = g x_1
have h : ∀ a ∈ Ioc c x, f a = g a
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm (goal)
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_1 : ℝ), x_1 ∈ Ioc x c → f x_1 = g x_1
have h : ∀ a ∈ Ioc x c, f a = g a
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (goal)
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
have pos : ∀ (h : a = b), ∃ 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (goal)
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 ∂μ
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
have neg : ∀ (h : ¬a = b), ∃ 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (goal)
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
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
have 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 ∂μ
Tactic: subst h
Cleared hypotheses: b, hf, hg, hg0, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (goal)
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
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
have neg : ∀
  (this :
    ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
      (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
      ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ)
  (hab : ¬a < b), ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
Tactic: wlog hab : a < b generalizing a b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (goal)
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
neg :
  ∀
    (this :
      ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
        (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
        ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ)
    (hab : ¬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 ∂μ
have wlog : ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
  (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
  ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
Tactic: wlog hab : a < b generalizing a b
Cleared hypotheses: hf, hg, hg0, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (hypothesis)
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
this :
  ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
    (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
    ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : ¬a < b
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
have hab₁ : b ≤ a
Tactic: simp only [not_lt] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (goal)
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
this :
  ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
    (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
    ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : b ≤ a
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
have neg : ∀ (c : ℝ) (c_in_uIcc : c ∈ [[b, a]]) (that : ∫ (x : ℝ) in b..a, f x * g x ∂μ = f c * ∫ (x : ℝ) in b..a, g x ∂μ),
  ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
Tactic: obtain ⟨c, c_in_uIcc, that⟩ :=
      this (by rwa [uIcc_comm]) hg.symm (by rwa [uIoc_comm]) (by lia) (lt_of_le_of_ne' hab h)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (hypothesis)
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
have hs : s = Ioc a b
Tactic: have hs : s = Ioc a b := uIoc_of_le hab.le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (hypothesis)
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
have hs' : s ⊆ [[a, b]]
Tactic: have hs' : s ⊆ [[a, b]] := uIoc_subset_uIcc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (hypothesis)
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
have hs_conn : IsConnected s
Tactic: have hs_conn : IsConnected s := by simpa [hs] using isConnected_Ioc hab