awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r)
I2 : closedBall y ((4 * K + 3) * r) ⊆ closedBall y (max (4 * K + 3) 3 * r)
pos :
  (μ : (a : Set α) → ENNReal) (closedBall y (max (4 * K + 3) 3 * r)) ≤
    HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
      ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (closedBall x (3 * ((K + 1) * r))) ≤
    HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
      ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)

Tactic:
apply (measure_mono (I1.trans I2)).trans

Premises used: HasSubset.Subset.trans, MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r)
I2 : closedBall y ((4 * K + 3) * r) ⊆ closedBall y (max (4 * K + 3) 3 * r)
⊢ (μ : (a : Set α) → ENNReal) (closedBall y (max (4 * K + 3) 3 * r)) ≤
    HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
      ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)

Tactic:
measure_mul_le_scalingConstantOf_mul _
        ⟨zero_lt_three.trans_le (le_max_right _ _), le_rfl⟩ hr

Premises used: le_max_right, le_rfl, zero_lt_three, IsUnifLocDoublingMeasure.measure_mul_le_scalingConstantOf_mul, LT.lt.trans_le, And.intro
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r)
I2 : closedBall y ((4 * K + 3) * r) ⊆ closedBall y (max (4 * K + 3) 3 * r)
⊢ (μ : (a : Set α) → ENNReal) (closedBall y (max (4 * K + 3) 3 * r)) ≤
    HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
      ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)

Tactic:
exact measure_mul_le_scalingConstantOf_mul _
        ⟨zero_lt_three.trans_le (le_max_right _ _), le_rfl⟩ hr

Premises used: le_max_right, le_rfl, zero_lt_three, IsUnifLocDoublingMeasure.measure_mul_le_scalingConstantOf_mul, LT.lt.trans_le, And.intro
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
⊢ ∃ (r_1 : ℝ),
    closedBall y r ⊆ closedBall x r_1 ∧
      (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
        HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
          ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)

Tactic:
⟨_, H, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
pos :
  (μ : (a : Set α) → ENNReal) (closedBall x (3 * (R / 4))) ≤
    HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
      ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)
⊢ ∃ (r_1 : ℝ),
    closedBall y r ⊆ closedBall x r_1 ∧
      (μ : (a : Set α) → ENNReal) (closedBall x (3 * r_1)) ≤
        HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
          ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)

Tactic:
refine ⟨_, H, ?_⟩
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
pos : 3 * (R / 4) + dist x y ≤ r
⊢ (μ : (a : Set α) → ENNReal) (closedBall x (3 * (R / 4))) ≤
    HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
      ((μ : (a : Set α) → ENNReal) (closedBall y r) : ENNReal)

Tactic:
grw [scalingConstantOf, ← le_max_right, ENNReal.coe_one, one_mul,
      closedBall_subset_closedBall' (y := y)]

Premises used: le_max_right, IsUnifLocDoublingMeasure.scalingConstantOf, ENNReal.coe_one, Metric.closedBall_subset_closedBall', one_mul
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
⊢ y ∈ closedBall y r

Tactic:
have A : y ∈ closedBall y r := mem_closedBall_self rpos.le
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
A : y ∈ closedBall y r
⊢ dist x y ≤ R / 4

Tactic:
have B := mem_closedBall'.1 (H A)
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
A : y ∈ closedBall y r
B : dist x y ≤ R / 4
linarith : r < 3 * (R / 4) + dist x y → 4 / 4 = 1
linarith₁ linarith₂ : r < 3 * (R / 4) + dist x y → HMul.hMul (α := ℝ) 1 4 = 4
linarith₃ : r < 3 * (R / 4) + dist x y → GT.gt (α := ℝ) 4 0
linarith₄ : r < 3 * (R / 4) + dist x y → 4 / 4 = 1
linarith₅ : r < 3 * (R / 4) + dist x y → HMul.hMul (α := ℝ) 1 4 = 4
linarith₆ : r < 3 * (R / 4) + dist x y → GT.gt (α := ℝ) 4 0
linarith₇ :
  r < 3 * (R / 4) + dist x y →
    4 * (R - r) + (4 * dist x y - 1 * R) + (4 * r - (HMul.hMul (α := ℝ) 1 3 * (1 * R) + 4 * dist x y)) = 0
linarith₈ : r < 3 * (R / 4) + dist x y → GT.gt (α := ℝ) 4 0
⊢ 3 * (R / 4) + dist x y ≤ r

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
⊢ Tendsto (fun (j : ι) ↦ closedBall (w j) (δ j)) l (VitaliFamily.filterAt (vitaliFamily μ K) x)

Tactic:
(vitaliFamily μ K).tendsto_filterAt_iff.mpr ⟨?_, fun ε hε => ?_⟩

Premises used: Iff.mpr, IsUnifLocDoublingMeasure.vitaliFamily, VitaliFamily.tendsto_filterAt_iff, And.intro
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
refine_1 : ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
refine_2 : ∀ (ε : ℝ) (hε : ε > 0), ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
⊢ Tendsto (fun (j : ι) ↦ closedBall (w j) (δ j)) l (VitaliFamily.filterAt (vitaliFamily μ K) x)

Tactic:
refine (vitaliFamily μ K).tendsto_filterAt_iff.mpr ⟨?_, fun ε hε => ?_⟩

Premises used: Iff.mpr, IsUnifLocDoublingMeasure.vitaliFamily, VitaliFamily.tendsto_filterAt_iff, And.intro
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
h :
  ∀ (j : ι) (hj : x ∈ closedBall (w j) (K * δ j)) (h'j : j ∈ δ ⁻¹' Ioi 0),
    closedBall (w j) (δ j) ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ∈ VitaliFamily.setsAt (vitaliFamily μ K) x

Tactic:
filter_upwards [xmem, δlim self_mem_nhdsWithin] with j hj h'j

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : j ∈ δ ⁻¹' Ioi 0
⊢ closedBall (w j) (δ j) ∈ VitaliFamily.setsAt (vitaliFamily μ K) x

Tactic:
closedBall_mem_vitaliFamily_of_dist_le_mul μ hj h'j

Premises used: IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : j ∈ δ ⁻¹' Ioi 0
⊢ closedBall (w j) (δ j) ∈ VitaliFamily.setsAt (vitaliFamily μ K) x

Tactic:
exact closedBall_mem_vitaliFamily_of_dist_le_mul μ hj h'j

Premises used: IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
refine_2 :
  ∀ (δlim : Tendsto δ ⊥ (𝓝[>] 0)) (xmem : ∀ᶠ (j : ι) in ⊥, x ∈ closedBall (w j) (K * δ j)),
    ∀ᶠ (i : ι) in ⊥, closedBall (w i) (δ i) ⊆ closedBall x ε
refine_2₁ : ∀ (h : l.NeBot), ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε

Tactic:
rcases l.eq_or_neBot with rfl | h

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
w : ι → α
δ : ι → ℝ
ε : ℝ
hε : ε > 0
δlim : Tendsto δ ⊥ (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in ⊥, x ∈ closedBall (w j) (K * δ j)
⊢ ∀ᶠ (i : ι) in ⊥, closedBall (w i) (δ i) ⊆ closedBall x ε

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
rcases : ∀ (j : ι) (hj : x ∈ closedBall (w j) (K * δ j)) (h'j : Membership.mem (γ := Set ℝ) (Ioi 0) (δ j)), 0 ≤ K
⊢ 0 ≤ K

Tactic:
rcases (xmem.and (δlim self_mem_nhdsWithin)).exists with ⟨j, hj, h'j⟩

Premises used: Filter.Eventually.and, Filter.Eventually.exists, self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : Membership.mem (γ := Set ℝ) (Ioi 0) (δ j)
⊢ 0 ≤ K * δ j

Tactic:
have : 0 ≤ K * δ j := nonempty_closedBall.1 ⟨x, hj⟩
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : Membership.mem (γ := Set ℝ) (Ioi 0) (δ j)
this : 0 ≤ K * δ j
⊢ 0 ≤ K

Tactic:
(mul_nonneg_iff_left_nonneg_of_pos (mem_Ioi.1 h'j)).1 this

Premises used: Set.mem_Ioi, mul_nonneg_iff_left_nonneg_of_pos, Iff.mp
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : Membership.mem (γ := Set ℝ) (Ioi 0) (δ j)
this : 0 ≤ K * δ j
⊢ 0 ≤ K

Tactic:
exact (mul_nonneg_iff_left_nonneg_of_pos (mem_Ioi.1 h'j)).1 this

Premises used: Set.mem_Ioi, mul_nonneg_iff_left_nonneg_of_pos, Iff.mp
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
⊢ 0 ≤ K

Tactic:
have hK : 0 ≤ K := by
      rcases (xmem.and (δlim self_mem_nhdsWithin)).exists with ⟨j, hj, h'j⟩
      have : 0 ≤ K * δ j := nonempty_closedBall.1 ⟨x, hj⟩
      exact (mul_nonneg_iff_left_nonneg_of_pos (mem_Ioi.1 h'j)).1 this
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
hK : 0 ≤ K
⊢ ∀ᶠ (i : ι) in l, Membership.mem (γ := Set ℝ) (Ioi 0) (δ i)

Tactic:
have δpos := eventually_mem_of_tendsto_nhdsWithin δlim
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
hK : 0 ≤ K
δpos : ∀ᶠ (i : ι) in l, Membership.mem (γ := Set ℝ) (Ioi 0) (δ i)
⊢ Tendsto δ l (𝓝 0)

Tactic:
replace δlim := tendsto_nhds_of_tendsto_nhdsWithin δlim
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
hK : 0 ≤ K
δpos : ∀ᶠ (i : ι) in l, Membership.mem (γ := Set ℝ) (Ioi 0) (δ i)
δlim : Tendsto δ l (𝓝 0)
linarith : K + 1 ≤ 0 → -1 + (0 - K) + (K + 1 - 0) = 0
⊢ 0 < K + 1

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
hK : 0 ≤ K
δpos : ∀ᶠ (i : ι) in l, Membership.mem (γ := Set ℝ) (Ioi 0) (δ i)
δlim : Tendsto δ l (𝓝 0)
⊢ 0 < K + 1

Tactic:
replace hK : 0 < K + 1 := by linarith
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
δpos : ∀ᶠ (i : ι) in l, Membership.mem (γ := Set ℝ) (Ioi 0) (δ i)
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
refine_2 :
  ∀ (x_1 : ι),
    (dist (δ x_1) 0 < ε / (K + 1) ∧ Membership.mem (γ := Set ℝ) (Ioi 0) (δ x_1)) ∧ x ∈ closedBall (w x_1) (K * δ x_1) →
      closedBall (w x_1) (δ x_1) ⊆ closedBall x ε
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε

Tactic:
apply (((Metric.tendsto_nhds.mp δlim _ (div_pos hε hK)).and δpos).and xmem).mono

Premises used: Metric.tendsto_nhds, Filter.Eventually.and, Filter.Eventually.mono, Iff.mp, div_pos
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
δpos : ∀ᶠ (i : ι) in l, Membership.mem (γ := Set ℝ) (Ioi 0) (δ i)
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hx : x ∈ closedBall (w j) (K * δ j)
hjε : dist (δ j) 0 < ε / (K + 1)
hj₀ : 0 < δ j
y : α
hy : y ∈ closedBall (w j) (δ j)
⊢ (K + 1) * δ j < ε

Tactic:
simpa [abs_eq_self.mpr hj₀.le] using (lt_div_iff₀' hK).mp hjε

Premises used: Iff.mpr, lt_div_iff₀', LT.lt.le, Iff.mp, abs_eq_self
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
δpos : ∀ᶠ (i : ι) in l, Membership.mem (γ := Set ℝ) (Ioi 0) (δ i)
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hx : x ∈ closedBall (w j) (K * δ j)
hjε : dist (δ j) 0 < ε / (K + 1)
hj₀ : 0 < δ j
y : α
hy : y ∈ closedBall (w j) (δ j)
⊢ (K + 1) * δ j < ε

Tactic:
replace hjε : (K + 1) * δ j < ε := by
      simpa [abs_eq_self.mpr hj₀.le] using (lt_div_iff₀' hK).mp hjε
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
δpos : ∀ᶠ (i : ι) in l, Membership.mem (γ := Set ℝ) (Ioi 0) (δ i)
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hx : x ∈ closedBall (w j) (K * δ j)
hj₀ : 0 < δ j
y : α
hy : y ∈ closedBall (w j) (δ j)
hjε : (K + 1) * δ j < ε
⊢ dist x (w j) ≤ K * δ j

Tactic:
simp only [mem_closedBall] at hx hy ⊢

Premises used: Metric.mem_closedBall
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
δpos : ∀ᶠ (i : ι) in l, Membership.mem (γ := Set ℝ) (Ioi 0) (δ i)
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hx : x ∈ closedBall (w j) (K * δ j)
hj₀ : 0 < δ j
y : α
hy : y ∈ closedBall (w j) (δ j)
hjε : (K + 1) * δ j < ε
hx₁ : dist x (w j) ≤ K * δ j
⊢ dist y (w j) ≤ δ j

Tactic:
simp only [mem_closedBall] at hx hy ⊢

Premises used: Metric.mem_closedBall
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
δpos : ∀ᶠ (i : ι) in l, Membership.mem (γ := Set ℝ) (Ioi 0) (δ i)
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hj₀ : 0 < δ j
y : α
hjε : (K + 1) * δ j < ε
hx : dist x (w j) ≤ K * δ j
hy : dist y (w j) ≤ δ j
linarith :
  ε < dist y x →
    (K + 1) * δ j - ε + (dist x (w j) - K * δ j) + (dist y (w j) - δ j) + (ε - dist y x) +
        (dist y x - (dist y (w j) + dist x (w j))) =
      0
⊢ dist y x ≤ ε

Tactic:
linarith [dist_triangle_right y x (w j)]

Premises used: dist_triangle_right