awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
c : ι
ct : c ∈ t
b : ι
hcb : (B c ∩ B b).Nonempty
H : ∀ (d : ι) (_ : d ∈ u), Disjoint (B c) (B d)
a'A : b ∈ A
ha' : m / τ ≤ δ b
a'_ne_u : b ∉ u
ba'u : b ∈ insert b u
δ₁ : m = τ * (m / τ)
δ₂ : τ * (m / τ) ≤ τ * δ b
⊢ δ c ≤ τ * δ b

Tactic:
calc
          δ c ≤ m := le_csSup bddA (mem_image_of_mem _ ⟨ct, H⟩)
          _ = τ * (m / τ) := by field
          _ ≤ τ * δ b := by gcongr

Premises used: HDiv.hDiv, Set.mem_image_of_mem, And.intro, le_csSup
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
ct : c ∈ t
b : ι
ba'u : b ∈ insert a' u
hcb : (B c ∩ B b).Nonempty
H : ∀ (d : ι) (_ : d ∈ u), Disjoint (B c) (B d)
H' : b ∈ u
⊢ ¬Disjoint (B c) (B b)

Tactic:
rw [← not_disjoint_iff_nonempty_inter] at hcb

Premises used: Set.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
ct : c ∈ t
b : ι
ba'u : b ∈ insert a' u
hcb : (B c ∩ B b).Nonempty
H : ∀ (d : ι) (_ : d ∈ u), Disjoint (B c) (B d)
H' : b ∈ u
hcb₁ : ¬Disjoint (B c) (B b)
⊢ ∀ (d : ι) (_ : d ∈ u), Disjoint (B c) (B d)

Tactic:
rw [← not_disjoint_iff_nonempty_inter] at hcb

Premises used: Set.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
ct : c ∈ t
b : ι
ba'u : b ∈ insert a' u
hcb : (B c ∩ B b).Nonempty
H : ∀ (d : ι) (_ : d ∈ u), Disjoint (B c) (B d)
H' : b ∈ u
hcb₁ : ¬Disjoint (B c) (B b)
H₁ : ∀ (d : ι) (_ : d ∈ u), Disjoint (B c) (B d)
⊢ b ∈ u

Tactic:
rw [← not_disjoint_iff_nonempty_inter] at hcb

Premises used: Set.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
ct : c ∈ t
b : ι
ba'u : b ∈ insert a' u
hcb : ¬Disjoint (B c) (B b)
H : ∀ (d : ι) (_ : d ∈ u), Disjoint (B c) (B d)
H' : b ∈ u
⊢ ∃ c_1 ∈ insert a' u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1

Tactic:
(hcb (H _ H')).elim

Premises used: False.elim
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
ct : c ∈ t
b : ι
ba'u : b ∈ insert a' u
hcb : ¬Disjoint (B c) (B b)
H : ∀ (d : ι) (_ : d ∈ u), Disjoint (B c) (B d)
H' : b ∈ u
⊢ ∃ c_1 ∈ insert a' u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1

Tactic:
exact (hcb (H _ H')).elim

Premises used: False.elim
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
inl :
  ∀ (hr : ∀ (a : ι), Membership.mem (γ := Set ι) ∅ a → r a ≤ R),
    ∃ u ⊆ ∅,
      (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)) ∧
        ∀ (a : ι), Membership.mem (γ := Set ι) ∅ a → ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
inr :
  t.Nonempty →
    ∃ u ⊆ t,
      (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)) ∧
        ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
⊢ ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
rcases eq_empty_or_nonempty t with (rfl | _)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
x : ι → α
r : ι → ℝ
R τ : ℝ
hτ : 3 < τ
hr : ∀ (a : ι), Membership.mem (γ := Set ι) ∅ a → r a ≤ R
⊢ ∀ (a : ι),
    Membership.mem (γ := Set ι) ∅ a →
      ∃ (b : ι), Membership.mem (γ := Set ι) ∅ b ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
x : ι → α
r : ι → ℝ
R τ : ℝ
hτ : 3 < τ
hr : ∀ (a : ι), Membership.mem (γ := Set ι) ∅ a → r a ≤ R
⊢ ∃ u ⊆ ∅,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)) ∧
      ∀ (a : ι), Membership.mem (γ := Set ι) ∅ a → ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
exact ⟨∅, Subset.refl _, pairwiseDisjoint_empty, by simp⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
pos :
  ∀ (ht : ∀ a ∈ t, r a < 0),
    ∃ u ⊆ t,
      (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)) ∧
        ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
neg :
  ∀ (ht : ∃ a ∈ t, 0 ≤ r a),
    ∃ u ⊆ t,
      (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)) ∧
        ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
⊢ ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
by_cases! ht : ∀ a ∈ t, r a < 0
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∀ a ∈ t, r a < 0
a : ι
ha : a ∈ t
b : ι
h_1 : b ∈ t
h_2 : a ≠ b
⊢ Function.onFun.{u_2 + 1, u_1 + 1, 1} (β := Set α) Disjoint (fun (a : ι) ↦ closedBall (x a) (r a)) a b

Tactic:
simp only [closedBall_eq_empty.2 (ht a ha), empty_disjoint, Function.onFun]

Premises used: Iff.mpr, Function.onFun, Metric.closedBall_eq_empty, Set.empty_disjoint
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∀ a ∈ t, r a < 0
a : ι
ha : a ∈ t
⊢ closedBall (x a) (r a) ⊆ closedBall (x a) (τ * r a)

Tactic:
simp only [closedBall_eq_empty.2 (ht a ha), empty_subset]

Premises used: Iff.mpr, Metric.closedBall_eq_empty, Set.empty_subset
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∀ a ∈ t, r a < 0
⊢ ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
exact ⟨t, Subset.rfl, fun a ha b _ _ => by
      simp only [closedBall_eq_empty.2 (ht a ha), empty_disjoint, Function.onFun],
      fun a ha => ⟨a, ha, by simp only [closedBall_eq_empty.2 (ht a ha), empty_subset]⟩⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
linarith : (τ - 1) / 2 ≤ 1 → 2 / 2 = 1
linarith₁ : (τ - 1) / 2 ≤ 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (τ - 1) / 2 ≤ 1 → GT.gt (α := ℝ) 2 0
linarith₃ : (τ - 1) / 2 ≤ 1 → 3 - τ + (1 * τ - HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 2 1) = 0
⊢ 1 < (τ - 1) / 2

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
neg :
  ∀ (u : Set ι) (ut' : u ⊆ t')
    (u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a))
    (hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b),
    ∃ u ⊆ t,
      (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)) ∧
        ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
⊢ ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
rcases exists_disjoint_subfamily_covering_enlargement (fun a => closedBall (x a) (r a)) t' r
      ((τ - 1) / 2) (by linarith) (fun a ha => ha.2) R (fun a ha => hr a ha.1) fun a ha =>
      ⟨x a, mem_closedBall_self ha.2⟩ with
    ⟨u, ut', u_disj, hu⟩

Premises used: HSub.hSub, HDiv.hDiv, Vitali.exists_disjoint_subfamily_covering_enlargement, And.right, And.left, Exists.intro, Metric.closedBall, OfNat.ofNat, Metric.mem_closedBall_self
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
rcases :
  ∀ (b : ι) (bu : b ∈ u) (hb : (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty)
    (rb : r a ≤ (τ - 1) / 2 * r b), ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
rcases hu a ha with ⟨b, bu, hb, rb⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
⟨b, bu, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
refine : closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
refine ⟨b, bu, ?_⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
⊢ dist (x a) (x b) ≤ r a + r b

Tactic:
have : dist (x a) (x b) ≤ r a + r b := dist_le_add_of_nonempty_closedBall_inter_closedBall hb
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h_1 : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) ≤ r a + r b
h : r a + dist (x a) (x b) ≤ τ * r b
⊢ closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

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 α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) ≤ r a + r b
linarith : τ * r b < r a + dist (x a) (x b) → 2 / 2 = 1
linarith₁ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : τ * r b < r a + dist (x a) (x b) → GT.gt (α := ℝ) 2 0
linarith₄ :
  τ * r b < r a + dist (x a) (x b) →
    2 * r a - (1 * τ - HMul.hMul (α := ℝ) 1 1) * (1 * r b) + (dist (x a) (x b) - (r a + r b)) +
        (τ * r b - (r a + dist (x a) (x b))) =
      0
⊢ r a + dist (x a) (x b) ≤ τ * r b

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
⊢ ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
have A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b) := by
    intro a ha
    rcases hu a ha with ⟨b, bu, hb, rb⟩
    refine ⟨b, bu, ?_⟩
    have : dist (x a) (x b) ≤ r a + r b := dist_le_add_of_nonempty_closedBall_inter_closedBall hb
    apply closedBall_subset_closedBall'
    linarith
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
⊢ ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
⟨u, ut'.trans fun a ha => ha.1, u_disj, fun a ha => ?_⟩

Premises used: HasSubset.Subset.trans, And.left, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
neg : ∀ (a : ι) (ha : a ∈ t), ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
⊢ ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
refine ⟨u, ut'.trans fun a ha => ha.1, u_disj, fun a ha => ?_⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
a : ι
ha : a ∈ t
neg : ∀ (h'a : 0 ≤ r a), ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
neg₁ : ∀ (h'a : r a < 0), ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
rcases le_or_gt 0 (r a) with (h'a | h'a)

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
a : ι
ha : a ∈ t
h'a : 0 ≤ r a
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
A a ⟨ha, h'a⟩

Premises used: And.intro
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
a : ι
ha : a ∈ t
h'a : 0 ≤ r a
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
exact A a ⟨ha, h'a⟩

Premises used: And.intro
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
a : ι
ha : a ∈ t
h'a : r a < 0
neg : ∀ (b : ι) (rb : b ∈ t ∧ 0 ≤ r b), ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
rcases ht with ⟨b, rb⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
a : ι
ha : a ∈ t
h'a : r a < 0
b : ι
rb : b ∈ t ∧ 0 ≤ r b
neg :
  ∀ (c : ι) (cu : c ∈ u),
    closedBall (x b) (r b) ⊆ closedBall (x c) (τ * r c) → ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
rcases A b ⟨rb.1, rb.2⟩ with ⟨c, cu, _⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
a : ι
ha : a ∈ t
h'a : r a < 0
b : ι
rb : b ∈ t ∧ 0 ≤ r b
c : ι
cu : c ∈ u
right : closedBall (x b) (r b) ⊆ closedBall (x c) (τ * r c)
⊢ closedBall (x a) (r a) ⊆ closedBall (x c) (τ * r c)

Tactic:
simp only [closedBall_eq_empty.2 h'a, empty_subset]

Premises used: Iff.mpr, Metric.closedBall_eq_empty, Set.empty_subset