case inl
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ ∅ → r a ≤ R
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ ∅ → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)

case inr
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
rcases eq_empty_or_nonempty t with (rfl | _)
case pos
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∀ (a : ι), a ∈ t → r a < 0
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)

case neg
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ¬∀ (a : ι), a ∈ t → r a < 0
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
case inr
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
by_cases ht : ∀ a ∈ t, r a < 0
case neg
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
case neg
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ¬∀ (a : ι), a ∈ t → r a < 0
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
push_neg at ht
case neg
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
case neg
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
let t' := { a ∈ t | 0 ≤ r a }
case neg.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
case neg
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
rcases exists_disjoint_subfamily_covering_enlargment (fun a => closedBall (x a) (r a)) t' r 2
    one_lt_two (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⟩
case neg.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
A : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
case neg.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
have A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (5 * 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
case neg.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
A : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
a : ι
ha : a ∈ t
⊢ ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
case neg.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
A : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
refine' ⟨u, ut'.trans fun a ha => ha.1, u_disj, fun a ha => _⟩
case neg.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
A : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
a : ι
ha : a ∈ t
h'a : 0 ≤ r a
⊢ ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)

case neg.intro.intro.intro.inr
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
A : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
a : ι
ha : a ∈ t
h'a : r a < 0
⊢ ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
case neg.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
A : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
a : ι
ha : a ∈ t
⊢ ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
rcases le_or_lt 0 (r a) with (h'a | h'a)
no goals
case inl
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ ∅ → r a ≤ R
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ ∅ → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
exact ⟨∅, Subset.refl _, pairwiseDisjoint_empty, by simp⟩
no goals
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ ∅ → r a ≤ R
⊢ ∀ (a : ι), a ∈ ∅ → ∃ b, b ∈ ∅ ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
simp
no goals
case pos
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∀ (a : ι), a ∈ t → r a < 0
⊢ ∃ u x_1,
    (PairwiseDisjoint u fun a => closedBall (x a) (r a)) ∧
      ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
exact ⟨t, Subset.rfl, fun a ha b _ _ => by
  simp only [Function.onFun, closedBall_eq_empty.2 (ht a ha), empty_disjoint],
  fun a ha => ⟨a, ha, by simp only [closedBall_eq_empty.2 (ht a ha), empty_subset]⟩⟩
no goals
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∀ (a : ι), a ∈ t → r a < 0
a : ι
ha : a ∈ t
b : ι
x✝¹ : b ∈ t
x✝ : a ≠ b
⊢ (Disjoint on fun a => closedBall (x a) (r a)) a b
simp only [Function.onFun, closedBall_eq_empty.2 (ht a ha), empty_disjoint]
no goals
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∀ (a : ι), a ∈ t → r a < 0
a : ι
ha : a ∈ t
⊢ closedBall (x a) (r a) ⊆ closedBall (x a) (5 * r a)
simp only [closedBall_eq_empty.2 (ht a ha), empty_subset]
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
a : ι
ha : a ∈ t'
⊢ ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
⊢ ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
intro a ha
case intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b))
rb : r a ≤ 2 * r b
⊢ ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
a : ι
ha : a ∈ t'
⊢ ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
rcases hu a ha with ⟨b, bu, hb, rb⟩
case intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b))
rb : r a ≤ 2 * r b
⊢ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
case intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b))
rb : r a ≤ 2 * r b
⊢ ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
refine' ⟨b, bu, _⟩
case intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b))
rb : r a ≤ 2 * r b
this : dist (x a) (x b) ≤ r a + r b
⊢ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
case intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b))
rb : r a ≤ 2 * r b
⊢ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
have : dist (x a) (x b) ≤ r a + r b := dist_le_add_of_nonempty_closedBall_inter_closedBall hb
case intro.intro.intro.h
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b))
rb : r a ≤ 2 * r b
this : dist (x a) (x b) ≤ r a + r b
⊢ r a + dist (x a) (x b) ≤ 5 * r b
case intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b))
rb : r a ≤ 2 * r b
this : dist (x a) (x b) ≤ r a + r b
⊢ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
apply closedBall_subset_closedBall'
no goals
case intro.intro.intro.h
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b))
rb : r a ≤ 2 * r b
this : dist (x a) (x b) ≤ r a + r b
⊢ r a + dist (x a) (x b) ≤ 5 * r b
linarith
no goals
case neg.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
A : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
a : ι
ha : a ∈ t
h'a : 0 ≤ r a
⊢ ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
exact A a ⟨ha, h'a⟩
case neg.intro.intro.intro.inr.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
A : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
a : ι
ha : a ∈ t
h'a : r a < 0
b : ι
rb : b ∈ t ∧ 0 ≤ r b
⊢ ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
case neg.intro.intro.intro.inr
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
ht : ∃ a, a ∈ t ∧ 0 ≤ r a
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
A : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
a : ι
ha : a ∈ t
h'a : r a < 0
⊢ ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
rcases ht with ⟨b, rb⟩
case neg.intro.intro.intro.inr.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
A : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * 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) (5 * r c)
⊢ ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
case neg.intro.intro.intro.inr.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
A : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
a : ι
ha : a ∈ t
h'a : r a < 0
b : ι
rb : b ∈ t ∧ 0 ≤ r b
⊢ ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
rcases A b ⟨rb.1, rb.2⟩ with ⟨c, cu, _⟩
no goals
case neg.intro.intro.intro.inr.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
A : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * 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) (5 * r c)
⊢ ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * r b)
refine' ⟨c, cu, by simp only [closedBall_eq_empty.2 h'a, empty_subset]⟩
no goals
α : Type u_1
ι : Type u_2
inst✝ : MetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ (a : ι), a ∈ t → r a ≤ R
h✝ : Set.Nonempty t
t' : Set ι := {a | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint u fun a => closedBall (x a) (r a)
hu : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ Set.Nonempty (closedBall (x a) (r a) ∩ closedBall (x b) (r b)) ∧ r a ≤ 2 * r b
A : ∀ (a : ι), a ∈ t' → ∃ b, b ∈ u ∧ closedBall (x a) (r a) ⊆ closedBall (x b) (5 * 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) (5 * r c)
⊢ closedBall (x a) (r a) ⊆ closedBall (x c) (5 * r c)
simp only [closedBall_eq_empty.2 h'a, empty_subset]