awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
have A : (μ.withDensity (v.limRatioMeas hρ)).rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ
Tactic: have A : (μ.withDensity (v.limRatioMeas hρ)).rnDeriv μ =ᵐ[μ] v.limRatioMeas hρ :=
    rnDeriv_withDensity μ (v.limRatioMeas_measurable hρ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : (μ.withDensity (v.limRatioMeas hρ)).rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
have A₁ : ρ.rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ
Tactic: rw [v.withDensity_limRatioMeas_eq hρ] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : ρ.rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
have h : ∀ (a : α),
  Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt a) (𝓝 (v.limRatioMeas hρ a)) →
    ∀ (h'x : ρ.rnDeriv μ a = v.limRatioMeas hρ a),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt a) (𝓝 (ρ.rnDeriv μ a))
Tactic: filter_upwards [v.ae_tendsto_limRatioMeas hρ, A] with _ _ h'x
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
t : Measure α := μ.withDensity (ρ.rnDeriv μ)
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
have eq_add : ρ = ρ.singularPart μ + t
Tactic: have eq_add : ρ = ρ.singularPart μ + t := haveLebesgueDecomposition_add _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
t : Measure α := μ.withDensity (ρ.rnDeriv μ)
eq_add : ρ = ρ.singularPart μ + t
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
have A : ∀ᵐ (x : α) ∂μ,
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)
Tactic: have A : ∀ᵐ x ∂μ, Tendsto (fun a => ρ.singularPart μ a / μ a) (v.filterAt x) (𝓝 0) :=
    v.ae_eventually_measure_zero_of_singular (mutuallySingular_singularPart ρ μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
t : Measure α := μ.withDensity (ρ.rnDeriv μ)
eq_add : ρ = ρ.singularPart μ + t
A :
  ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
have B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x
Tactic: have B : ∀ᵐ x ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x :=
    rnDeriv_withDensity μ (measurable_rnDeriv ρ μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
t : Measure α := μ.withDensity (ρ.rnDeriv μ)
eq_add : ρ = ρ.singularPart μ + t
A :
  ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x
C :
  ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (t.rnDeriv μ x))
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
have h : ∀ (a : α)
  (Ax :
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt a) (𝓝 0))
  (Bx : t.rnDeriv μ a = ρ.rnDeriv μ a)
  (Cx :
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt a) (𝓝 (t.rnDeriv μ a))),
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt a) (𝓝 (ρ.rnDeriv μ a))
Tactic: filter_upwards [A, B, C] with _ Ax Bx Cx
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
t : Measure α := μ.withDensity (ρ.rnDeriv μ)
eq_add : ρ = ρ.singularPart μ + t
A :
  ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x
C :
  ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (t.rnDeriv μ x))
a : α
Ax :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt a) (𝓝 0)
Bx : t.rnDeriv μ a = ρ.rnDeriv μ a
Cx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt a) (𝓝 (t.rnDeriv μ a))
⊢ Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt a) (𝓝 (ρ.rnDeriv μ a))
have h : Eq.{u_1 + 1} (α := Set α → ℝ≥0∞)
  (fun (a : Set α) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
  fun (x : Set α) ↦
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) +
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
Tactic: convert! Ax.add Cx using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
t : Measure α := μ.withDensity (ρ.rnDeriv μ)
eq_add : ρ = ρ.singularPart μ + t
A :
  ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x
C :
  ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (t.rnDeriv μ x))
a : α
Ax :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt a) (𝓝 0)
Bx : t.rnDeriv μ a = ρ.rnDeriv μ a
Cx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt a) (𝓝 (t.rnDeriv μ a))
h :
  Eq.{u_1 + 1} (α := Set α → ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    fun (x : Set α) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
⊢ Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt a) (𝓝 (ρ.rnDeriv μ a))
have h₁ : 𝓝 (ρ.rnDeriv μ a) = 𝓝 (0 + t.rnDeriv μ a)
Tactic: convert! Ax.add Cx using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
t : Measure α := μ.withDensity (ρ.rnDeriv μ)
eq_add : ρ = ρ.singularPart μ + t
A :
  ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x
C :
  ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (t.rnDeriv μ x))
a : α
Ax :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt a) (𝓝 0)
Bx : t.rnDeriv μ a = ρ.rnDeriv μ a
Cx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt a) (𝓝 (t.rnDeriv μ a))
⊢ Eq.{u_1 + 1} (α := Set α → ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    fun (x : Set α) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
have h : ∀ (a : Set α),
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
t : Measure α := μ.withDensity (ρ.rnDeriv μ)
eq_add : ρ = ρ.singularPart μ + t
A :
  ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x
C :
  ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (t.rnDeriv μ x))
a_1 : α
Ax :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt a_1) (𝓝 0)
Bx : t.rnDeriv μ a_1 = ρ.rnDeriv μ a_1
Cx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt a_1) (𝓝 (t.rnDeriv μ a_1))
a : Set α
| HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
have rw : HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ + t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: rw [eq_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
t : Measure α := μ.withDensity (ρ.rnDeriv μ)
eq_add : ρ = ρ.singularPart μ + t
A :
  ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x
C :
  ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (t.rnDeriv μ x))
a_1 : α
Ax :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt a_1) (𝓝 0)
Bx : t.rnDeriv μ a_1 = ρ.rnDeriv μ a_1
Cx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt a_1) (𝓝 (t.rnDeriv μ a_1))
a : Set α
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
have h : HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ + t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) =
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) +
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: conv_lhs => rw [eq_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (s.indicator 1 x))
have this : IsLocallyFiniteMeasure (μ.restrict s)
Tactic: haveI : IsLocallyFiniteMeasure (μ.restrict s) :=
    isLocallyFiniteMeasure_of_le restrict_le_self
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
s : Set α
hs : MeasurableSet s
this : IsLocallyFiniteMeasure (μ.restrict s)
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (s.indicator 1 x))
have h : ∀ (a : α),
  Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt a) (𝓝 ((μ.restrict s).rnDeriv μ a)) →
    (μ.restrict s).rnDeriv μ a = s.indicator 1 a →
      Tendsto (β := ℝ≥0∞)
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt a) (𝓝 (s.indicator 1 a))
Tactic: filter_upwards [ae_tendsto_rnDeriv v (μ.restrict s), rnDeriv_restrict_self μ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (t.indicator 1 x))
have a : {x : α |
    (fun (x : α) ↦
        Tendsto (β := ℝ≥0∞)
          (fun (a : Set α) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
          (v.filterAt x) (𝓝 (t.indicator 1 x)))
      x} ∈
  ae μ
Tactic: apply ae_mono restrict_le_self
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
⊢ {x : α |
      (fun (x : α) ↦
          Tendsto (β := ℝ≥0∞)
            (fun (a : Set α) ↦
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞)
                ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
            (v.filterAt x) (𝓝 (t.indicator 1 x)))
        x} ∈
    ae μ
have a : MeasurableSet t
Tactic: apply ae_tendsto_measure_inter_div_of_measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 1)
have A : ∀ᵐ (x : α) ∂μ.restrict s,
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (t.indicator 1 x))
Tactic: have A :
    ∀ᵐ x ∂μ.restrict s,
      Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x)) := by
    apply ae_mono restrict_le_self
    apply ae_tendsto_measure_inter_div_of_measurableSet
    exact measurableSet_toMeasurable _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A :
  ∀ᵐ (x : α) ∂μ.restrict s,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (t.indicator 1 x))
⊢ ∀ᵐ (x : α) ∂μ.restrict s, Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
have refine : ∀ᵐ (x : α) ∂μ.restrict (toMeasurable μ s), Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
Tactic: refine ae_restrict_of_ae_restrict_of_subset (subset_toMeasurable μ s) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A :
  ∀ᵐ (x : α) ∂μ.restrict s,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (t.indicator 1 x))
⊢ ∀ᵐ (x : α) ∂μ.restrict (toMeasurable μ s), Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
have h : ∀ (a : α) (hx : a ∈ toMeasurable μ s), Eq (α := ℝ≥0∞) (t.indicator 1 a) 1
Tactic: filter_upwards [ae_restrict_mem (measurableSet_toMeasurable μ s)] with _ hx