awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
⊢ ∃ u_1 ∈ 𝓝[s \ ⋃ a ∈ u, B a] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u_1 : ℝ≥0∞) (0 : ℝ≥0∞)
have refine : ∀ (ε : ℝ≥0∞) (εpos : 0 < ε), (μ : (a : Set α) → ℝ≥0∞) ((s \ ⋃ a ∈ u, B a) ∩ ball x (R x)) ≤ ε
Tactic: refine ⟨_ ∩ ball x (R x), inter_mem_nhdsWithin _ (ball_mem_nhds _ (hR0 _)),
    nonpos_iff_eq_zero.mp (le_of_forall_gt_imp_ge_of_dense fun ε εpos => ?_)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
⊢ Eq (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ a ∈ v, B a) : ℝ≥0∞)
have rw : v.PairwiseDisjoint B
Tactic: rw [measure_biUnion (u_count.mono vu) _ fun a ha => (h't _ (vu.trans ut ha)).measurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
⊢ LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
have a : Eq (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι)) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (⋃ a ∈ v, B a) : ℝ≥0∞)
Tactic: calc
      (∑' a : v, μ (B a)) = μ (⋃ a ∈ v, B a) := by
        rw [measure_biUnion (u_count.mono vu) _ fun a ha => (h't _ (vu.trans ut ha)).measurableSet]
        exact u_disj.subset vu
      _ ≤ μ (closedBall x K) := (measure_mono (iUnion₂_subset fun a ha => hK a (vu ha) ha.2))
      _ < ∞ := μK
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
⊢ (μ : (a : Set α) → ℝ≥0∞) ((s \ ⋃ a ∈ u, B a) ∩ ball x (R x)) ≤ ε
have I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
Tactic: have I : (∑' a : v, μ (B a)) < ∞ := by
    calc
      (∑' a : v, μ (B a)) = μ (⋃ a ∈ v, B a) := by
        rw [measure_biUnion (u_count.mono vu) _ fun a ha => (h't _ (vu.trans ut ha)).measurableSet]
        exact u_disj.subset vu
      _ ≤ μ (closedBall x K) := (measure_mono (iUnion₂_subset fun a ha => hK a (vu ha) ha.2))
      _ < ∞ := μK
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
⊢ (μ : (a : Set α) → ℝ≥0∞) ((s \ ⋃ a ∈ u, B a) ∩ ball x (R x)) ≤ ε
have obtain : ∀ (w : Finset (↑v : Type u_2))
  (hw :
    ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
      ε / (↑C : ℝ≥0∞)),
  (μ : (a : Set α) → ℝ≥0∞) ((s \ ⋃ a ∈ u, B a) ∩ ball x (R x)) ≤ ε
Tactic: obtain ⟨w, hw⟩ : ∃ w : Finset v, (∑' a : { a // a ∉ w }, μ (B a)) < ε / C :=
    haveI : 0 < ε / C := by
      simp only [ENNReal.div_pos_iff, εpos.ne', ENNReal.coe_ne_top, Ne, not_false_iff,
        and_self_iff]
    ((tendsto_order.1 (ENNReal.tendsto_tsum_compl_atTop_zero I.ne)).2 _ this).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
z : α
hz : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
k : Set α := ⋃ a ∈ w, B (↑a : ι)
⊢ Membership.mem (γ := Set α)
    (⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι)))
    z
have k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
Tactic: have k_closed : IsClosed k := isClosed_biUnion_finset fun i _ => h't _ (ut (vu i.2))
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
z : α
hz : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
k : Set α := ⋃ a ∈ w, B (↑a : ι)
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
⊢ z ∉ k
have simp : ∀ (x : ι) (x_1 : x ∈ v) (h : Subtype.mk (p := fun (x : ι) ↦ x ∈ v) x sorry ∈ w), z ∉ B x
Tactic: simp only [k, not_exists, exists_prop, mem_iUnion, forall_exists_index,
        SetCoe.exists, not_and, exists_and_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
z : α
hz : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
k : Set α := ⋃ a ∈ w, B (↑a : ι)
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
b : ι
hbv : b ∈ v
h_1 : Subtype.mk (p := fun (x : ι) ↦ x ∈ v) b ⋯ ∈ w
h'z : z ∈ B b
⊢ False
have this : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ⋃ a ∈ u, B a
Tactic: have : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ⋃ a ∈ u, B a :=
        mem_inter (mem_of_mem_inter_left hz) (mem_biUnion (vu hbv) h'z)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
z : α
hz : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
k : Set α := ⋃ a ∈ w, B (↑a : ι)
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
⊢ Membership.mem (γ := Set α)
    (⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι)))
    z
have z_notmem_k : z ∉ k
Tactic: have z_notmem_k : z ∉ k := by
      simp only [k, not_exists, exists_prop, mem_iUnion, forall_exists_index,
        SetCoe.exists, not_and, exists_and_right]
      intro b hbv _ h'z
      have : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ⋃ a ∈ u, B a :=
        mem_inter (mem_of_mem_inter_left hz) (mem_biUnion (vu hbv) h'z)
      simpa only [diff_inter_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
z : α
hz : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
k : Set α := ⋃ a ∈ w, B (↑a : ι)
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
z_notmem_k : z ∉ k
⊢ ball x (R x) \ k ∈ 𝓝 z
have apply : z ∈ ball x (R x) \ k
Tactic: apply IsOpen.mem_nhds (isOpen_ball.sdiff k_closed) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
z : α
hz : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
k : Set α := ⋃ a ∈ w, B (↑a : ι)
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
z_notmem_k : z ∉ k
⊢ Membership.mem (γ := Set α)
    (⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι)))
    z
have this : ball x (R x) \ k ∈ 𝓝 z
Tactic: have : ball x (R x) \ k ∈ 𝓝 z := by
      apply IsOpen.mem_nhds (isOpen_ball.sdiff k_closed) _
      exact (mem_diff _).2 ⟨mem_of_mem_inter_right hz, z_notmem_k⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
z : α
hz : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
k : Set α := ⋃ a ∈ w, B (↑a : ι)
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
z_notmem_k : z ∉ k
this : ball x (R x) \ k ∈ 𝓝 z
⊢ Membership.mem (γ := Set α)
    (⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι)))
    z
have obtain : ∀ (d : ℝ) (dpos : 0 < d) (hd : closedBall z d ⊆ ball x (R x) \ k),
  Membership.mem (γ := Set α)
    (⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι)))
    z
Tactic: obtain ⟨d, dpos, hd⟩ : ∃ d, 0 < d ∧ closedBall z d ⊆ ball x (R x) \ k :=
      nhds_basis_closedBall.mem_iff.1 this