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
a : ι
hav : a ∈ v
⊢ B a ∩ ball x (R x) ⊆ closedBall (c a) (r a) ∩ closedBall x (R x)
have h : B a ⊆ closedBall (c a) (r a)
Tactic: 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 μ
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_1 : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
a : ι
hav : a ∈ v
h : B a ⊆ closedBall (c a) (r a)
⊢ B a ∩ ball x (R x) ⊆ closedBall (c a) (r a) ∩ closedBall x (R x)
have h₁ : ball x (R x) ⊆ closedBall x (R x)
Tactic: gcongr
-- 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 : ℝ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
have Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
Tactic: have Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x := by
      intro a hav
      apply dist_le_add_of_nonempty_closedBall_inter_closedBall
      refine hav.2.mono ?_
      gcongr
      exacts [hB a (ut (vu hav)), ball_subset_closedBall]
-- 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
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
⊢ ∃ (K : ℝ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
have R0_def : let R0 := sSup (r '' v);
R0 = sSup (r '' v)
Tactic: set R0 := sSup (r '' v) with R0_def
-- 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
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
⊢ BddAbove (r '' v)
have refine : ∀ (r' : ℝ) (hr' : r' ∈ r '' v), r' ≤ 1
Tactic: refine ⟨1, fun r' hr' => ?_⟩
-- 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
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
r' : ℝ
hr' : r' ∈ r '' v
⊢ r' ≤ 1
have rcases : ∀ (b : ι) (hb : b ∈ v) (hr' : r b ∈ r '' v), r b ≤ 1
Tactic: rcases (mem_image _ _ _).1 hr' with ⟨b, hb, rfl⟩
Cleared hypotheses: r', hr'
-- 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
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
⊢ ∃ (K : ℝ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
have R0_bdd : BddAbove (r '' v)
Tactic: have R0_bdd : BddAbove (r '' v) := by
      refine ⟨1, fun r' hr' => ?_⟩
      rcases (mem_image _ _ _).1 hr' with ⟨b, hb, rfl⟩
      exact le_trans (ut' (vu hb)).2 (hR1 (c b))
-- 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
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
⊢ ∃ (K : ℝ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
have inl : ∀ (H : R0 ≤ R x),
  ∃ (K : ℝ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
Tactic: rcases le_total R0 (R x) with (H | H)
-- 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
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
inl :
  ∀ (H : R0 ≤ R x),
    ∃ (K : ℝ),
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
⊢ ∃ (K : ℝ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
have inr : ∀ (H : R x ≤ R0),
  ∃ (K : ℝ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
Tactic: rcases le_total R0 (R x) with (H | H)
-- 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
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
H : R0 ≤ R x
⊢ ∃ (K : ℝ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
have inl : ∀ (a : ι) (au : a ∈ u) (hax : (B a ∩ ball x (R x)).Nonempty), B a ⊆ closedBall x (20 * R x)
Tactic: refine ⟨20 * R x, hRμ x, fun a au hax => ?_⟩
-- 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
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
H : R0 ≤ R x
a : ι
au : a ∈ u
hax : (B a ∩ ball x (R x)).Nonempty
⊢ B a ⊆ closedBall x (20 * R x)
have inl : closedBall (c a) (r a) ⊆ closedBall x (20 * R x)
Tactic: refine (hB a (ut au)).trans ?_
-- 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
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
H : R0 ≤ R x
a : ι
au : a ∈ u
hax : (B a ∩ ball x (R x)).Nonempty
⊢ closedBall (c a) (r a) ⊆ closedBall x (20 * R x)
have inl : r a + dist (c a) x ≤ 20 * R x
Tactic: apply closedBall_subset_closedBall'
-- 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
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
H : R0 ≤ R x
a : ι
au : a ∈ u
hax : (B a ∩ ball x (R x)).Nonempty
⊢ r a + dist (c a) x ≤ 20 * R x
have this : r a ≤ R0
Tactic: have : r a ≤ R0 := le_csSup R0_bdd (mem_image_of_mem _ ⟨au, hax⟩)
-- 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
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
H : R0 ≤ R x
a : ι
au : a ∈ u
hax : (B a ∩ ball x (R x)).Nonempty
this : r a ≤ R0
⊢ r a + dist (c a) x ≤ 20 * R x
have linarith : 20 * R x < r a + dist (c a) x →
  2 * (R0 - R x) + 2 * (r a - R0) + (20 * R x - (r a + dist (c a) x)) + (dist (c a) x - (r a + R x)) + 17 * (0 - R x) =
    0
Tactic: linarith [Idist_v a ⟨au, hax⟩, hR0 x]
-- 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
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
H : R0 ≤ R x
a : ι
au : a ∈ u
hax : (B a ∩ ball x (R x)).Nonempty
this : r a ≤ R0
linarith :
  20 * R x < r a + dist (c a) x →
    2 * (R0 - R x) + 2 * (r a - R0) + (20 * R x - (r a + dist (c a) x)) + (dist (c a) x - (r a + R x)) +
        17 * (0 - R x) =
      0
⊢ r a + dist (c a) x ≤ 20 * R x
have linarith₁ : 20 * R x < r a + dist (c a) x → GT.gt (α := ℝ) 2 0
Tactic: linarith [Idist_v a ⟨au, hax⟩, hR0 x]