awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
⊢ 3 * (R / 4) + dist x y ≤ r
have linarith₁ : r < 3 * (R / 4) + dist x y → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
⊢ 3 * (R / 4) + dist x y ≤ r
have linarith₃ : r < 3 * (R / 4) + dist x y → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
⊢ 3 * (R / 4) + dist x y ≤ r
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
have refine_1 : ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
Tactic: refine (vitaliFamily μ K).tendsto_filterAt_iff.mpr ⟨?_, fun ε hε => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
⊢ Tendsto (fun (j : ι) ↦ closedBall (w j) (δ j)) l (VitaliFamily.filterAt (vitaliFamily μ K) x)
have refine_2 : ∀ (ε : ℝ) (hε : ε > 0), ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
Tactic: refine (vitaliFamily μ K).tendsto_filterAt_iff.mpr ⟨?_, fun ε hε => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
have h : ∀ (j : ι) (hj : x ∈ closedBall (w j) (K * δ j)) (h'j : j ∈ δ ⁻¹' Ioi 0),
  closedBall (w j) (δ j) ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
Tactic: filter_upwards [xmem, δlim self_mem_nhdsWithin] with j hj h'j
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
have refine_2 : ∀ (δlim : Tendsto δ ⊥ (𝓝[>] 0)) (xmem : ∀ᶠ (j : ι) in ⊥, x ∈ closedBall (w j) (K * δ j)),
  ∀ᶠ (i : ι) in ⊥, closedBall (w i) (δ i) ⊆ closedBall x ε
Tactic: rcases l.eq_or_neBot with rfl | h
Cleared hypotheses: l, δlim, xmem
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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 ε
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
have refine_2₁ : ∀ (h : l.NeBot), ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
Tactic: rcases l.eq_or_neBot with rfl | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
have rcases : ∀ (j : ι) (hj : x ∈ closedBall (w j) (K * δ j)) (h'j : Membership.mem (γ := Set ℝ) (Ioi 0) (δ j)), 0 ≤ K
Tactic: rcases (xmem.and (δlim self_mem_nhdsWithin)).exists with ⟨j, hj, h'j⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (hypothesis)
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
have this : 0 ≤ K * δ j
Tactic: have : 0 ≤ K * δ j := nonempty_closedBall.1 ⟨x, hj⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (hypothesis)
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
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
have hK : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (hypothesis)
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, closedBall (w i) (δ i) ⊆ closedBall x ε
have δpos : ∀ᶠ (i : ι) in l, Membership.mem (γ := Set ℝ) (Ioi 0) (δ i)
Tactic: have δpos := eventually_mem_of_tendsto_nhdsWithin δlim
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (hypothesis)
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)
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
have δlim₁ : Tendsto δ l (𝓝 0)
Tactic: replace δlim := tendsto_nhds_of_tendsto_nhdsWithin δlim
Cleared hypotheses: δlim
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
have linarith : K + 1 ≤ 0 → -1 + (0 - K) + (K + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (hypothesis)
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)
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
have hK₁ : 0 < K + 1
Tactic: replace hK : 0 < K + 1 := by linarith
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
have 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 ε
Tactic: apply (((Metric.tendsto_nhds.mp δlim _ (div_pos hε hK)).and δpos).and xmem).mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (hypothesis)
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)
⊢ y ∈ closedBall x ε
have hjε₁ : (K + 1) * δ j < ε
Tactic: replace hjε : (K + 1) * δ j < ε := by
      simpa [abs_eq_self.mpr hj₀.le] using (lt_div_iff₀' hK).mp hjε
Cleared hypotheses: hjε
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (hypothesis)
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 < ε
⊢ y ∈ closedBall x ε
have hx₁ : dist x (w j) ≤ K * δ j
Tactic: simp only [mem_closedBall] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (hypothesis)
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
⊢ y ∈ closedBall x ε
have hy₁ : dist y (w j) ≤ δ j
Tactic: simp only [mem_closedBall] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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
⊢ dist y x ≤ ε
have 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
Tactic: linarith [dist_triangle_right y x (w j)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
S : Set α
K : ℝ
⊢ ∀ᵐ (x : α) ∂μ.restrict S,
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[>] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (β := ENNReal)
            (fun (j : ι) ↦
              HDiv.hDiv (α := ENNReal) (β := ENNReal)
                ((μ : (a : Set α) → ENNReal) (S ∩ closedBall (w j) (δ j)) : ENNReal)
                ((μ : (a : Set α) → ENNReal) (closedBall (w j) (δ j)) : ENNReal))
            l (𝓝 1)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α |
            (fun (x : α) ↦
                Tendsto (β := ENNReal)
                  (fun (a : Set α) ↦
                    HDiv.hDiv (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) (S ∩ a) : ENNReal)
                      ((μ : (a : Set α) → ENNReal) a : ENNReal))
                  (VitaliFamily.filterAt (vitaliFamily μ K) x) (𝓝 1))
              x}
          x →
        Membership.mem (γ := Set α)
          {x : α |
            (fun (x : α) ↦
                ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
                  Tendsto δ l (𝓝[>] 0) →
                    (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
                      Tendsto (β := ENNReal)
                        (fun (j : ι) ↦
                          HDiv.hDiv (α := ENNReal) (β := ENNReal)
                            ((μ : (a : Set α) → ENNReal) (S ∩ closedBall (w j) (δ j)) : ENNReal)
                            ((μ : (a : Set α) → ENNReal) (closedBall (w j) (δ j)) : ENNReal))
                        l (𝓝 1))
              x}
          x}
    a
Tactic: filter_upwards [(vitaliFamily μ K).ae_tendsto_measure_inter_div S] with x hx ι l w δ δlim
    xmem using hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
S : Set α
K : ℝ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  Tendsto (β := ENNReal)
                    (fun (a : Set α) ↦
                      HDiv.hDiv (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) (S ∩ a) : ENNReal)
                        ((μ : (a : Set α) → ENNReal) a : ENNReal))
                    (VitaliFamily.filterAt (vitaliFamily μ K) x) (𝓝 1))
                x}
            x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
                    Tendsto δ l (𝓝[>] 0) →
                      (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
                        Tendsto (β := ENNReal)
                          (fun (j : ι) ↦
                            HDiv.hDiv (α := ENNReal) (β := ENNReal)
                              ((μ : (a : Set α) → ENNReal) (S ∩ closedBall (w j) (δ j)) : ENNReal)
                              ((μ : (a : Set α) → ENNReal) (closedBall (w j) (δ j)) : ENNReal))
                          l (𝓝 1))
                x}
            x}
      a
⊢ ∀ᵐ (x : α) ∂μ.restrict S,
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[>] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (β := ENNReal)
            (fun (j : ι) ↦
              HDiv.hDiv (α := ENNReal) (β := ENNReal)
                ((μ : (a : Set α) → ENNReal) (S ∩ closedBall (w j) (δ j)) : ENNReal)
                ((μ : (a : Set α) → ENNReal) (closedBall (w j) (δ j)) : ENNReal))
            l (𝓝 1)
have h₁ : ∀ (a : α),
  Tendsto (β := ENNReal)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) (S ∩ a) : ENNReal)
          ((μ : (a : Set α) → ENNReal) a : ENNReal))
      (VitaliFamily.filterAt (vitaliFamily μ K) a) (𝓝 1) →
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[>] 0) →
        (∀ᶠ (j : ι) in l, a ∈ closedBall (w j) (K * δ j)) →
          Tendsto (β := ENNReal)
            (fun (j : ι) ↦
              HDiv.hDiv (α := ENNReal) (β := ENNReal)
                ((μ : (a : Set α) → ENNReal) (S ∩ closedBall (w j) (δ j)) : ENNReal)
                ((μ : (a : Set α) → ENNReal) (closedBall (w j) (δ j)) : ENNReal))
            l (𝓝 1)
Tactic: filter_upwards [(vitaliFamily μ K).ae_tendsto_measure_inter_div S] with x hx ι l w δ δlim
    xmem using hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
E : Type u_2
inst_6 : NormedAddCommGroup E
f : α → E
hf : LocallyIntegrable f μ
K : ℝ
⊢ ∀ᵐ (x : α) ∂μ,
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[>] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (β := ℝ) (fun (j : ι) ↦ ⨍ (y : α) in closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (𝓝 0)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α |
            (fun (x : α) ↦
                Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ)
                  (VitaliFamily.filterAt (vitaliFamily μ K) x) (𝓝 0))
              x}
          x →
        Membership.mem (γ := Set α)
          {x : α |
            (fun (x : α) ↦
                ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
                  Tendsto δ l (𝓝[>] 0) →
                    (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
                      Tendsto (β := ℝ) (fun (j : ι) ↦ ⨍ (y : α) in closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (𝓝 0))
              x}
          x}
    a
Tactic: filter_upwards [(vitaliFamily μ K).ae_tendsto_average_norm_sub hf] with x hx ι l w δ δlim
    xmem using hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
E : Type u_2
inst_6 : NormedAddCommGroup E
f : α → E
hf : LocallyIntegrable f μ
K : ℝ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  Tendsto (β := ℝ) (fun (a : Set α) ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ)
                    (VitaliFamily.filterAt (vitaliFamily μ K) x) (𝓝 0))
                x}
            x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
                    Tendsto δ l (𝓝[>] 0) →
                      (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
                        Tendsto (β := ℝ) (fun (j : ι) ↦ ⨍ (y : α) in closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (𝓝 0))
                x}
            x}
      a
⊢ ∀ᵐ (x : α) ∂μ,
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[>] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (β := ℝ) (fun (j : ι) ↦ ⨍ (y : α) in closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (𝓝 0)
have h₁ : ∀ (a : α),
  Tendsto (β := ℝ) (fun (a_1 : Set α) ↦ ⨍ (y : α) in a_1, ‖f y - f a‖ ∂μ) (VitaliFamily.filterAt (vitaliFamily μ K) a)
      (𝓝 0) →
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[>] 0) →
        (∀ᶠ (j : ι) in l, a ∈ closedBall (w j) (K * δ j)) →
          Tendsto (β := ℝ) (fun (j : ι) ↦ ⨍ (y : α) in closedBall (w j) (δ j), ‖f y - f a‖ ∂μ) l (𝓝 0)
Tactic: filter_upwards [(vitaliFamily μ K).ae_tendsto_average_norm_sub hf] with x hx ι l w δ δlim
    xmem using hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)