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 μ
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:
have A : IntegrableOn (fun y => (‖f y - f x‖₊ : ℝ)) a μ := by
    simp_rw [coe_nnnorm]
    exact (h''a.sub (integrableOn_const h'a.ne)).norm
-- 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 μ
A : IntegrableOn (ε := ℝ) (fun (y : α) ↦ (↑‖f y - f x‖₊ : ℝ)) a μ
⊢ LE.le (α := ℝ) 0 (∫ (a : α) in a, (↑‖f a - f x‖₊ : ℝ) ∂μ)

Tactic:
positivity
-- 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 μ
A : IntegrableOn (ε := ℝ) (fun (y : α) ↦ (↑‖f y - f x‖₊ : ℝ)) a μ
h :
  (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) a))⁻¹ * ∫ (a : α) in a, (↑‖f a - f x‖₊ : ℝ) ∂μ =
    (μ.real a)⁻¹ * ∫ (y : α) in a, ‖f y - f x‖ ∂μ
⊢ (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) a))⁻¹ * (∫⁻ (y : α) in a, (↑‖f y - f x‖₊ : ℝ≥0∞) ∂μ).toReal =
    (μ.real a)⁻¹ * ∫ (y : α) in a, ‖f y - f x‖ ∂μ

Tactic:
rw [lintegral_coe_eq_integral _ A, ENNReal.toReal_ofReal (by positivity)]

Premises used: ENNReal.toReal_ofReal, MeasureTheory.lintegral_coe_eq_integral
-- 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 μ
A : IntegrableOn (ε := ℝ) (fun (y : α) ↦ (↑‖f y - f x‖₊ : ℝ)) a μ
⊢ (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) a))⁻¹ * ∫ (a : α) in a, (↑‖f a - f x‖₊ : ℝ) ∂μ =
    (μ.real a)⁻¹ * ∫ (y : α) in a, ‖f y - f x‖ ∂μ

Tactic:
simp only [coe_nnnorm, measureReal_def]

Premises used: coe_nnnorm, MeasureTheory.measureReal_def
-- 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
h :
  ∀ (x : α) (hx : Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0))
    (h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)),
    Tendsto (fun (a : Set α) ↦ ⨍ (y : α) in a, f y ∂μ) (v.filterAt x) (𝓝 (f x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (a : Set α) ↦ ⨍ (y : α) in a, f y ∂μ) (v.filterAt x) (𝓝 (f x))

Tactic:
filter_upwards [v.ae_tendsto_average_norm_sub hf, v.ae_eventually_measure_pos] with x hx h'x

Premises used: VitaliFamily.ae_tendsto_average_norm_sub, VitaliFamily.ae_eventually_measure_pos
-- 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h : Tendsto (β := ℝ) (fun (e : Set α) ↦ ‖⨍ (y : α) in e, f y ∂μ - f x‖) (v.filterAt x) (𝓝 0)
⊢ Tendsto (fun (a : Set α) ↦ ⨍ (y : α) in a, f y ∂μ) (v.filterAt x) (𝓝 (f x))

Tactic:
rw [tendsto_iff_norm_sub_tendsto_zero]

Premises used: tendsto_iff_norm_sub_tendsto_zero
-- 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ Tendsto (β := ℝ) (fun (e : Set α) ↦ ‖⨍ (y : α) in e, f y ∂μ - f x‖) (v.filterAt x) (𝓝 0)

Tactic:
squeeze_zero' (Eventually.of_forall fun a => norm_nonneg _) ?_ hx

Premises used: HSub.hSub, MeasureTheory.Measure.restrict, Filter.Eventually.of_forall, MeasureTheory.average, norm_nonneg, squeeze_zero'
-- 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h : ∀ᶠ (t : Set α) in v.filterAt x, ‖⨍ (y : α) in t, f y ∂μ - f x‖ ≤ ⨍ (y : α) in t, ‖f y - f x‖ ∂μ
⊢ Tendsto (β := ℝ) (fun (e : Set α) ↦ ‖⨍ (y : α) in e, f y ∂μ - f x‖) (v.filterAt x) (𝓝 0)

Tactic:
refine squeeze_zero' (Eventually.of_forall fun a => norm_nonneg _) ?_ hx

Premises used: Filter.Eventually.of_forall, norm_nonneg, squeeze_zero'
-- 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h :
  ∀ (a : Set α) (ha : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)) (h''a : IntegrableOn f a μ),
    ‖⨍ (y : α) in a, f y ∂μ - f x‖ ≤ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
⊢ ∀ᶠ (t : Set α) in v.filterAt x, ‖⨍ (y : α) in t, f y ∂μ - f x‖ ≤ ⨍ (y : α) in t, ‖f y - f x‖ ∂μ

Tactic:
filter_upwards [h'x, v.eventually_measure_lt_top x, v.eventually_filterAt_integrableOn x hf]
    with a ha 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
a : Set α
ha : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h''a : IntegrableOn f a μ
h : ‖HSub.hSub (α := E) (⨍ (y : α) in a, f y ∂μ) (⨍ (x_1 : α) in a, f x ∂μ)‖ ≤ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
⊢ ‖⨍ (y : α) in a, f y ∂μ - f x‖ ≤ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ

Tactic:
nth_rw 1 [← setAverage_const ha.ne' h'a.ne (f x)]

Premises used: LT.lt.ne', MeasureTheory.setAverage_const, 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
a : Set α
ha : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h''a : IntegrableOn f a μ
h :
  ‖HSub.hSub (α := E) (∫ (y : α), f y ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a))
        (∫ (x_1 : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a))‖ ≤
    ∫ (y : α), ‖f y - f x‖ ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a)
⊢ ‖HSub.hSub (α := E) (⨍ (y : α) in a, f y ∂μ) (⨍ (x_1 : α) in a, f x ∂μ)‖ ≤ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ

Tactic:
simp_rw [setAverage_eq']

Premises used: MeasureTheory.setAverage_eq'
-- 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
a : Set α
ha : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h''a : IntegrableOn f a μ
h :
  norm.{u_2} (E := E)
      (∫ (a : α), f a - f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a)) ≤
    ∫ (y : α), ‖f y - f x‖ ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a)
h₁ : Integrable f (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a))
h₂ :
  Integrable.{u_2, u_1} (ε := E) (fun (x_1 : α) ↦ f x)
    (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a))
⊢ ‖HSub.hSub (α := E) (∫ (y : α), f y ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a))
        (∫ (x_1 : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a))‖ ≤
    ∫ (y : α), ‖f y - f x‖ ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a)

Tactic:
rw [← integral_sub]

Premises used: MeasureTheory.integral_sub
-- 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
a : Set α
ha : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h''a : IntegrableOn f a μ
⊢ norm.{u_2} (E := E)
      (∫ (a : α), f a - f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a)) ≤
    ∫ (y : α), ‖f y - f x‖ ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a)

Tactic:
norm_integral_le_integral_norm _

Premises used: MeasureTheory.norm_integral_le_integral_norm
-- 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
a : Set α
ha : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h''a : IntegrableOn f a μ
⊢ norm.{u_2} (E := E)
      (∫ (a : α), f a - f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a)) ≤
    ∫ (y : α), ‖f y - f x‖ ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a)

Tactic:
exact norm_integral_le_integral_norm _

Premises used: MeasureTheory.norm_integral_le_integral_norm
-- 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
a : Set α
ha : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h''a : IntegrableOn f a μ
⊢ Integrable f (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a))

Tactic:
(integrable_inv_smul_measure ha.ne' h'a.ne).2 h''a

Premises used: Iff.mpr, LT.lt.ne', MeasureTheory.integrable_inv_smul_measure, 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
a : Set α
ha : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h''a : IntegrableOn f a μ
⊢ Integrable f (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a))

Tactic:
exact (integrable_inv_smul_measure ha.ne' h'a.ne).2 h''a

Premises used: Iff.mpr, LT.lt.ne', MeasureTheory.integrable_inv_smul_measure, 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
a : Set α
ha : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h''a : IntegrableOn f a μ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x_1 : α) ↦ f x)
    (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a))

Tactic:
(integrable_inv_smul_measure ha.ne' h'a.ne).2 (integrableOn_const h'a.ne)

Premises used: Iff.mpr, LT.lt.ne', MeasureTheory.integrableOn_const, MeasureTheory.integrable_inv_smul_measure, 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
x : α
hx : Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
a : Set α
ha : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h'a : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h''a : IntegrableOn f a μ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x_1 : α) ↦ f x)
    (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a))

Tactic:
exact (integrable_inv_smul_measure ha.ne' h'a.ne).2 (integrableOn_const h'a.ne)

Premises used: Iff.mpr, LT.lt.ne', MeasureTheory.integrableOn_const, MeasureTheory.integrable_inv_smul_measure, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
hMr : ∀ᶠ (i : ℕ) in atTop, M * r₁ i ≤ r₂ i
set :
  let Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i);
  blimsup Y₁ atTop p ≤ᶠ[ae μ] blimsup (fun (i : ℕ) ↦ cthickening (r₂ i) (s i)) atTop p
⊢ (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r₁ i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r₂ i) (s i)) atTop p)

Tactic:
set Y₁ : ℕ → Set α := fun i => cthickening (r₁ i) (s i)

Premises used: Metric.cthickening
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
hMr : ∀ᶠ (i : ℕ) in atTop, M * r₁ i ≤ r₂ i
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
set :
  let Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i);
  blimsup Y₁ atTop p ≤ᶠ[ae μ] blimsup Y₂ atTop p
⊢ blimsup Y₁ atTop p ≤ᶠ[ae μ] blimsup (fun (i : ℕ) ↦ cthickening (r₂ i) (s i)) atTop p

Tactic:
set Y₂ : ℕ → Set α := fun i => cthickening (r₂ i) (s i)

Premises used: Metric.cthickening
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
hMr : ∀ᶠ (i : ℕ) in atTop, M * r₁ i ≤ r₂ i
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
this : ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (blimsup Y₁ atTop p \ Z i) : ℝ≥0∞) (0 : ℝ≥0∞)
rwa : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (blimsup Y₁ atTop p \ blimsup Y₂ atTop p) : ℝ≥0∞) (0 : ℝ≥0∞)
rwa₁ :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (blimsup Y₁ atTop p \ ⨅ (i : ℕ), ⨆ (j : ℕ), ⨆ (_ : p j ∧ i ≤ j), Y₂ j) : ℝ≥0∞) (0 : ℝ≥0∞)
rwa₂ :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (blimsup Y₁ atTop p \ ⋂ (i : ℕ), ⨆ (j : ℕ), ⨆ (_ : p j ∧ i ≤ j), Y₂ j) : ℝ≥0∞) (0 : ℝ≥0∞)
rwa₃ :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), blimsup Y₁ atTop p \ ⨆ (j : ℕ), ⨆ (_ : p j ∧ i ≤ j), Y₂ j) : ℝ≥0∞) (0 : ℝ≥0∞)
rwa₄ rwa₅ rwa₆ rwa₇ :
  ∀ (i : ℕ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (blimsup Y₁ atTop p \ ⨆ (j : ℕ), ⨆ (_ : p j ∧ i ≤ j), Y₂ j) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ blimsup Y₁ atTop p ≤ᶠ[ae μ] blimsup Y₂ atTop p

Tactic:
rwa [ae_le_set, @blimsup_eq_iInf_biSup_of_nat _ _ _ Y₂, iInf_eq_iInter, diff_iInter,
      measure_iUnion_null_iff]

Premises used: Set.iInf_eq_iInter, MeasureTheory.measure_iUnion_null_iff, Filter.blimsup_eq_iInf_biSup_of_nat, Set.diff_iInter, MeasureTheory.ae_le_set
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
hMr : ∀ᶠ (i : ℕ) in atTop, M * r₁ i ≤ r₂ i
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
suffices : ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (blimsup Y₁ atTop p \ Z i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ blimsup Y₁ atTop p ≤ᶠ[ae μ] blimsup Y₂ atTop p

Tactic:
suffices ∀ i, μ (atTop.blimsup Y₁ p \ Z i) = 0 by
    rwa [ae_le_set, @blimsup_eq_iInf_biSup_of_nat _ _ _ Y₂, iInf_eq_iInter, diff_iInter,
      measure_iUnion_null_iff]