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 : 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)
⊢ Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
have 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‖ ∂μ
Tactic: apply Tendsto.congr' _ this
-- 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 : α
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)
⊢ (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‖ ∂μ
have 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‖ ∂μ
Tactic: filter_upwards [v.eventually_measure_lt_top x, v.eventually_filterAt_integrableOn x hf]
    with a h'a 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 μ
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 μ
⊢ (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‖ ∂μ
have 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‖ ∂μ)
Tactic: simp only [Function.comp_apply, ENNReal.toReal_div, setAverage_eq, div_eq_inv_mul]
-- 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 : α
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 μ
have simp_rw : IntegrableOn (ε := ℝ) (fun (y : α) ↦ ‖f y - f x‖) a μ
Tactic: simp_rw [coe_nnnorm]
-- 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)
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 μ
⊢ (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‖ ∂μ)
have 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
-- 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 : α
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))⁻¹ * (∫⁻ (y : α) in a, (↑‖f y - f x‖₊ : ℝ≥0∞) ∂μ).toReal =
    (μ.real a)⁻¹ * ∫ (y : α) in a, ‖f y - f x‖ ∂μ
have h : (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) a))⁻¹ * ∫ (a : α) in a, (↑‖f a - f x‖₊ : ℝ) ∂μ =
  (μ.real a)⁻¹ * ∫ (y : α) in a, ‖f y - f x‖ ∂μ
Tactic: rw [lintegral_coe_eq_integral _ A, ENNReal.toReal_ofReal (by positivity)]
-- 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 μ
inst_5 : NormedSpace ℝ E
inst_6 : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (a : Set α) ↦ ⨍ (y : α) in a, f y ∂μ) (v.filterAt x) (𝓝 (f x))
have 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))
Tactic: filter_upwards [v.ae_tendsto_average_norm_sub hf, v.ae_eventually_measure_pos] with x hx 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 μ
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 (a : Set α) ↦ ⨍ (y : α) in a, f y ∂μ) (v.filterAt x) (𝓝 (f x))
have h : Tendsto (β := ℝ) (fun (e : Set α) ↦ ‖⨍ (y : α) in e, f y ∂μ - f x‖) (v.filterAt x) (𝓝 0)
Tactic: rw [tendsto_iff_norm_sub_tendsto_zero]
-- 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 μ
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)
have h : ∀ᶠ (t : Set α) in v.filterAt x, ‖⨍ (y : α) in t, f y ∂μ - f x‖ ≤ ⨍ (y : α) in t, ‖f y - f x‖ ∂μ
Tactic: refine squeeze_zero' (Eventually.of_forall fun a => norm_nonneg _) ?_ 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 μ
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∞)
⊢ ∀ᶠ (t : Set α) in v.filterAt x, ‖⨍ (y : α) in t, f y ∂μ - f x‖ ≤ ⨍ (y : α) in t, ‖f y - f x‖ ∂μ
have 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‖ ∂μ
Tactic: filter_upwards [h'x, v.eventually_measure_lt_top x, v.eventually_filterAt_integrableOn x hf]
    with a ha h'a 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 μ
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 μ
⊢ ‖⨍ (y : α) in a, f y ∂μ - f x‖ ≤ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
have h : ‖HSub.hSub (α := E) (⨍ (y : α) in a, f y ∂μ) (⨍ (x_1 : α) in a, f x ∂μ)‖ ≤ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
Tactic: nth_rw 1 [← setAverage_const ha.ne' h'a.ne (f 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 μ
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 μ
⊢ ‖HSub.hSub (α := E) (⨍ (y : α) in a, f y ∂μ) (⨍ (x_1 : α) in a, f x ∂μ)‖ ≤ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ
have 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)
Tactic: simp_rw [setAverage_eq']
-- 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 μ
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 μ
⊢ ‖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)
have 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)
Tactic: rw [← integral_sub]
-- 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 μ
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)
⊢ ‖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)
have h₁ : Integrable f (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a))
Tactic: rw [← integral_sub]
-- 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 μ
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))
⊢ ‖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)
have h₂ : Integrable.{u_2, u_1} (ε := E) (fun (x_1 : α) ↦ f x)
  (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞) (μ.restrict a))
Tactic: rw [← integral_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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∞)
⊢ blimsup Y₁ atTop p ≤ᶠ[ae μ] blimsup Y₂ atTop p
have rwa : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (blimsup Y₁ atTop p \ blimsup Y₂ atTop p) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rwa [ae_le_set, @blimsup_eq_iInf_biSup_of_nat _ _ _ Y₂, iInf_eq_iInter, diff_iInter,
      measure_iUnion_null_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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∞)
⊢ blimsup Y₁ atTop p ≤ᶠ[ae μ] blimsup Y₂ atTop p
have rwa₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (blimsup Y₁ atTop p \ ⨅ (i : ℕ), ⨆ (j : ℕ), ⨆ (_ : p j ∧ i ≤ j), Y₂ j) : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rwa [ae_le_set, @blimsup_eq_iInf_biSup_of_nat _ _ _ Y₂, iInf_eq_iInter, diff_iInter,
      measure_iUnion_null_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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∞)
⊢ blimsup Y₁ atTop p ≤ᶠ[ae μ] blimsup Y₂ atTop p
have rwa₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (blimsup Y₁ atTop p \ ⋂ (i : ℕ), ⨆ (j : ℕ), ⨆ (_ : p j ∧ i ≤ j), Y₂ j) : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rwa [ae_le_set, @blimsup_eq_iInf_biSup_of_nat _ _ _ Y₂, iInf_eq_iInter, diff_iInter,
      measure_iUnion_null_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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∞)
⊢ blimsup Y₁ atTop p ≤ᶠ[ae μ] blimsup Y₂ atTop p
have rwa₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), blimsup Y₁ atTop p \ ⨆ (j : ℕ), ⨆ (_ : p j ∧ i ≤ j), Y₂ j) : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rwa [ae_le_set, @blimsup_eq_iInf_biSup_of_nat _ _ _ Y₂, iInf_eq_iInter, diff_iInter,
      measure_iUnion_null_iff]