awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
obtain : ∀ (r' : ℝ) (r'mem : r' ∈ r '' v) (hr' : R0 / 2 < r'), ∃ a ∈ v, R0 / 2 < r a
⊢ ∃ a ∈ v, R0 / 2 < r a

Tactic:
obtain ⟨r', r'mem, hr'⟩ : ∃ r' ∈ r '' v, R0 / 2 < r' :=
          exists_lt_of_lt_csSup (vnonempty.image _) (half_lt_self R0pos)

Premises used: half_lt_self, exists_lt_of_lt_csSup, Set.Nonempty.image
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
r' : ℝ
r'mem : r' ∈ r '' v
hr' : R0 / 2 < r'
rcases : ∀ (a : ι) (hav : a ∈ v) (r'mem : r a ∈ r '' v) (hr' : R0 / 2 < r a), ∃ a ∈ v, R0 / 2 < r a
⊢ ∃ a ∈ v, R0 / 2 < r a

Tactic:
rcases (mem_image _ _ _).1 r'mem with ⟨a, hav, rfl⟩

Premises used: Set.mem_image, Iff.mp, rfl
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
a : ι
hav : a ∈ v
r'mem : r a ∈ r '' v
hr' : R0 / 2 < r a
⊢ ∃ a ∈ v, R0 / 2 < r a

Tactic:
⟨a, hav, hr'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
a : ι
hav : a ∈ v
r'mem : r a ∈ r '' v
hr' : R0 / 2 < r a
⊢ ∃ a ∈ v, R0 / 2 < r a

Tactic:
exact ⟨a, hav, hr'⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
inr :
  ∀ (a : ι) (hav : a ∈ v) (R0a : R0 / 2 < r a),
    ∃ (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

Tactic:
obtain ⟨a, hav, R0a⟩ : ∃ a ∈ v, R0 / 2 < r a := by
        obtain ⟨r', r'mem, hr'⟩ : ∃ r' ∈ r '' v, R0 / 2 < r' :=
          exists_lt_of_lt_csSup (vnonempty.image _) (half_lt_self R0pos)
        rcases (mem_image _ _ _).1 r'mem with ⟨a, hav, rfl⟩
        exact ⟨a, hav, hr'⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
a : ι
hav : a ∈ v
R0a : R0 / 2 < r a
⊢ ∃ (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:
⟨8 * R0, ?_, ?_⟩

Premises used: HMul.hMul, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
a : ι
hav : a ∈ v
R0a : R0 / 2 < r a
inr : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (8 * R0)) : ℝ≥0∞) (∞ : ℝ≥0∞)
inr₁ : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x (8 * 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:
refine ⟨8 * R0, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
a : ι
hav : a ∈ v
R0a : R0 / 2 < r a
apply : closedBall x (8 * R0) ⊆ closedBall (c a) (20 * R (c a))
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (8 * R0)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply lt_of_le_of_lt (measure_mono _) (hRμ (c a))

Premises used: lt_of_le_of_lt, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
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 : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
a : ι
hav : a ∈ v
R0a : R0 / 2 < r a
h : 8 * R0 + dist x (c a) ≤ 20 * R (c a)
⊢ closedBall x (8 * R0) ⊆ closedBall (c a) (20 * R (c a))

Tactic:
apply closedBall_subset_closedBall'

Premises used: Metric.closedBall_subset_closedBall'
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
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 : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
a : ι
hav : a ∈ v
R0a : R0 / 2 < r a
h : 8 * R0 + dist (c a) x ≤ 20 * R (c a)
⊢ 8 * R0 + dist x (c a) ≤ 20 * R (c a)

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
a : ι
hav : a ∈ v
R0a : R0 / 2 < r a
linarith : 20 * R (c a) < 8 * R0 + dist (c a) x → 2 / 2 = 1
linarith₁ : 20 * R (c a) < 8 * R0 + dist (c a) x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 20 * R (c a) < 8 * R0 + dist (c a) x → GT.gt (α := ℝ) 2 0
linarith₃ :
  20 * R (c a) < 8 * R0 + dist (c a) x →
    2 * (R x - R0) + (0 - R0) + 19 * (1 * R0 - 2 * r a) + 2 * (20 * R (c a) - (8 * R0 + dist (c a) x)) +
          2 * (dist (c a) x - (r a + R x)) +
        40 * (r a - R (c a)) =
      0
linarith₄ : 20 * R (c a) < 8 * R0 + dist (c a) x → GT.gt (α := ℝ) 2 0
linarith₅ : 20 * R (c a) < 8 * R0 + dist (c a) x → GT.gt (α := ℝ) 19 0
linarith₆ linarith₇ : 20 * R (c a) < 8 * R0 + dist (c a) x → GT.gt (α := ℝ) 2 0
linarith₈ : 20 * R (c a) < 8 * R0 + dist (c a) x → GT.gt (α := ℝ) 40 0
⊢ 8 * R0 + dist (c a) x ≤ 20 * R (c a)

Tactic:
linarith [Idist_v a hav, (ut' (vu hav)).2]

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
a : ι
hav : a ∈ v
R0a : R0 / 2 < r a
b : ι
bu : b ∈ u
hbx : (B b ∩ ball x (R x)).Nonempty
⊢ B b ⊆ closedBall x (8 * R0)

Tactic:
(hB b (ut bu)).trans ?_

Premises used: HasSubset.Subset.trans
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
a : ι
hav : a ∈ v
R0a : R0 / 2 < r a
b : ι
bu : b ∈ u
hbx : (B b ∩ ball x (R x)).Nonempty
inr : closedBall (c b) (r b) ⊆ closedBall x (8 * R0)
⊢ B b ⊆ closedBall x (8 * R0)

Tactic:
refine (hB b (ut bu)).trans ?_

Premises used: HasSubset.Subset.trans
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 : R x ≤ R0
R0pos : 0 < R0
vnonempty : v.Nonempty
a : ι
hav : a ∈ v
R0a : R0 / 2 < r a
b : ι
bu : b ∈ u
hbx : (B b ∩ ball x (R x)).Nonempty
inr : r b + dist (c b) x ≤ 8 * R0
⊢ closedBall (c b) (r b) ⊆ closedBall x (8 * R0)

Tactic:
apply closedBall_subset_closedBall'

Premises used: Metric.closedBall_subset_closedBall'