awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
I : Integrable (AEStronglyMeasurable.mk f ⋯) μ
x : α
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
⊢ Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)
have apply : ∀ (x_1 : Set α),
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in x_1, ‖AEStronglyMeasurable.mk f sorry y - AEStronglyMeasurable.mk f sorry x‖ₑ ∂μ)
      ((μ : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥0∞) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in x_1, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥0∞)
Tactic: apply hx.congr _
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
I : Integrable (AEStronglyMeasurable.mk f ⋯) μ
x : α
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
a : Set α
⊢ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ)
      ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
have e_a : ∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f sorry y - AEStronglyMeasurable.mk f sorry x‖ₑ ∂μ = ∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
I : Integrable (AEStronglyMeasurable.mk f ⋯) μ
x : α
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
a : Set α
⊢ ∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ =
    ∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ
have e_a : (ae (μ.restrict a)).EventuallyEq (β := ℝ≥0∞)
  (fun (a : α) ↦ ‖AEStronglyMeasurable.mk f sorry a - AEStronglyMeasurable.mk f sorry x‖ₑ) fun (a : α) ↦ ‖f a - f x‖ₑ
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
I : Integrable (AEStronglyMeasurable.mk f ⋯) μ
x : α
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
a : Set α
⊢ (ae (μ.restrict a)).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ ‖AEStronglyMeasurable.mk f ⋯ a - AEStronglyMeasurable.mk f ⋯ x‖ₑ) fun (a : α) ↦ ‖f a - f x‖ₑ
have e_a : ∀ᵐ (x_1 : α) ∂μ,
  Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ‖AEStronglyMeasurable.mk f sorry a - AEStronglyMeasurable.mk f sorry x‖ₑ) x_1)
    ((fun (a : α) ↦ ‖f a - f x‖ₑ) x_1)
Tactic: apply ae_restrict_of_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
I : Integrable (AEStronglyMeasurable.mk f ⋯) μ
x : α
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
a : Set α
⊢ ∀ᵐ (x_1 : α) ∂μ,
    Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ‖AEStronglyMeasurable.mk f ⋯ a - AEStronglyMeasurable.mk f ⋯ x‖ₑ) x_1)
      ((fun (a : α) ↦ ‖f a - f x‖ₑ) x_1)
have h : ∀ (y : α) (hy : f y = AEStronglyMeasurable.mk f sorry y),
  ‖AEStronglyMeasurable.mk f sorry y - AEStronglyMeasurable.mk f sorry x‖ₑ = ‖f y - f x‖ₑ
Tactic: filter_upwards [hf.1.ae_eq_mk] with y hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
I : Integrable (AEStronglyMeasurable.mk f ⋯) μ
x : α
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
a : Set α
y : α
hy : f y = AEStronglyMeasurable.mk f ⋯ y
⊢ ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ = ‖f y - f x‖ₑ
have h : ‖AEStronglyMeasurable.mk f sorry y - AEStronglyMeasurable.mk f sorry x‖ₑ = ‖AEStronglyMeasurable.mk f sorry y - f x‖ₑ
Tactic: rw [hy, h'x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
I : Integrable (AEStronglyMeasurable.mk f ⋯) μ
x : α
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
a : Set α
y : α
hy : f y = AEStronglyMeasurable.mk f ⋯ y
h : ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ = ‖AEStronglyMeasurable.mk f ⋯ y - f x‖ₑ
⊢ ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ = ‖f y - f x‖ₑ
have h₁ : ‖AEStronglyMeasurable.mk f sorry y - AEStronglyMeasurable.mk f sorry x‖ₑ =
  ‖AEStronglyMeasurable.mk f sorry y - AEStronglyMeasurable.mk f sorry x‖ₑ
Tactic: rw [hy, h'x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
have rcases : ∀ (u : ℕ → Set α) (u_open : ∀ (n : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (u n))
  (u_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), u n) univ) (hu : ∀ (n : ℕ), IntegrableOn f (u n) μ),
  ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
Tactic: rcases hf.exists_nat_integrableOn with ⟨u, u_open, u_univ, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (u n)
u_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), u n) univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
have hf₁ : Integrable ((u n).indicator f) μ
Tactic: apply ae_tendsto_lintegral_enorm_sub_div_of_integrable
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (u n)
u_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), u n) univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
have this : ∀ (n : ℕ),
  ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
Tactic: have : ∀ n, ∀ᵐ x ∂μ,
      Tendsto (fun a => (∫⁻ y in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a)
      (v.filterAt x) (𝓝 0) := by
    intro n
    apply ae_tendsto_lintegral_enorm_sub_div_of_integrable
    exact (integrable_indicator_iff (u_open n).measurableSet).2 (hu n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (u n)
u_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), u n) univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (β := ℝ≥0∞)
        (fun (a : Set α) ↦
          HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ)
            ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 0)
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
have h : ∀ (x : α)
  (hx :
    ∀ (i : ℕ),
      Tendsto (β := ℝ≥0∞)
        (fun (a : Set α) ↦
          HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ)
            ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 0)),
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)
Tactic: filter_upwards [ae_all_iff.2 this] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (u n)
u_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), u n) univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (β := ℝ≥0∞)
        (fun (a : Set α) ↦
          HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ)
            ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)
have h : ∀ (n : ℕ) (hn : x ∈ u n),
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)
Tactic: obtain ⟨n, hn⟩ : ∃ n, x ∈ u n := by simpa only [← u_univ, mem_iUnion] using mem_univ x
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (u n)
u_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), u n) univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (β := ℝ≥0∞)
        (fun (a : Set α) ↦
          HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ)
            ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
n : ℕ
hn : x ∈ u n
⊢ Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)
have apply : (v.filterAt x).EventuallyEq (β := ℝ≥0∞)
  (fun (a : Set α) ↦
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ)
      ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
  fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: apply Tendsto.congr' _ (hx n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (u n)
u_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), u n) univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (β := ℝ≥0∞)
        (fun (a : Set α) ↦
          HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ)
            ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
n : ℕ
hn : x ∈ u n
⊢ (v.filterAt x).EventuallyEq (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
have h : ∀ (a : Set α) (ha : a ⊆ u n) (h'a : MeasurableSet a),
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ)
      ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: filter_upwards [v.eventually_filterAt_subset_of_nhds ((u_open n).mem_nhds hn),
    v.eventually_filterAt_measurableSet x] with a ha h'a
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (u n)
u_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), u n) univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (β := ℝ≥0∞)
        (fun (a : Set α) ↦
          HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ)
            ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
n : ℕ
hn : x ∈ u n
a : Set α
ha : a ⊆ u n
h'a : MeasurableSet a
⊢ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ)
      ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
have h : ∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ = ∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (u n)
u_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), u n) univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (β := ℝ≥0∞)
        (fun (a : Set α) ↦
          HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ)
            ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
n : ℕ
hn : x ∈ u n
a : Set α
ha : a ⊆ u n
h'a : MeasurableSet a
⊢ ∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ = ∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ
have h : ∀ (y : α) (hy : y ∈ a), ‖(u n).indicator f y - (u n).indicator f x‖ₑ = ‖f y - f x‖ₑ
Tactic: refine setLIntegral_congr_fun h'a (fun y hy ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (u n)
u_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), u n) univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (β := ℝ≥0∞)
        (fun (a : Set α) ↦
          HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ)
            ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
n : ℕ
hn : x ∈ u n
a : Set α
ha : a ⊆ u n
h'a : MeasurableSet a
y : α
hy : y ∈ a
⊢ ‖(u n).indicator f y - (u n).indicator f x‖ₑ = ‖f y - f x‖ₑ
have h : ‖f y - (u n).indicator f x‖ₑ = ‖f y - f x‖ₑ
Tactic: rw [indicator_of_mem (ha hy) f, indicator_of_mem hn f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (u n)
u_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), u n) univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (β := ℝ≥0∞)
        (fun (a : Set α) ↦
          HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ)
            ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
n : ℕ
hn : x ∈ u n
a : Set α
ha : a ⊆ u n
h'a : MeasurableSet a
y : α
hy : y ∈ a
h : ‖f y - (u n).indicator f x‖ₑ = ‖f y - f x‖ₑ
⊢ ‖(u n).indicator f y - (u n).indicator f x‖ₑ = ‖f y - f x‖ₑ
have h₁ : ‖f y - f x‖ₑ = ‖f y - f x‖ₑ
Tactic: rw [indicator_of_mem (ha hy) f, indicator_of_mem hn f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
have h : ∀ (x : α)
  (hx :
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)),
  Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
Tactic: filter_upwards [v.ae_tendsto_lintegral_enorm_sub_div hf] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : SecondCountableTopology α
inst_3 : BorelSpace α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
x : α
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
have this : Tendsto
  (ENNReal.toReal ∘ fun (a : Set α) ↦
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
  (v.filterAt x) (𝓝 (ENNReal.toReal 0))
Tactic: have := (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp hx