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ρ : ρ ≪ μ
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
m n : ℕ
I : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (u m) : ℝ≥0∞) (∞ : ℝ≥0∞)
J : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)
rw :
  LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ w n) : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ w n) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ w n) : ℝ≥0∞) ≤
    (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ w n)

Tactic:
rw [← coe_nnreal_smul_apply]

Premises used: MeasureTheory.Measure.coe_nnreal_smul_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 μ
ρ : 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
m n : ℕ
I : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (u m) : ℝ≥0∞) (∞ : ℝ≥0∞)
J : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ w n) : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ w n) : ℝ≥0∞)

Tactic:
v.measure_le_of_frequently_le _ (.smul_left .rfl _) _ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left, VitaliFamily.measure_le_of_frequently_le, MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- 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
m n : ℕ
I : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (u m) : ℝ≥0∞) (∞ : ℝ≥0∞)
J : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)
refine :
  ∀ x ∈ toMeasurable (ρ + μ) (u m) ∩ w n,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ w n) : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ w n) : ℝ≥0∞)

Tactic:
refine v.measure_le_of_frequently_le _ (.smul_left .rfl _) _ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left, VitaliFamily.measure_le_of_frequently_le, MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- 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
m n : ℕ
I : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (u m) : ℝ≥0∞) (∞ : ℝ≥0∞)
J : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
⊢ 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:
have L : Tendsto (fun a : Set α => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x)) :=
          tendsto_nhds_limUnder hx.2.1.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 μ
ρ : 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
m n : ℕ
I : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (u m) : ℝ≥0∞) (∞ : ℝ≥0∞)
J : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (v.limRatio ρ x))
⊢ ∀ᶠ (b : Set α) in v.filterAt x,
    (↑q : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
have I : ∀ᶠ b : Set α in v.filterAt x, (q : ℝ≥0∞) < ρ b / μ b :=
          (tendsto_order.1 L).1 _ hx.2.1.2
-- 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
m n : ℕ
I_1 : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (u m) : ℝ≥0∞) (∞ : ℝ≥0∞)
J : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (v.limRatio ρ x))
I :
  ∀ᶠ (b : Set α) in v.filterAt x,
    (↑q : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞)
apply :
  ∀ (a : Set α)
    (ha :
      (↑q : ℝ≥0∞) <
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ ∃ᶠ (a : Set α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
apply I.frequently.mono fun a ha => ?_

Premises used: Filter.Frequently.mono, Filter.Eventually.frequently
-- 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
m n : ℕ
I_1 : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (u m) : ℝ≥0∞) (∞ : ℝ≥0∞)
J : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (v.limRatio ρ x))
I :
  ∀ᶠ (b : Set α) in v.filterAt x,
    (↑q : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞)
a : Set α
ha :
  (↑q : ℝ≥0∞) <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
rw : HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
⊢ LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
rw [coe_nnreal_smul_apply]

Premises used: MeasureTheory.Measure.coe_nnreal_smul_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 μ
ρ : 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
m n : ℕ
I_1 : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (u m) : ℝ≥0∞) (∞ : ℝ≥0∞)
J : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (v.limRatio ρ x))
I :
  ∀ᶠ (b : Set α) in v.filterAt x,
    (↑q : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞)
a : Set α
ha :
  (↑q : ℝ≥0∞) <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a

Tactic:
ENNReal.mul_le_of_le_div ha.le

Premises used: LT.lt.le, ENNReal.mul_le_of_le_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ρ : ρ ≪ μ
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
m n : ℕ
I_1 : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (u m) : ℝ≥0∞) (∞ : ℝ≥0∞)
J : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (v.limRatio ρ x))
I :
  ∀ᶠ (b : Set α) in v.filterAt x,
    (↑q : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞)
a : Set α
ha :
  (↑q : ℝ≥0∞) <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a

Tactic:
exact ENNReal.mul_le_of_le_div ha.le

Premises used: LT.lt.le, ENNReal.mul_le_of_le_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ρ : ρ ≪ μ
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
m n : ℕ
I : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (u m) : ℝ≥0∞) (∞ : ℝ≥0∞)
J : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)
rw : ((ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (w n) ∩ toMeasurable (ρ + μ) (u m)) : ℝ≥0∞)
| ((ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- 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
m n : ℕ
I : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (u m) : ℝ≥0∞) (∞ : ℝ≥0∞)
J : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)
conv_rhs :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ w n) : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (w n) ∩ toMeasurable (ρ + μ) (u m)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ w n) : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)

Tactic:
conv_rhs => rw [inter_comm]

Premises used: Set.inter_comm
-- 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
m n : ℕ
I : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (u m) : ℝ≥0∞) (∞ : ℝ≥0∞)
J : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (w n ∩ toMeasurable (ρ + μ) (u m)) : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (w n) ∩ toMeasurable (ρ + μ) (u m)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ w n) : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (w n) ∩ toMeasurable (ρ + μ) (u m)) : ℝ≥0∞)

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- 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
m n : ℕ
I : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (u m) : ℝ≥0∞) (∞ : ℝ≥0∞)
J : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (w n ∩ toMeasurable (ρ + μ) (u m)) : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (w n) ∩ toMeasurable (ρ + μ) (u m)) : ℝ≥0∞)

Tactic:
(measure_toMeasurable_add_inter_left (measurableSet_toMeasurable _ _) J).symm

Premises used: MeasureTheory.Measure.measure_toMeasurable_add_inter_left, MeasureTheory.measurableSet_toMeasurable, Eq.symm
-- 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
m n : ℕ
I : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (u m) : ℝ≥0∞) (∞ : ℝ≥0∞)
J : Ne (α := ℝ≥0∞) ((ρ + μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  (ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (w n ∩ toMeasurable (ρ + μ) (u m)) : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) (toMeasurable (ρ + μ) (w n) ∩ toMeasurable (ρ + μ) (u m)) : ℝ≥0∞)

Tactic:
exact (measure_toMeasurable_add_inter_left (measurableSet_toMeasurable _ _) J).symm

Premises used: MeasureTheory.Measure.measure_toMeasurable_add_inter_left, MeasureTheory.measurableSet_toMeasurable, Eq.symm