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
ε : ℝ≥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∞)
k : Set α := ⋃ a ∈ w, B (↑a : ι)
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
d : ℝ
dpos : 0 < d
a : ι
hat : a ∈ t
hz : c a ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
z_notmem_k : c a ∉ k
this : ball x (R x) \ k ∈ 𝓝 (c a)
hd : closedBall (c a) d ⊆ ball x (R x) \ k
ad : r a ≤ min d (R (c a))
ax : B a ⊆ ball x (R x)
b : ι
bu : b ∈ u
ab : (B a ∩ B b).Nonempty
bdiam : r a ≤ 2 * r b
bv : b ∈ v
b' : (↑v : Type u_2) := Subtype.mk (p := fun (x : ι) ↦ x ∈ v) b bv
b'_notmem_w : b' ∉ w
b'' : { a : (↑v : Type u_2) // a ∉ w } := Subtype.mk (p := fun (a : (↑v : Type u_2)) ↦ a ∉ w) b' b'_notmem_w
zb : c a ∈ closedBall (c b) (3 * r b)
⊢ 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)) : ι)))
    (c a)
have suffices : closedBall (c (↑(↑b'' : (↑v : Type u_2)) : ι)) (3 * r (↑(↑b'' : (↑v : Type u_2)) : ι)) ⊆
  ⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
    closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))
Tactic: suffices H : closedBall (c b'') (3 * r b'')
        ⊆ ⋃ a : { a // a ∉ w }, closedBall (c a) (3 * r a) from H zb
-- 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∞)
M :
  (s \ ⋃ a ∈ u, B a) ∩ ball x (R x) ⊆
    ⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))
⊢ (μ : (a : Set α) → ℝ≥0∞) ((s \ ⋃ a ∈ u, B a) ∩ ball x (R x)) ≤ ε
have this : Countable.{u_2 + 1} (↑v : Type u_2)
Tactic: haveI : Countable v := (u_count.mono vu).to_subtype
-- 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∞)
M :
  (s \ ⋃ a ∈ u, B a) ∩ ball x (R x) ⊆
    ⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))
this : Countable.{u_2 + 1} (↑v : Type u_2)
⊢ (μ : (a : Set α) → ℝ≥0∞) ((s \ ⋃ a ∈ u, B a) ∩ ball x (R x)) ≤ ε
have μ₁ : (↑C : ℝ≥0∞) * ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) ≤
  (↑C : ℝ≥0∞) * (ε / (↑C : ℝ≥0∞))
Tactic: calc
    μ ((s \ ⋃ a ∈ u, B a) ∩ ball x (R x)) ≤ μ (⋃ a : { a // a ∉ w }, closedBall (c a) (3 * r a)) :=
      measure_mono M
    _ ≤ ∑' a : { a // a ∉ w }, μ (closedBall (c a) (3 * r a)) := measure_iUnion_le _
    _ ≤ ∑' a : { a // a ∉ w }, C * μ (B a) := (ENNReal.tsum_le_tsum fun a => μB a (ut (vu a.1.2)))
    _ = C * ∑' a : { a // a ∉ w }, μ (B a) := ENNReal.tsum_mul_left
    _ ≤ C * (ε / C) := by gcongr
    _ ≤ ε := ENNReal.mul_div_le
-- 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, ∃ᶠ (ε : ℝ) in 𝓝[>] 0, ∃ a ∈ t, r a = ε ∧ c a = x
⊢ ∃ u ⊆ t,
    u.Countable ∧ u.PairwiseDisjoint B ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ a ∈ u, B a) : ℝ≥0∞) (0 : ℝ≥0∞)
have suffices : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
Tactic: suffices ∀ x ∈ s, ∀ ε > (0 : ℝ), ∃ a ∈ t, r a ≤ ε ∧ c a = x from
    exists_disjoint_covering_ae μ s t C r c B hB μB ht h't this
-- 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, ∃ᶠ (ε : ℝ) in 𝓝[>] 0, ∃ a ∈ t, r a = ε ∧ c a = x
x : α
hx : x ∈ s
ε : ℝ
hε : ε > 0
⊢ ∃ a ∈ t, r a ≤ ε ∧ c a = x
have hf₁ : ∃ᶠ (ε : ℝ) in 𝓝[>] 0, ∃ a ∈ t, r a = ε ∧ c a = x
Tactic: specialize hf x hx
Cleared hypotheses: hf
-- 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)
x : α
hx : x ∈ s
ε : ℝ
hε : ε > 0
hf : ∃ᶠ (ε : ℝ) in 𝓝[>] 0, ∃ a ∈ t, r a = ε ∧ c a = x
⊢ ∃ a ∈ t, r a ≤ ε ∧ c a = x
have hf₁ : ∀ (U : Set ℝ), 0 ∈ U → IsOpen U → ∃ y ∈ U, (∃ a ∈ t, r a = y ∧ c a = x) ∧ Membership.mem (γ := Set ℝ) (Ioi 0) y
Tactic: rw [frequently_nhdsWithin_iff, frequently_nhds_iff] at hf
Cleared hypotheses: hf
-- 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)
x : α
hx : x ∈ s
ε : ℝ
hε : ε > 0
hf : ∀ (U : Set ℝ), 0 ∈ U → IsOpen U → ∃ y ∈ U, (∃ a ∈ t, r a = y ∧ c a = x) ∧ Membership.mem (γ := Set ℝ) (Ioi 0) y
⊢ ∃ a ∈ t, r a ≤ ε ∧ c a = x
have obtain : ∀ w ∈ Ioo (-ε) ε,
  Membership.mem (γ := Set ℝ) (Ioi 0) w →
    ∀ (a : ι) (ha₁ : a ∈ t) (ha₂ : r a = w) (ha₃ : c a = x), ∃ a ∈ t, r a ≤ ε ∧ c a = x
Tactic: obtain ⟨_, _, ⟨a, ha₁, ha₂, ha₃⟩, _⟩ := hf (Ioo (-ε) ε) (by grind) isOpen_Ioo
-- 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 μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
x : α
ε : ℝ
εpos : ε > 0
⊢ ∃ (s : Set α),
    Membership.mem (γ := Set (Set α))
        {a : Set α |
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
            (interior a).Nonempty ∧
              ∃ (r : ℝ),
                a ⊆ closedBall x r ∧
                  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
        s ∧
      s ⊆ closedBall x ε
have obtain : ∀ (r : ℝ)
  (μr :
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
  (rpos : 0 < r) (rε : r ≤ ε),
  ∃ (s : Set α),
    Membership.mem (γ := Set (Set α))
        {a : Set α |
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
            (interior a).Nonempty ∧
              ∃ (r : ℝ),
                a ⊆ closedBall x r ∧
                  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
        s ∧
      s ⊆ closedBall x ε
Tactic: obtain ⟨r, μr, rpos, rε⟩ :
        ∃ r, μ (closedBall x (3 * r)) ≤ C * μ (closedBall x r) ∧ r ∈ Ioc (0 : ℝ) ε :=
      ((h x).and_eventually (Ioc_mem_nhdsGT εpos)).exists
-- 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 μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
x : α
ε : ℝ
εpos : ε > 0
r : ℝ
μr :
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
rpos : 0 < r
rε : r ≤ ε
⊢ ∃ (s : Set α),
    Membership.mem (γ := Set (Set α))
        {a : Set α |
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
            (interior a).Nonempty ∧
              ∃ (r : ℝ),
                a ⊆ closedBall x r ∧
                  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
        s ∧
      s ⊆ closedBall x ε
have refine : (interior (closedBall x r)).Nonempty
Tactic: refine ⟨closedBall x r, ⟨isClosed_closedBall, ?_, ⟨r, Subset.rfl, μr⟩⟩, by gcongr⟩
-- 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 μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
x : α
xs : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
have rcases : ∀ (a : Set α) (ha : a ∈ f x) (h'a : a ⊆ closedBall x ε), ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
Tactic: rcases ffine x xs ε εpos with ⟨a, ha, h'a⟩
-- 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 μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
x : α
xs : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
ha : a ∈ f x
h'a : a ⊆ closedBall x ε
⊢ ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
have rcases : ∀ (a_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a) (a_int : (interior a).Nonempty) (r : ℝ)
  (ar : a ⊆ closedBall x r)
  (μr :
    (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)),
  ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
Tactic: rcases fsubset x xs ha with ⟨a_closed, a_int, ⟨r, ar, μr⟩⟩
-- 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 μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
x : α
xs : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
ha : a ∈ f x
h'a : a ⊆ closedBall x ε
a_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
a_int : (interior a).Nonempty
r : ℝ
ar : a ⊆ closedBall x r
μr :
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
have refine_1 : (min r ε, x, a).2.2 ⊆ closedBall (min r ε, x, a).2.1 (min r ε, x, a).1
Tactic: refine ⟨⟨min r ε, x, a⟩, ⟨?_, ?_, a_int, a_closed, ha, xs⟩, min_le_right _ _, rfl⟩
-- 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 μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
x : α
xs : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
ha : a ∈ f x
h'a : a ⊆ closedBall x ε
a_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
a_int : (interior a).Nonempty
r : ℝ
ar : a ⊆ closedBall x r
μr :
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
refine_1 : (min r ε, x, a).2.2 ⊆ closedBall (min r ε, x, a).2.1 (min r ε, x, a).1
⊢ ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
have refine_2 : (μ : (a : Set α) → ℝ≥0∞) (closedBall (min r ε, x, a).2.1 (3 * (min r ε, x, a).1)) ≤
  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (min r ε, x, a).2.2 : ℝ≥0∞)
Tactic: refine ⟨⟨min r ε, x, a⟩, ⟨?_, ?_, a_int, a_closed, ha, xs⟩, min_le_right _ _, rfl⟩
-- 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 μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
x : α
xs : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
ha : a ∈ f x
h'a : a ⊆ closedBall x ε
a_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
a_int : (interior a).Nonempty
r : ℝ
ar : a ⊆ closedBall x r
μr :
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ (min r ε, x, a).2.2 ⊆ closedBall (min r ε, x, a).2.1 (min r ε, x, a).1
have refine_1 : ∀ (h' : min r ε = r ∧ r ≤ ε), (min r ε, x, a).2.2 ⊆ closedBall (min r ε, x, a).2.1 (min r ε, x, a).1
Tactic: rcases min_cases r ε with (h' | h')