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 μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦
      HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
a : ℝ≥0
ht : Membership.mem (γ := Set ℝ≥0) (Ioi 1) a
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑a : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
v.le_mul_withDensity hρ hs ht

Premises used: VitaliFamily.le_mul_withDensity
-- 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 μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦
      HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
a : ℝ≥0
ht : Membership.mem (γ := Set ℝ≥0) (Ioi 1) a
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑a : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact v.le_mul_withDensity hρ hs ht

Premises used: VitaliFamily.le_mul_withDensity
-- 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 μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ (μ.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ρ)
-- 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 μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : (μ.withDensity (v.limRatioMeas hρ)).rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ
⊢ ρ.rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ

Tactic:
rw [v.withDensity_limRatioMeas_eq hρ] at A

Premises used: VitaliFamily.withDensity_limRatioMeas_eq
-- 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 μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : ρ.rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ
a : α
h :
  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)) →
    ρ.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))
⊢ 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)) →
    ρ.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:
_
-- 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 μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : ρ.rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ
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))
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))

Tactic:
filter_upwards [v.ae_tendsto_limRatioMeas hρ, A] with _ _ h'x

Premises used: VitaliFamily.ae_tendsto_limRatioMeas
-- 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 μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : ρ.rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ
a : α
h_1 :
  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
h h₁ h₂ h₃ :
  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))
⊢ Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt a) (𝓝 (ρ.rnDeriv μ a))

Tactic:
rwa [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 μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
t : Measure α := μ.withDensity (ρ.rnDeriv μ)
⊢ ρ = ρ.singularPart μ + t

Tactic:
have eq_add : ρ = ρ.singularPart μ + t := haveLebesgueDecomposition_add _ _
-- 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 μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
t : Measure α := μ.withDensity (ρ.rnDeriv μ)
eq_add : ρ = ρ.singularPart μ + t
⊢ ∀ᵐ (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 ρ μ)
-- 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 μ
ρ : 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 : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x

Tactic:
have B : ∀ᵐ x ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x :=
    rnDeriv_withDensity μ (measurable_rnDeriv ρ μ)
-- 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 μ
ρ : 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))
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))
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))

Tactic:
filter_upwards [A, B, C] with _ Ax Bx Cx
-- 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 μ
ρ : 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 (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∞))
    (v.filterAt a) (𝓝 (0 + t.rnDeriv μ a))

Tactic:
Ax.add Cx

Premises used: Filter.Tendsto.add
-- 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 μ
ρ : 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∞)
h₁ : 𝓝 (ρ.rnDeriv μ a) = 𝓝 (0 + 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:
convert! Ax.add Cx using 1

Premises used: Filter.Tendsto.add
-- 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 μ
ρ : 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 :
  ∀ (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∞)
⊢ 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:
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 μ
ρ : 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 α
rw :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.singularPart μ + t : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
| HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
rw [eq_add]
-- 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 μ
ρ : 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 α
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∞)
⊢ 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:
conv_lhs => rw [eq_add]
-- 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 μ
ρ : 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∞) ((ρ.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:
simp only [Pi.add_apply, coe_add, ENNReal.add_div]

Premises used: MeasureTheory.Measure.coe_add, Pi.add_apply, ENNReal.add_div
-- 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 μ
ρ : 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))
⊢ 𝓝 (ρ.rnDeriv μ a) = 𝓝 (0 + t.rnDeriv μ a)

Tactic:
simp only [Bx, zero_add]

Premises used: zero_add
-- 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 μ
s : Set α
hs : MeasurableSet s
⊢ IsLocallyFiniteMeasure (μ.restrict s)

Tactic:
haveI : IsLocallyFiniteMeasure (μ.restrict s) :=
    isLocallyFiniteMeasure_of_le restrict_le_self