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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
A :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ∀ᵐ (x : α) ∂μ,
          ¬((∃ᶠ (a : Set α) in v.filterAt x,
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                  c) ∧
              ∃ᶠ (a : Set α) in v.filterAt x,
                d <
                  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
B :
  ∀ᵐ (x : α) ∂μ,
    ∀ c ∈ w,
      ∀ d ∈ w,
        c < d →
          ¬((∃ᶠ (a : Set α) in v.filterAt x,
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                  c) ∧
              ∃ᶠ (a : Set α) in v.filterAt x,
                d <
                  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
h :
  ∀ (a : α),
    (∀ c ∈ w,
        ∀ d ∈ w,
          c < d →
            ¬((∃ᶠ (a : Set α) in v.filterAt a,
                  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                      ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                    c) ∧
                ∃ᶠ (a : Set α) in v.filterAt a,
                  d <
                    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                      ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))) →
      ∃ (c : ℝ≥0∞),
        Tendsto
          (fun (a : Set α) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
          (v.filterAt a) (𝓝 c)
⊢ ∀ᵐ (x : α) ∂μ,
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)

Tactic:
filter_upwards [B]
-- 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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
A :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ∀ᵐ (x : α) ∂μ,
          ¬((∃ᶠ (a : Set α) in v.filterAt x,
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                  c) ∧
              ∃ᶠ (a : Set α) in v.filterAt x,
                d <
                  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
B :
  ∀ᵐ (x : α) ∂μ,
    ∀ c ∈ w,
      ∀ d ∈ w,
        c < d →
          ¬((∃ᶠ (a : Set α) in v.filterAt x,
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                  c) ∧
              ∃ᶠ (a : Set α) in v.filterAt x,
                d <
                  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
x : α
hx :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ¬((∃ᶠ (a : Set α) in v.filterAt x,
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                c) ∧
            ∃ᶠ (a : Set α) in v.filterAt x,
              d <
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
⊢ ∃ (c : ℝ≥0∞),
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 c)

Tactic:
tendsto_of_no_upcrossings w_dense hx

Premises used: tendsto_of_no_upcrossings
-- 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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
A :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ∀ᵐ (x : α) ∂μ,
          ¬((∃ᶠ (a : Set α) in v.filterAt x,
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                  c) ∧
              ∃ᶠ (a : Set α) in v.filterAt x,
                d <
                  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
B :
  ∀ᵐ (x : α) ∂μ,
    ∀ c ∈ w,
      ∀ d ∈ w,
        c < d →
          ¬((∃ᶠ (a : Set α) in v.filterAt x,
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                  c) ∧
              ∃ᶠ (a : Set α) in v.filterAt x,
                d <
                  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
x : α
hx :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ¬((∃ᶠ (a : Set α) in v.filterAt x,
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                c) ∧
            ∃ᶠ (a : Set α) in v.filterAt x,
              d <
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
⊢ ∃ (c : ℝ≥0∞),
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 c)

Tactic:
exact tendsto_of_no_upcrossings w_dense hx

Premises used: tendsto_of_no_upcrossings
-- 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ρ : ρ ≪ μ
h :
  ∀ (a : α),
    (∃ (c : ℝ≥0∞),
        Tendsto
          (fun (a : Set α) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
          (v.filterAt a) (𝓝 c)) →
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt a) (𝓝 (v.limRatio ρ a))
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatio ρ x))

Tactic:
filter_upwards [v.ae_tendsto_div hρ]

Premises used: VitaliFamily.ae_tendsto_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 ρ
hρ : ρ ≪ μ
x : α
hx :
  ∃ (c : ℝ≥0∞),
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 c)
⊢ Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (v.limRatio ρ x))

Tactic:
tendsto_nhds_limUnder hx

Premises used: VitaliFamily.limRatio, tendsto_nhds_limUnder
-- 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ρ : ρ ≪ μ
x : α
hx :
  ∃ (c : ℝ≥0∞),
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 c)
⊢ Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (v.limRatio ρ x))

Tactic:
exact tendsto_nhds_limUnder hx

Premises used: tendsto_nhds_limUnder
-- 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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α :=
  {x : α |
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ∩ o n
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
⊢ ∃ (a : Set α) (b : Set α),
    MeasurableSet a ∧
      MeasurableSet b ∧
        {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ⊆ a ∧
          {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ⊆ b ∧
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a ∩ b) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (u n),
      toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (w n), ?_, ?_, ?_, ?_, ?_⟩

Premises used: Compl.compl, HAdd.hAdd, And.intro, Exists.intro, MeasureTheory.toMeasurable, Union.union, Set.iUnion
-- 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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α :=
  {x : α |
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ∩ o n
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
refine_1 : MeasurableSet (toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n))
refine_2 : MeasurableSet (toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n))
refine_3 : {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ⊆ toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)
refine_4 : {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ⊆ toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)
refine_5 :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        ((toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)) ∩
          (toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ ∃ (a : Set α) (b : Set α),
    MeasurableSet a ∧
      MeasurableSet b ∧
        {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ⊆ a ∧
          {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ⊆ b ∧
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a ∩ b) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine
    ⟨toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (u n),
      toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (w n), ?_, ?_, ?_, ?_, ?_⟩
-- 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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α :=
  {x : α |
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ∩ o n
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
⊢ MeasurableSet (toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n))

Tactic:
(measurableSet_toMeasurable _ _).union
        (MeasurableSet.iUnion fun n => measurableSet_toMeasurable _ _)

Premises used: MeasureTheory.measurableSet_toMeasurable, HAdd.hAdd, MeasurableSet.union, MeasurableSet.iUnion
-- 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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α :=
  {x : α |
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ∩ o n
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
⊢ MeasurableSet (toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n))

Tactic:
exact
      (measurableSet_toMeasurable _ _).union
        (MeasurableSet.iUnion fun n => measurableSet_toMeasurable _ _)

Premises used: MeasureTheory.measurableSet_toMeasurable, MeasurableSet.union, MeasurableSet.iUnion
-- 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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α :=
  {x : α |
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ∩ o n
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
⊢ MeasurableSet (toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n))

Tactic:
(measurableSet_toMeasurable _ _).union
        (MeasurableSet.iUnion fun n => measurableSet_toMeasurable _ _)

Premises used: MeasureTheory.measurableSet_toMeasurable, HAdd.hAdd, MeasurableSet.union, MeasurableSet.iUnion
-- 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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α :=
  {x : α |
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ∩ o n
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
⊢ MeasurableSet (toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n))

Tactic:
exact
      (measurableSet_toMeasurable _ _).union
        (MeasurableSet.iUnion fun n => measurableSet_toMeasurable _ _)

Premises used: MeasureTheory.measurableSet_toMeasurable, MeasurableSet.union, MeasurableSet.iUnion
-- 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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α :=
  {x : α |
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ∩ o n
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
x : α
hx : Membership.mem (γ := Set α) {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} x
pos : ∀ (h : x ∈ s), x ∈ toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)
neg : ∀ (h : x ∉ s), x ∈ toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)
⊢ x ∈ toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)

Tactic:
by_cases h : x ∈ s
-- 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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α :=
  {x : α |
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ∩ o n
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
x : α
hx : Membership.mem (γ := Set α) {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} x
h : x ∈ s
⊢ x ∈ toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)

Tactic:
Or.inr (mem_iUnion.2 ⟨spanningSetsIndex (ρ + μ) x, ?_⟩)

Premises used: Iff.mpr, Set.union, Set.Mem, setOf, Set.mem_iUnion, MeasureTheory.spanningSetsIndex, HAdd.hAdd, Exists.intro, Or.inr
-- 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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α :=
  {x : α |
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ∩ o n
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
x : α
hx : Membership.mem (γ := Set α) {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} x
h : x ∈ s
pos : x ∈ toMeasurable (ρ + μ) (u (spanningSetsIndex (ρ + μ) x))
⊢ x ∈ toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)

Tactic:
refine Or.inr (mem_iUnion.2 ⟨spanningSetsIndex (ρ + μ) x, ?_⟩)

Premises used: Iff.mpr, Set.mem_iUnion, MeasureTheory.spanningSetsIndex, HAdd.hAdd, Exists.intro, Or.inr
-- 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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α :=
  {x : α |
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ∩ o n
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
x : α
hx : Membership.mem (γ := Set α) {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} x
h : x ∈ s
⊢ x ∈ toMeasurable (ρ + μ) (u (spanningSetsIndex (ρ + μ) x))

Tactic:
subset_toMeasurable _ _ ⟨⟨h, hx⟩, mem_spanningSetsIndex _ _⟩

Premises used: MeasureTheory.subset_toMeasurable, And.intro, MeasureTheory.mem_spanningSetsIndex
-- 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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α :=
  {x : α |
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ∩ o n
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
x : α
hx : Membership.mem (γ := Set α) {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} x
h : x ∈ s
⊢ x ∈ toMeasurable (ρ + μ) (u (spanningSetsIndex (ρ + μ) x))

Tactic:
exact subset_toMeasurable _ _ ⟨⟨h, hx⟩, mem_spanningSetsIndex _ _⟩
-- 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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α :=
  {x : α |
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ∩ o n
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
x : α
hx : Membership.mem (γ := Set α) {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} x
h : x ∉ s
⊢ x ∈ toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)

Tactic:
Or.inl (subset_toMeasurable μ sᶜ h)

Premises used: Set.union, Set.Mem, Compl.compl, setOf, MeasureTheory.subset_toMeasurable, Or.inl
-- 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ρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α :=
  {x : α |
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} ∩ o n
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ s ∩ {x : α | (↑q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
x : α
hx : Membership.mem (γ := Set α) {x : α | v.limRatio ρ x < (↑p : ℝ≥0∞)} x
h : x ∉ s
⊢ x ∈ toMeasurable μ sᶜ ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)

Tactic:
exact Or.inl (subset_toMeasurable μ sᶜ h)

Premises used: Compl.compl, MeasureTheory.subset_toMeasurable, Or.inl