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ρ : ρ ≪ μ
x : α
h : Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x = ∞} x
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = ∞} ∩ o
ρs : Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (q : ℝ≥0),
    1 ≤ q → (μ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞) (fun (q : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 0)
⊢ ∀ᶠ (c : ℝ≥0) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
eventually_atTop.2 ⟨1, A⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- 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 : α
h : Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x = ∞} x
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = ∞} ∩ o
ρs : Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (q : ℝ≥0),
    1 ≤ q → (μ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞) (fun (q : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 0)
⊢ ∀ᶠ (c : ℝ≥0) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact eventually_atTop.2 ⟨1, A⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- 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ρ : ρ ≪ μ
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (v.limRatioMeas hρ ⁻¹' {0}) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_null_of_locally_null _ fun x _ => ?_

Premises used: MeasureTheory.measure_null_of_locally_null
-- 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ρ : ρ ≪ μ
refine :
  ∀ x ∈ v.limRatioMeas hρ ⁻¹' {0},
    ∃ u ∈ 𝓝[v.limRatioMeas hρ ⁻¹' {0}] x, Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (v.limRatioMeas hρ ⁻¹' {0}) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine measure_null_of_locally_null _ fun x _ => ?_

Premises used: MeasureTheory.measure_null_of_locally_null
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
⊢ ∃ (o : Set α),
    x ∈ o ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
Measure.exists_isOpen_measure_lt_top μ x

Premises used: MeasureTheory.Measure.exists_isOpen_measure_lt_top
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
obtain :
  ∀ (o : Set α) (xo : x ∈ o) (o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o)
    (μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ∃ u ∈ 𝓝[v.limRatioMeas hρ ⁻¹' {0}] x, Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ u ∈ 𝓝[v.limRatioMeas hρ ⁻¹' {0}] x, Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
obtain ⟨o, xo, o_open, μo⟩ : ∃ o : Set α, x ∈ o ∧ IsOpen o ∧ μ o < ∞ :=
    Measure.exists_isOpen_measure_lt_top μ x

Premises used: MeasureTheory.Measure.exists_isOpen_measure_lt_top, Set
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
⊢ ∃ u ∈ 𝓝[v.limRatioMeas hρ ⁻¹' {0}] x, Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨s, inter_mem_nhdsWithin _ (o_open.mem_nhds xo), le_antisymm ?_ bot_le⟩

Premises used: inter_mem_nhdsWithin, le_antisymm, And.intro, IsOpen.mem_nhds, Exists.intro, bot_le
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
refine : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ u ∈ 𝓝[v.limRatioMeas hρ ⁻¹' {0}] x, Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine ⟨s, inter_mem_nhdsWithin _ (o_open.mem_nhds xo), le_antisymm ?_ bot_le⟩
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have μs : μ s ≠ ∞ := measure_ne_top_of_subset inter_subset_right μo.ne
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
q : ℝ≥0
hq : 0 < q
apply : s ⊆ {x : α | v.limRatioMeas hρ x < (↑q : ℝ≥0∞)}
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply v.measure_le_mul_of_subset_limRatioMeas_lt hρ

Premises used: VitaliFamily.measure_le_mul_of_subset_limRatioMeas_lt
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
q : ℝ≥0
hq : 0 < q
y : α
hy : y ∈ s
⊢ v.limRatioMeas hρ y = 0

Tactic:
have : v.limRatioMeas hρ y = 0 := hy.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ρ : ρ ≪ μ
x : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
q : ℝ≥0
hq : 0 < q
y : α
hy : y ∈ s
this : v.limRatioMeas hρ y = 0
⊢ Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x < (↑q : ℝ≥0∞)} y

Tactic:
simp only [this, mem_setOf_eq, hq, ENNReal.coe_pos]

Premises used: Set.mem_setOf_eq, ENNReal.coe_pos
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ (q : ℝ≥0),
    0 < q → (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
have A : ∀ q : ℝ≥0, 0 < q → ρ s ≤ q * μ s := by
    intro q hq
    apply v.measure_le_mul_of_subset_limRatioMeas_lt hρ
    intro y hy
    have : v.limRatioMeas hρ y = 0 := hy.1
    simp only [this, mem_setOf_eq, hq, ENNReal.coe_pos]
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (q : ℝ≥0),
    0 < q → (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
apply : Tendsto ENNReal.ofNNReal (𝓝[>] 0) (𝓝 (↑0 : ℝ≥0∞))
⊢ Tendsto (fun (q : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 (HMul.hMul (β := ℝ≥0∞) (↑0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
apply ENNReal.Tendsto.mul_const _ (Or.inr μs)

Premises used: ENNReal.Tendsto.mul_const, 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ρ : ρ ≪ μ
x : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (q : ℝ≥0),
    0 < q → (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw : Tendsto (β := ℝ≥0) (fun (a : ℝ≥0) ↦ a) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto ENNReal.ofNNReal (𝓝[>] 0) (𝓝 (↑0 : ℝ≥0∞))

Tactic:
rw [ENNReal.tendsto_coe]

Premises used: ENNReal.tendsto_coe
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (q : ℝ≥0),
    0 < q → (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0) (fun (a : ℝ≥0) ↦ a) (𝓝[>] 0) (𝓝 0)

Tactic:
nhdsWithin_le_nhds

Premises used: Set.Mem, setOf, nhdsWithin_le_nhds, Set.preimage, Filter.Tendsto
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (q : ℝ≥0),
    0 < q → (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0) (fun (a : ℝ≥0) ↦ a) (𝓝[>] 0) (𝓝 0)

Tactic:
exact nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (q : ℝ≥0),
    0 < q → (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Tendsto (fun (q : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 (HMul.hMul (β := ℝ≥0∞) (↑0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
have B : Tendsto (fun q : ℝ≥0 => (q : ℝ≥0∞) * μ s) (𝓝[>] (0 : ℝ≥0)) (𝓝 ((0 : ℝ≥0) * μ s)) := by
    apply ENNReal.Tendsto.mul_const _ (Or.inr μs)
    rw [ENNReal.tendsto_coe]
    exact nhdsWithin_le_nhds
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (q : ℝ≥0),
    0 < q → (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
B :
  Tendsto (fun (q : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 (HMul.hMul (β := ℝ≥0∞) (↑0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
⊢ Tendsto (β := ℝ≥0∞) (fun (q : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 0)

Tactic:
simp only [zero_mul, ENNReal.coe_zero] at B

Premises used: MulZeroClass.zero_mul, ENNReal.coe_zero
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (q : ℝ≥0),
    0 < q → (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞) (fun (q : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 0)
apply :
  ∀ᶠ (c : ℝ≥0) in 𝓝[>] 0,
    (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply ge_of_tendsto B

Premises used: ge_of_tendsto
-- 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 : α
h : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (q : ℝ≥0),
    0 < q → (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞) (fun (q : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 0)
⊢ ∀ (a : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) (Ioi 0) a →
      (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
A

Premises used: Set.Ioi, Set.Mem, setOf
-- 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 : α
h_1 : x ∈ v.limRatioMeas hρ ⁻¹' {0}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = 0} ∩ o
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (q : ℝ≥0),
    0 < q → (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞) (fun (q : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 0)
h :
  ∀ (a : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0)
      {x : ℝ≥0 |
        Membership.mem (γ := Set ℝ≥0) (Ioi 0) x →
          Membership.mem (γ := Set ℝ≥0)
            {x : ℝ≥0 |
              (fun (c : ℝ≥0) ↦
                  (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
                x}
            x}
      a
h₁ :
  ∀ (a : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) (Ioi 0) a →
      (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[>] 0,
    (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
filter_upwards [self_mem_nhdsWithin] using A

Premises used: self_mem_nhdsWithin
-- 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
t : ℝ≥0
ht : 1 < t
⊢ t ≠ 0

Tactic:
have t_ne_zero' : t ≠ 0 := (zero_lt_one.trans ht).ne'
-- 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
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
⊢ (↑t : ℝ≥0∞) ≠ 0

Tactic:
simpa only [ENNReal.coe_eq_zero, Ne] using t_ne_zero'

Premises used: Ne, ENNReal.coe_eq_zero
-- 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
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
⊢ (↑t : ℝ≥0∞) ≠ 0

Tactic:
have t_ne_zero : (t : ℝ≥0∞) ≠ 0 := by simpa only [ENNReal.coe_eq_zero, Ne] using t_ne_zero'
-- 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
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
⊢ Measurable f

Tactic:
have f_meas : Measurable f := 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
apply : LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)

Tactic:
apply zero_le.trans'

Premises used: zero_le, LE.le.trans'