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 μ
s : Set α
hs : MeasurableSet s
this : IsLocallyFiniteMeasure (μ.restrict s)
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))
⊢ ∀ᵐ (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))

Tactic:
filter_upwards [ae_tendsto_rnDeriv v (μ.restrict s), rnDeriv_restrict_self μ hs]

Premises used: MeasureTheory.Measure.restrict, VitaliFamily.ae_tendsto_rnDeriv, MeasureTheory.Measure.rnDeriv_restrict_self
-- 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
this : IsLocallyFiniteMeasure (μ.restrict s)
x : α
hx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 ((μ.restrict s).rnDeriv μ x))
h'x : (μ.restrict s).rnDeriv μ x = s.indicator 1 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))

Tactic:
simpa only [h'x, restrict_apply' hs, inter_comm] using hx

Premises used: Set.inter_comm, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
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 μ
⊢ ∀ᵐ (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:
apply ae_mono restrict_le_self

Premises used: MeasureTheory.ae_mono, MeasureTheory.Measure.restrict_le_self
-- 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 α
t : Set α := toMeasurable μ s
a : MeasurableSet t
⊢ {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_tendsto_measure_inter_div_of_measurableSet

Premises used: VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
⊢ MeasurableSet t

Tactic:
measurableSet_toMeasurable _ _

Premises used: MeasureTheory.measurableSet_toMeasurable
-- 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 α
t : Set α := toMeasurable μ s
⊢ MeasurableSet t

Tactic:
exact measurableSet_toMeasurable _ _

Premises used: MeasureTheory.measurableSet_toMeasurable
-- 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 α
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))

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 _ _
-- 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 α
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

Tactic:
ae_restrict_of_ae_restrict_of_subset (subset_toMeasurable μ s) ?_

Premises used: MeasureTheory.subset_toMeasurable, MeasureTheory.ae_restrict_of_ae_restrict_of_subset
-- 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 α
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))
refine : ∀ᵐ (x : α) ∂μ.restrict (toMeasurable μ s), Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
⊢ ∀ᵐ (x : α) ∂μ.restrict s, Eq (α := ℝ≥0∞) (t.indicator 1 x) 1

Tactic:
refine ae_restrict_of_ae_restrict_of_subset (subset_toMeasurable μ s) ?_

Premises used: MeasureTheory.subset_toMeasurable, MeasureTheory.ae_restrict_of_ae_restrict_of_subset
-- 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 α
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))
h : ∀ (a : α) (hx : a ∈ toMeasurable μ s), Eq (α := ℝ≥0∞) (t.indicator 1 a) 1
⊢ ∀ᵐ (x : α) ∂μ.restrict (toMeasurable μ s), Eq (α := ℝ≥0∞) (t.indicator 1 x) 1

Tactic:
filter_upwards [ae_restrict_mem (measurableSet_toMeasurable μ s)] with _ hx

Premises used: MeasureTheory.ae_restrict_mem, MeasureTheory.measurableSet_toMeasurable
-- 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 α
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))
a : α
hx : a ∈ toMeasurable μ s
⊢ Eq (α := ℝ≥0∞) (t.indicator 1 a) 1

Tactic:
simp only [t, hx, Pi.one_apply, indicator_of_mem]

Premises used: Pi.one_apply, Set.indicator_of_mem
-- 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 α
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

Tactic:
have B : ∀ᵐ x ∂μ.restrict s, t.indicator 1 x = (1 : ℝ≥0∞) := by
    refine ae_restrict_of_ae_restrict_of_subset (subset_toMeasurable μ s) ?_
    filter_upwards [ae_restrict_mem (measurableSet_toMeasurable μ s)] with _ hx
    simp only [t, hx, Pi.one_apply, indicator_of_mem]
-- 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 α
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))
B : ∀ᵐ (x : α) ∂μ.restrict s, Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
h :
  ∀ (x : α)
    (hx :
      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)))
    (h'x : Eq (α := ℝ≥0∞) (t.indicator 1 x) 1),
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 1)
⊢ ∀ᵐ (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)

Tactic:
filter_upwards [A, B] with x hx 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 μ
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))
B : ∀ᵐ (x : α) ∂μ.restrict s, Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
x : α
hx :
  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))
h'x : Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
⊢ Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 1)

Tactic:
rw [h'x] at hx
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
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))
B : ∀ᵐ (x : α) ∂μ.restrict s, Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
x : α
hx :
  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))
h'x : Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
hx₁ :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 1)
⊢ Eq (α := ℝ≥0∞) (t.indicator 1 x) 1

Tactic:
rw [h'x] at hx
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
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))
B : ∀ᵐ (x : α) ∂μ.restrict s, Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
x : α
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 1)
h'x : Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
apply :
  (v.filterAt x).EventuallyEq (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    fun (a : Set α) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 1)

Tactic:
apply hx.congr' _

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
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))
B : ∀ᵐ (x : α) ∂μ.restrict s, Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
x : α
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 1)
h'x : Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
h :
  ∀ (a : Set α) (ha : MeasurableSet a),
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) =
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ (v.filterAt x).EventuallyEq (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    fun (a : Set α) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

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

Premises used: VitaliFamily.eventually_filterAt_measurableSet
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
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))
B : ∀ᵐ (x : α) ∂μ.restrict s, Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
x : α
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 1)
h'x : Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
a : Set α
ha : MeasurableSet a
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
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))
B : ∀ᵐ (x : α) ∂μ.restrict s, Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
x : α
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 1)
h'x : Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
a : Set α
ha : MeasurableSet a
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞)

Tactic:
measure_toMeasurable_inter_of_sFinite ha _

Premises used: MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite
-- 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 α
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))
B : ∀ᵐ (x : α) ∂μ.restrict s, Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
x : α
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 1)
h'x : Eq (α := ℝ≥0∞) (t.indicator 1 x) 1
a : Set α
ha : MeasurableSet a
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞)

Tactic:
exact measure_toMeasurable_inter_of_sFinite ha _

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

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

Tactic:
filter_upwards [ae_tendsto_rnDeriv v ρ, rnDeriv_withDensity μ hf] with x hx h'x

Premises used: MeasureTheory.Measure.rnDeriv_withDensity, VitaliFamily.ae_tendsto_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 μ
f : α → ℝ≥0∞
hf : Measurable f
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
ρ : Measure α := μ.withDensity f
this : IsFiniteMeasure ρ
x : α
hx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
h'x : (μ.withDensity f).rnDeriv μ x = f x
h :
  Tendsto (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, f y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 ((μ.withDensity f).rnDeriv μ x))
⊢ Tendsto (fun (a : Set α) ↦ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (y : α) in a, f y ∂μ) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (f x))

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

Tactic:
apply hx.congr' _

Premises used: Filter.Tendsto.congr'