α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
⊢ ∃ u x, PairwiseDisjoint u B ∧ ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ Set.Nonempty (B a ∩ B b) ∧ δ a ≤ τ * δ b
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
⊢ ∃ u x, PairwiseDisjoint u B ∧ ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ Set.Nonempty (B a ∩ B b) ∧ δ a ≤ τ * δ b
let T : Set (Set ι) := { u | u ⊆ t ∧ u.PairwiseDisjoint B ∧
  ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c }
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
hu : ∀ (v : Set ι), v ∈ T → u ⊆ v → v = u
⊢ ∃ u x, PairwiseDisjoint u B ∧ ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ Set.Nonempty (B a ∩ B b) ∧ δ a ≤ τ * δ b
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
⊢ ∃ u x, PairwiseDisjoint u B ∧ ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ Set.Nonempty (B a ∩ B b) ∧ δ a ≤ τ * δ b
obtain ⟨u, uT, hu⟩ : ∃ u ∈ T, ∀ v ∈ T, u ⊆ v → v = u := by
  refine' zorn_subset _ fun U UT hU => _
  refine' ⟨⋃₀ U, _, fun s hs => subset_sUnion_of_mem hs⟩
  simp only [Set.sUnion_subset_iff, and_imp, exists_prop, forall_exists_index, mem_sUnion,
    Set.mem_setOf_eq]
  refine'
    ⟨fun u hu => (UT hu).1, (pairwiseDisjoint_sUnion hU.directedOn).2 fun u hu => (UT hu).2.1,
      fun a hat b u uU hbu hab => _⟩
  obtain ⟨c, cu, ac, hc⟩ : ∃ c, c ∈ u ∧ (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c :=
    (UT uU).2.2 a hat b hbu hab
  exact ⟨c, ⟨u, uU, cu⟩, ac, hc⟩
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
hu : ∀ (v : Set ι), v ∈ T → u ⊆ v → v = u
a : ι
hat : a ∈ t
⊢ ∃ b, b ∈ u ∧ Set.Nonempty (B a ∩ B b) ∧ δ a ≤ τ * δ b
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
hu : ∀ (v : Set ι), v ∈ T → u ⊆ v → v = u
⊢ ∃ u x, PairwiseDisjoint u B ∧ ∀ (a : ι), a ∈ t → ∃ b, b ∈ u ∧ Set.Nonempty (B a ∩ B b) ∧ δ a ≤ τ * δ b
refine' ⟨u, uT.1, uT.2.1, fun a hat => _⟩
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
hu : ∀ (v : Set ι), v ∈ T → u ⊆ v → v = u
a : ι
hat : a ∈ t
⊢ ∃ b, b ∈ u ∧ Set.Nonempty (B a ∩ B b) ∧ δ a ≤ τ * δ b
contrapose! hu
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
have a_disj : ∀ c ∈ u, Disjoint (B a) (B c) := by
  intro c hc
  by_contra h
  rw [not_disjoint_iff_nonempty_inter] at h
  obtain ⟨d, du, ad, hd⟩ : ∃ d, d ∈ u ∧ (B a ∩ B d).Nonempty ∧ δ a ≤ τ * δ d :=
    uT.2.2 a hat c hc h
  exact lt_irrefl _ ((hu d du ad).trans_le hd)
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
let A := { a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c) }
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
have Anonempty : A.Nonempty := ⟨a, hat, a_disj⟩
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
let m := sSup (δ '' A)
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
have bddA : BddAbove (δ '' A) := by
  refine' ⟨R, fun x xA => _⟩
  rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩
  exact δle a' ha'.1
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
clear hat hu a_disj a
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : ¬a' ∈ u
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
have a'_ne_u : a' ∉ u := fun H => (hne _ a'A.1).ne_empty (disjoint_self.1 (a'A.2 _ H))
case intro.intro.intro.intro.refine'_1
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : ¬a' ∈ u
⊢ insert a' u ⊆ t

case intro.intro.intro.intro.refine'_2
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : ¬a' ∈ u
⊢ PairwiseDisjoint (insert a' u) B

case intro.intro.intro.intro.refine'_3
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : ¬a' ∈ u
⊢ ∀ (a : ι),
    a ∈ t →
      ∀ (b : ι),
        b ∈ insert a' u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ insert a' u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : ¬a' ∈ u
⊢ ∃ v,
    v ∈
        {u |
          u ⊆ t ∧
            PairwiseDisjoint u B ∧
              ∀ (a : ι),
                a ∈ t →
                  ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c} ∧
      u ⊆ v ∧ v ≠ u
refine' ⟨insert a' u, ⟨_, _, _⟩, subset_insert _ _, (ne_insert_of_not_mem _ a'_ne_u).symm⟩
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun x x_1 => x ⊆ x_1) U
⊢ ∃ ub, ub ∈ T ∧ ∀ (s : Set ι), s ∈ U → s ⊆ ub
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
⊢ ∃ u, u ∈ T ∧ ∀ (v : Set ι), v ∈ T → u ⊆ v → v = u
refine' zorn_subset _ fun U UT hU => _
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun x x_1 => x ⊆ x_1) U
⊢ ⋃₀ U ∈ T
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun x x_1 => x ⊆ x_1) U
⊢ ∃ ub, ub ∈ T ∧ ∀ (s : Set ι), s ∈ U → s ⊆ ub
refine' ⟨⋃₀ U, _, fun s hs => subset_sUnion_of_mem hs⟩
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun x x_1 => x ⊆ x_1) U
⊢ (∀ (t' : Set ι), t' ∈ U → t' ⊆ t) ∧
    PairwiseDisjoint (⋃₀ U) B ∧
      ∀ (a : ι),
        a ∈ t →
          ∀ (b : ι) (x : Set ι),
            x ∈ U →
              b ∈ x → Set.Nonempty (B a ∩ B b) → ∃ c, (∃ t, t ∈ U ∧ c ∈ t) ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun x x_1 => x ⊆ x_1) U
⊢ ⋃₀ U ∈ T
simp only [Set.sUnion_subset_iff, and_imp, exists_prop, forall_exists_index, mem_sUnion,
  Set.mem_setOf_eq]
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun x x_1 => x ⊆ x_1) U
a : ι
hat : a ∈ t
b : ι
u : Set ι
uU : u ∈ U
hbu : b ∈ u
hab : Set.Nonempty (B a ∩ B b)
⊢ ∃ c, (∃ t, t ∈ U ∧ c ∈ t) ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun x x_1 => x ⊆ x_1) U
⊢ (∀ (t' : Set ι), t' ∈ U → t' ⊆ t) ∧
    PairwiseDisjoint (⋃₀ U) B ∧
      ∀ (a : ι),
        a ∈ t →
          ∀ (b : ι) (x : Set ι),
            x ∈ U →
              b ∈ x → Set.Nonempty (B a ∩ B b) → ∃ c, (∃ t, t ∈ U ∧ c ∈ t) ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c
refine'
  ⟨fun u hu => (UT hu).1, (pairwiseDisjoint_sUnion hU.directedOn).2 fun u hu => (UT hu).2.1,
    fun a hat b u uU hbu hab => _⟩
case intro.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun x x_1 => x ⊆ x_1) U
a : ι
hat : a ∈ t
b : ι
u : Set ι
uU : u ∈ U
hbu : b ∈ u
hab : Set.Nonempty (B a ∩ B b)
c : ι
cu : c ∈ u
ac : Set.Nonempty (B a ∩ B c)
hc : δ a ≤ τ * δ c
⊢ ∃ c, (∃ t, t ∈ U ∧ c ∈ t) ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun x x_1 => x ⊆ x_1) U
a : ι
hat : a ∈ t
b : ι
u : Set ι
uU : u ∈ U
hbu : b ∈ u
hab : Set.Nonempty (B a ∩ B b)
⊢ ∃ c, (∃ t, t ∈ U ∧ c ∈ t) ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c
obtain ⟨c, cu, ac, hc⟩ : ∃ c, c ∈ u ∧ (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c :=
  (UT uU).2.2 a hat b hbu hab
no goals
case intro.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun x x_1 => x ⊆ x_1) U
a : ι
hat : a ∈ t
b : ι
u : Set ι
uU : u ∈ U
hbu : b ∈ u
hab : Set.Nonempty (B a ∩ B b)
c : ι
cu : c ∈ u
ac : Set.Nonempty (B a ∩ B c)
hc : δ a ≤ τ * δ c
⊢ ∃ c, (∃ t, t ∈ U ∧ c ∈ t) ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c
exact ⟨c, ⟨u, uU, cu⟩, ac, hc⟩
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
c : ι
hc : c ∈ u
⊢ Disjoint (B a) (B c)
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
⊢ ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
intro c hc
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
c : ι
hc : c ∈ u
h : ¬Disjoint (B a) (B c)
⊢ False
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
c : ι
hc : c ∈ u
⊢ Disjoint (B a) (B c)
by_contra h
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
c : ι
hc : c ∈ u
h : Set.Nonempty (B a ∩ B c)
⊢ False
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
c : ι
hc : c ∈ u
h : ¬Disjoint (B a) (B c)
⊢ False
rw [not_disjoint_iff_nonempty_inter] at h
case intro.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
c : ι
hc : c ∈ u
h : Set.Nonempty (B a ∩ B c)
d : ι
du : d ∈ u
ad : Set.Nonempty (B a ∩ B d)
hd : δ a ≤ τ * δ d
⊢ False
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
c : ι
hc : c ∈ u
h : Set.Nonempty (B a ∩ B c)
⊢ False
obtain ⟨d, du, ad, hd⟩ : ∃ d, d ∈ u ∧ (B a ∩ B d).Nonempty ∧ δ a ≤ τ * δ d :=
  uT.2.2 a hat c hc h
no goals
case intro.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
c : ι
hc : c ∈ u
h : Set.Nonempty (B a ∩ B c)
d : ι
du : d ∈ u
ad : Set.Nonempty (B a ∩ B d)
hd : δ a ≤ τ * δ d
⊢ False
exact lt_irrefl _ ((hu d du ad).trans_le hd)
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
x : ℝ
xA : x ∈ δ '' A
⊢ x ≤ R
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
⊢ BddAbove (δ '' A)
refine' ⟨R, fun x xA => _⟩
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
a' : ι
ha' : a' ∈ A
xA : δ a' ∈ δ '' A
⊢ δ a' ≤ R
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
x : ℝ
xA : x ∈ δ '' A
⊢ x ≤ R
rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩
no goals
case intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
a' : ι
ha' : a' ∈ A
xA : δ a' ∈ δ '' A
⊢ δ a' ≤ R
exact δle a' ha'.1
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
⊢ ∃ a', a' ∈ A ∧ m / τ ≤ δ a'
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
⊢ ∃ a', a' ∈ A ∧ m / τ ≤ δ a'
have : 0 ≤ m := (δnonneg a hat).trans (le_csSup bddA (mem_image_of_mem _ ⟨hat, a_disj⟩))
case inl
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mzero : 0 = m
⊢ ∃ a', a' ∈ A ∧ m / τ ≤ δ a'

case inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
⊢ ∃ a', a' ∈ A ∧ m / τ ≤ δ a'
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
⊢ ∃ a', a' ∈ A ∧ m / τ ≤ δ a'
rcases eq_or_lt_of_le this with (mzero | mpos)
case inl
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mzero : 0 = m
⊢ m / τ ≤ δ a
case inl
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mzero : 0 = m
⊢ ∃ a', a' ∈ A ∧ m / τ ≤ δ a'
refine' ⟨a, ⟨hat, a_disj⟩, _⟩
no goals
case inl
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mzero : 0 = m
⊢ m / τ ≤ δ a
simpa only [← mzero, zero_div] using δnonneg a hat
case inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
I : m / τ < m
⊢ ∃ a', a' ∈ A ∧ m / τ ≤ δ a'
case inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
⊢ ∃ a', a' ∈ A ∧ m / τ ≤ δ a'
have I : m / τ < m := by
  rw [div_lt_iff (zero_lt_one.trans hτ)]
  conv_lhs => rw [← mul_one m]
  exact (mul_lt_mul_left mpos).2 hτ
case inr.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
I : m / τ < m
x : ℝ
xA : x ∈ δ '' A
hx : m / τ < x
⊢ ∃ a', a' ∈ A ∧ m / τ ≤ δ a'
case inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
I : m / τ < m
⊢ ∃ a', a' ∈ A ∧ m / τ ≤ δ a'
rcases exists_lt_of_lt_csSup (nonempty_image_iff.2 Anonempty) I with ⟨x, xA, hx⟩
case inr.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
I : m / τ < m
a' : ι
ha' : a' ∈ A
xA : δ a' ∈ δ '' A
hx : m / τ < δ a'
⊢ ∃ a', a' ∈ A ∧ m / τ ≤ δ a'
case inr.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
I : m / τ < m
x : ℝ
xA : x ∈ δ '' A
hx : m / τ < x
⊢ ∃ a', a' ∈ A ∧ m / τ ≤ δ a'
rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩
no goals
case inr.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
I : m / τ < m
a' : ι
ha' : a' ∈ A
xA : δ a' ∈ δ '' A
hx : m / τ < δ a'
⊢ ∃ a', a' ∈ A ∧ m / τ ≤ δ a'
exact ⟨a', ha', hx.le⟩
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
⊢ m < m * τ
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
⊢ m / τ < m
rw [div_lt_iff (zero_lt_one.trans hτ)]
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
⊢ m * 1 < m * τ
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
⊢ m < m * τ
conv_lhs => rw [← mul_one m]
no goals
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
a : ι
hat : a ∈ t
hu : ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → τ * δ b < δ a
a_disj : ∀ (c : ι), c ∈ u → Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
⊢ m * 1 < m * τ
exact (mul_lt_mul_left mpos).2 hτ
case intro.intro.intro.intro.refine'_1
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : ¬a' ∈ u
⊢ a' ∈ t ∧ u ⊆ t
case intro.intro.intro.intro.refine'_1
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : ¬a' ∈ u
⊢ insert a' u ⊆ t
rw [insert_subset]
no goals
case intro.intro.intro.intro.refine'_1
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : ¬a' ∈ u
⊢ a' ∈ t ∧ u ⊆ t
exact ⟨a'A.1, uT.1⟩
no goals
case intro.intro.intro.intro.refine'_2
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : ¬a' ∈ u
⊢ PairwiseDisjoint (insert a' u) B
exact uT.2.1.insert fun b bu _ => a'A.2 b bu
case intro.intro.intro.intro.refine'_3
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
case intro.intro.intro.intro.refine'_3
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : ¬a' ∈ u
⊢ ∀ (a : ι),
    a ∈ t →
      ∀ (b : ι),
        b ∈ insert a' u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ insert a' u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c
intro c ct b ba'u hcb
case pos
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
H : ∃ d, d ∈ u ∧ Set.Nonempty (B c ∩ B d)
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1

case neg
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
H : ¬∃ d, d ∈ u ∧ Set.Nonempty (B c ∩ B d)
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
case intro.intro.intro.intro.refine'_3
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
by_cases H : ∃ d ∈ u, (B c ∩ B d).Nonempty
case pos.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
d : ι
du : d ∈ u
hd : Set.Nonempty (B c ∩ B d)
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
case pos
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
H : ∃ d, d ∈ u ∧ Set.Nonempty (B c ∩ B d)
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
rcases H with ⟨d, du, hd⟩
case pos.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
d : ι
du : d ∈ u
hd : Set.Nonempty (B c ∩ B d)
d' : ι
d'u : d' ∈ u
hd' : Set.Nonempty (B c ∩ B d') ∧ δ c ≤ τ * δ d'
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
case pos.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
d : ι
du : d ∈ u
hd : Set.Nonempty (B c ∩ B d)
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
rcases uT.2.2 c ct d du hd with ⟨d', d'u, hd'⟩
no goals
case pos.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
d : ι
du : d ∈ u
hd : Set.Nonempty (B c ∩ B d)
d' : ι
d'u : d' ∈ u
hd' : Set.Nonempty (B c ∩ B d') ∧ δ c ≤ τ * δ d'
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
exact ⟨d', mem_insert_of_mem _ d'u, hd'⟩
case neg
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
H : ∀ (d : ι), d ∈ u → ¬Set.Nonempty (B c ∩ B d)
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
case neg
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
H : ¬∃ d, d ∈ u ∧ Set.Nonempty (B c ∩ B d)
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
push_neg at H
case neg
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
H : ∀ (d : ι), d ∈ u → Disjoint (B c) (B d)
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
case neg
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
H : ∀ (d : ι), d ∈ u → ¬Set.Nonempty (B c ∩ B d)
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
simp only [← not_disjoint_iff_nonempty_inter, Classical.not_not] at H
case neg.inl
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
c : ι
ct : c ∈ t
b : ι
hcb : Set.Nonempty (B c ∩ B b)
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
⊢ ∃ c_1, c_1 ∈ insert b u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1

case neg.inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
H : ∀ (d : ι), d ∈ u → Disjoint (B c) (B d)
H' : b ∈ u
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
case neg
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
H : ∀ (d : ι), d ∈ u → Disjoint (B c) (B d)
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
rcases mem_insert_iff.1 ba'u with (rfl | H')
case neg.inl
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
c : ι
ct : c ∈ t
b : ι
hcb : Set.Nonempty (B c ∩ B b)
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
⊢ δ c ≤ τ * δ b
case neg.inl
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
c : ι
ct : c ∈ t
b : ι
hcb : Set.Nonempty (B c ∩ B b)
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
⊢ ∃ c_1, c_1 ∈ insert b u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
refine' ⟨b, mem_insert _ _, hcb, _⟩
no goals
case neg.inl
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
c : ι
ct : c ∈ t
b : ι
hcb : Set.Nonempty (B c ∩ B b)
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
⊢ δ c ≤ τ * δ b
calc
  δ c ≤ m := le_csSup bddA (mem_image_of_mem _ ⟨ct, H⟩)
  _ = τ * (m / τ) := by
    field_simp [(zero_lt_one.trans hτ).ne']
    ring
  _ ≤ τ * δ b := mul_le_mul_of_nonneg_left ha' (zero_le_one.trans hτ.le)
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
c : ι
ct : c ∈ t
b : ι
hcb : Set.Nonempty (B c ∩ B b)
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
⊢ sSup (δ '' {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}) * τ =
    τ * sSup (δ '' {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)})
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
c : ι
ct : c ∈ t
b : ι
hcb : Set.Nonempty (B c ∩ B b)
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 / τ)
field_simp [(zero_lt_one.trans hτ).ne']
no goals
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
c : ι
ct : c ∈ t
b : ι
hcb : Set.Nonempty (B c ∩ B b)
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
⊢ sSup (δ '' {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}) * τ =
    τ * sSup (δ '' {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)})
ring
case neg.inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
case neg.inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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 : Set.Nonempty (B c ∩ B b)
H : ∀ (d : ι), d ∈ u → Disjoint (B c) (B d)
H' : b ∈ u
⊢ ∃ c_1, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
rw [← not_disjoint_iff_nonempty_inter] at hcb
no goals
case neg.inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ (a : ι), a ∈ t → 0 ≤ δ a
R : ℝ
δle : ∀ (a : ι), a ∈ t → δ a ≤ R
hne : ∀ (a : ι), a ∈ t → Set.Nonempty (B a)
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      PairwiseDisjoint u B ∧
        ∀ (a : ι),
          a ∈ t → ∀ (b : ι), b ∈ u → Set.Nonempty (B a ∩ B b) → ∃ c, c ∈ u ∧ Set.Nonempty (B a ∩ B c) ∧ δ a ≤ τ * δ c}
u : Set ι
uT : u ∈ T
A : Set ι := {a' | a' ∈ t ∧ ∀ (c : ι), c ∈ u → Disjoint (B a') (B c)}
Anonempty : Set.Nonempty A
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, c_1 ∈ insert a' u ∧ Set.Nonempty (B c ∩ B c_1) ∧ δ c ≤ τ * δ c_1
exact (hcb (H _ H')).elim