awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : Measurable f
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
ρ : Measure α := μ.withDensity f
this : IsFiniteMeasure ρ
x : α
hx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
h'x : (μ.withDensity f).rnDeriv μ x = f x
h :
  ∀ (a : Set α) (ha : MeasurableSet a),
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) =
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, f y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ (v.filterAt x).EventuallyEq (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, f y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
filter_upwards [v.eventually_filterAt_measurableSet x] with a ha

Premises used: VitaliFamily.eventually_filterAt_measurableSet
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : Measurable f
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
ρ : Measure α := μ.withDensity f
this : IsFiniteMeasure ρ
x : α
hx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
h'x : (μ.withDensity f).rnDeriv μ x = f x
a : Set α
ha : MeasurableSet a
h h₁ :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, f y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
rw [← withDensity_apply f ha]

Premises used: MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
⊢ ∫⁻ (y : α), f y ∂μ ≠ ∞

Tactic:
h'f
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
h : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ = ∫⁻ (y : α), f y ∂μ
⊢ ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞

Tactic:
convert! h'f using 1
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
h : AEMeasurable.mk f hf =ᶠ[ae μ] f
⊢ ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ = ∫⁻ (y : α), f y ∂μ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
⊢ AEMeasurable.mk f hf =ᶠ[ae μ] f

Tactic:
hf.ae_eq_mk.symm

Premises used: AEMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
⊢ AEMeasurable.mk f hf =ᶠ[ae μ] f

Tactic:
exact hf.ae_eq_mk.symm

Premises used: AEMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
⊢ ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞

Tactic:
have A : (∫⁻ y, hf.mk f y ∂μ) ≠ ∞ := by
    convert! h'f using 1
    apply lintegral_congr_ae
    exact hf.ae_eq_mk.symm
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞
h :
  ∀ (x : α)
    (hx :
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x)))
    (h'x : f x = AEMeasurable.mk f hf x),
    Tendsto (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, f y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (f x))
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, f y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (f x))

Tactic:
filter_upwards [v.ae_tendsto_lintegral_div' hf.measurable_mk A, hf.ae_eq_mk] with x hx h'x

Premises used: VitaliFamily.ae_tendsto_lintegral_div', AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞
x : α
hx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
h :
  Tendsto (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, f y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
⊢ Tendsto (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, f y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (f x))

Tactic:
rw [h'x]
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞
x : α
hx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
⊢ Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))

Tactic:
hx
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞
x : α
hx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
h :
  Eq.{u_1 + 1} (α := Set α → ℝ≥0∞)
    (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, f y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    fun (a : Set α) ↦
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ Tendsto (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, f y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))

Tactic:
convert! hx using 1
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞
x : α
hx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
h :
  ∀ (a : Set α),
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, f y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) =
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Set α → ℝ≥0∞)
    (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, f y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    fun (a : Set α) ↦
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
ext1 a
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞
x : α
hx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
a : Set α
h : ∫⁻ (y : α) in a, f y ∂μ = ∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ
⊢ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, f y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞
x : α
hx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
a : Set α
h : f =ᶠ[ae (μ.restrict a)] AEMeasurable.mk f hf
⊢ ∫⁻ (y : α) in a, f y ∂μ = ∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞
x : α
hx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
a : Set α
⊢ f =ᶠ[ae (μ.restrict a)] AEMeasurable.mk f hf

Tactic:
ae_restrict_of_ae hf.ae_eq_mk

Premises used: Filter.EventuallyEq, MeasureTheory.ae_restrict_of_ae, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞
x : α
hx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
a : Set α
⊢ f =ᶠ[ae (μ.restrict a)] AEMeasurable.mk f hf

Tactic:
exact ae_restrict_of_ae hf.ae_eq_mk

Premises used: MeasureTheory.ae_restrict_of_ae, AEMeasurable.ae_eq_mk
-- 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 : Integrable f μ
⊢ Integrable (AEStronglyMeasurable.mk f ⋯) μ

Tactic:
have I : Integrable (hf.1.mk f) μ := hf.congr hf.1.ae_eq_mk
-- 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 : Integrable f μ
I : Integrable (AEStronglyMeasurable.mk f ⋯) μ
h :
  ∀ (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)
⊢ ∀ᵐ (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 [v.ae_tendsto_lintegral_enorm_sub_div'_of_integrable I hf.1.stronglyMeasurable_mk,
    hf.1.ae_eq_mk] with x hx h'x

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, And.left, VitaliFamily.ae_tendsto_lintegral_enorm_sub_div'_of_integrable
-- 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 : 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
apply :
  ∀ (x_1 : Set α),
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in x_1, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ)
        ((μ : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥0∞) =
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in x_1, ‖f y - f x‖ₑ ∂μ) ((μ : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥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 hx.congr _

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 : 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 α
e_a :
  ∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ =
    ∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ
⊢ 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∞)

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 : 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 α
e_a :
  (ae (μ.restrict a)).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ ‖AEStronglyMeasurable.mk f ⋯ a - AEStronglyMeasurable.mk f ⋯ x‖ₑ) fun (a : α) ↦ ‖f a - f x‖ₑ
⊢ ∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ =
    ∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- 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 : 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 α
e_a :
  ∀ᵐ (x_1 : α) ∂μ,
    Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ‖AEStronglyMeasurable.mk f ⋯ a - AEStronglyMeasurable.mk f ⋯ x‖ₑ) x_1)
      ((fun (a : α) ↦ ‖f a - f x‖ₑ) x_1)
⊢ (ae (μ.restrict a)).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ ‖AEStronglyMeasurable.mk f ⋯ a - AEStronglyMeasurable.mk f ⋯ x‖ₑ) fun (a : α) ↦ ‖f a - f x‖ₑ

Tactic:
apply ae_restrict_of_ae

Premises used: MeasureTheory.ae_restrict_of_ae
-- 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 : 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 α
h :
  ∀ (y : α) (hy : f y = AEStronglyMeasurable.mk f ⋯ y),
    ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ = ‖f y - f x‖ₑ
⊢ ∀ᵐ (x_1 : α) ∂μ,
    Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ‖AEStronglyMeasurable.mk f ⋯ a - AEStronglyMeasurable.mk f ⋯ x‖ₑ) x_1)
      ((fun (a : α) ↦ ‖f a - f x‖ₑ) x_1)

Tactic:
filter_upwards [hf.1.ae_eq_mk] with y hy

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, And.left
-- 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 : 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‖ₑ
h₁ h₂ :
  ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ =
    ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ
⊢ ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ = ‖f y - f x‖ₑ

Tactic:
rw [hy, h'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 μ
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)
⊢ ∀ᵐ (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⟩

Premises used: MeasureTheory.LocallyIntegrable.exists_nat_integrableOn
-- 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 : ℕ
hf₁ : Integrable ((u n).indicator f) μ
⊢ ∀ᵐ (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:
apply ae_tendsto_lintegral_enorm_sub_div_of_integrable

Premises used: VitaliFamily.ae_tendsto_lintegral_enorm_sub_div_of_integrable