awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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 : ℕ
⊢ Integrable ((u n).indicator f) μ

Tactic:
(integrable_indicator_iff (u_open n).measurableSet).2 (hu n)

Premises used: Iff.mpr, IsOpen.measurableSet, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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 : ℕ
⊢ Integrable ((u n).indicator f) μ

Tactic:
exact (integrable_indicator_iff (u_open n).measurableSet).2 (hu n)

Premises used: Iff.mpr, IsOpen.measurableSet, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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)

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)
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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)
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)
⊢ ∀ᵐ (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:
filter_upwards [ae_all_iff.2 this] with x hx

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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 : ℕ), x ∈ u n

Tactic:
simpa only [← u_univ, mem_iUnion] using mem_univ x

Premises used: Set.mem_iUnion, Set.mem_univ
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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)
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)
⊢ 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
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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
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∞)
⊢ 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:
apply Tendsto.congr' _ (hx n)

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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
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∞)
⊢ (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:
filter_upwards [v.eventually_filterAt_subset_of_nhds ((u_open n).mem_nhds hn),
    v.eventually_filterAt_measurableSet x] with a ha h'a

Premises used: VitaliFamily.eventually_filterAt_subset_of_nhds, VitaliFamily.eventually_filterAt_measurableSet, IsOpen.mem_nhds
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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
h : ∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ = ∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ
⊢ 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:
congr 1
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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‖ₑ ∂μ

Tactic:
setLIntegral_congr_fun h'a (fun y hy ↦ ?_)

Premises used: MeasureTheory.setLIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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
h : ∀ (y : α) (hy : y ∈ a), ‖(u n).indicator f y - (u n).indicator f x‖ₑ = ‖f y - f x‖ₑ
⊢ ∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ = ∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ

Tactic:
refine setLIntegral_congr_fun h'a (fun y hy ↦ ?_)

Premises used: MeasureTheory.setLIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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‖ₑ
h₁ h₂ : ‖f y - f x‖ₑ = ‖f y - f x‖ₑ
⊢ ‖(u n).indicator f y - (u n).indicator f x‖ₑ = ‖f y - f x‖ₑ

Tactic:
rw [indicator_of_mem (ha hy) f, indicator_of_mem hn f]

Premises used: Set.indicator_of_mem
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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 μ
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)
⊢ ∀ᵐ (x : α) ∂μ, 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

Premises used: VitaliFamily.ae_tendsto_lintegral_enorm_sub_div
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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
    (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
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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)
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) (𝓝 0)
apply :
  (ENNReal.toReal ∘ fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)) =ᶠ[v.filterAt x]
    fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
⊢ Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)

Tactic:
apply Tendsto.congr' _ this

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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)
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) (𝓝 0)
h :
  ∀ (a : Set α) (h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)) (h''a : IntegrableOn f a μ),
    (ENNReal.toReal ∘ fun (a : Set α) ↦
          HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        a =
      ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
⊢ (ENNReal.toReal ∘ fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)) =ᶠ[v.filterAt x]
    fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ

Tactic:
filter_upwards [v.eventually_measure_lt_top x, v.eventually_filterAt_integrableOn x hf]
    with a h'a h''a

Premises used: VitaliFamily.eventually_filterAt_integrableOn, VitaliFamily.eventually_measure_lt_top
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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)
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) (𝓝 0)
a : Set α
h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h''a : IntegrableOn f a μ
h :
  (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) a))⁻¹ * (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ).toReal =
    HSMul.hSMul (β := ℝ) (μ.real a)⁻¹ (∫ (y : α) in a, ‖f y - f x‖ ∂μ)
⊢ (ENNReal.toReal ∘ fun (a : Set α) ↦
        HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      a =
    ⨍ (y : α) in a, ‖f y - f x‖ ∂μ

Tactic:
simp only [Function.comp_apply, ENNReal.toReal_div, setAverage_eq, div_eq_inv_mul]

Premises used: MeasureTheory.setAverage_eq, Function.comp_apply, div_eq_inv_mul, ENNReal.toReal_div
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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)
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) (𝓝 0)
a : Set α
h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h''a : IntegrableOn f a μ
simp_rw : IntegrableOn (ε := ℝ) (fun (y : α) ↦ ‖f y - f x‖) a μ
⊢ IntegrableOn (ε := ℝ) (fun (y : α) ↦ (↑‖f y - f x‖₊ : ℝ)) a μ

Tactic:
simp_rw [coe_nnnorm]

Premises used: coe_nnnorm
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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)
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) (𝓝 0)
a : Set α
h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h''a : IntegrableOn f a μ
⊢ IntegrableOn (ε := ℝ) (fun (y : α) ↦ ‖f y - f x‖) a μ

Tactic:
(h''a.sub (integrableOn_const h'a.ne)).norm

Premises used: MeasureTheory.IntegrableOn.sub, MeasureTheory.IntegrableOn, MeasureTheory.integrableOn_const, MeasureTheory.Integrable.norm, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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)
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) (𝓝 0)
a : Set α
h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h''a : IntegrableOn f a μ
⊢ IntegrableOn (ε := ℝ) (fun (y : α) ↦ ‖f y - f x‖) a μ

Tactic:
exact (h''a.sub (integrableOn_const h'a.ne)).norm

Premises used: MeasureTheory.IntegrableOn.sub, MeasureTheory.integrableOn_const, MeasureTheory.Integrable.norm, LT.lt.ne