α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
⊢ False
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
⊢ Set.Nonempty
    {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
by_contra h
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
H : Function.Injective (index p)
⊢ False

case H
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
⊢ Function.Injective (index p)
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
⊢ False
suffices H : Function.Injective p.index
case H
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
⊢ Function.Injective (index p)
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
H : Function.Injective (index p)
⊢ False

case H
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
⊢ Function.Injective (index p)
exact not_injective_of_ordinal p.index H
case H
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
x y : Ordinal
hxy : index p x = index p y
⊢ x = y
case H
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
⊢ Function.Injective (index p)
intro x y hxy
case H.inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
x y : Ordinal
hxy : index p x = index p y
this : ∀ ⦃x y : Ordinal⦄, index p x = index p y → x ≤ y → x = y
x_le_y : ¬x ≤ y
⊢ x = y

α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
⊢ x = y
case H
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
x y : Ordinal
hxy : index p x = index p y
⊢ x = y
wlog x_le_y : x ≤ y generalizing x y
case inl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
x : Ordinal
hxy : index p x = index p x
x_le_y : x ≤ x
⊢ x = x

case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
⊢ x = y
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
⊢ x = y
rcases eq_or_lt_of_le x_le_y with (rfl | H)
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h :
  ∀ (x : Ordinal),
    ∃ x_1, ¬BallPackage.c p.toBallPackage x_1 ∈ iUnionUpTo p x ∧ R p x ≤ p.τ * BallPackage.r p.toBallPackage x_1
⊢ x = y
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
⊢ x = y
simp only [nonempty_def, not_exists, exists_prop, not_and, not_lt, not_le, mem_setOf_eq,
  not_forall] at h
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
⊢ x = y
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h :
  ∀ (x : Ordinal),
    ∃ x_1, ¬BallPackage.c p.toBallPackage x_1 ∈ iUnionUpTo p x ∧ R p x ≤ p.τ * BallPackage.r p.toBallPackage x_1
⊢ x = y
specialize h y
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
A : ¬BallPackage.c p.toBallPackage (index p y) ∈ iUnionUpTo p y
⊢ x = y
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
⊢ x = y
have A : p.c (p.index y) ∉ p.iUnionUpTo y := by
  have :
      p.index y =
        Classical.epsilon fun b : β => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b := by
    rw [TauPackage.index]; rfl
  rw [this]
  exact (Classical.epsilon_spec h).1
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
A :
  ∀ (x : Ordinal),
    x < y →
      ¬BallPackage.c p.toBallPackage (index p y) ∈
          ball (BallPackage.c p.toBallPackage (index p x)) (BallPackage.r p.toBallPackage (index p x))
⊢ x = y
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
A : ¬BallPackage.c p.toBallPackage (index p y) ∈ iUnionUpTo p y
⊢ x = y
simp only [iUnionUpTo, not_exists, exists_prop, mem_iUnion, mem_closedBall, not_and, not_le,
  Subtype.exists, Subtype.coe_mk] at A
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
A :
  ¬BallPackage.c p.toBallPackage (index p y) ∈
      ball (BallPackage.c p.toBallPackage (index p x)) (BallPackage.r p.toBallPackage (index p x))
⊢ x = y
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
A :
  ∀ (x : Ordinal),
    x < y →
      ¬BallPackage.c p.toBallPackage (index p y) ∈
          ball (BallPackage.c p.toBallPackage (index p x)) (BallPackage.r p.toBallPackage (index p x))
⊢ x = y
specialize A x H
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
A : BallPackage.r p.toBallPackage (index p y) ≤ 0
⊢ x = y
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
A :
  ¬BallPackage.c p.toBallPackage (index p y) ∈
      ball (BallPackage.c p.toBallPackage (index p x)) (BallPackage.r p.toBallPackage (index p x))
⊢ x = y
simp [hxy] at A
no goals
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
A : BallPackage.r p.toBallPackage (index p y) ≤ 0
⊢ x = y
exact (lt_irrefl _ ((p.rpos (p.index y)).trans_le A)).elim
no goals
case H.inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
x y : Ordinal
hxy : index p x = index p y
this : ∀ ⦃x y : Ordinal⦄, index p x = index p y → x ≤ y → x = y
x_le_y : ¬x ≤ y
⊢ x = y
exact (this hxy.symm (le_of_not_le x_le_y)).symm
no goals
case inl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty
      {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
x : Ordinal
hxy : index p x = index p x
x_le_y : x ≤ x
⊢ x = x
rfl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
this :
  index p y =
    Classical.epsilon fun b =>
      ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage b
⊢ ¬BallPackage.c p.toBallPackage (index p y) ∈ iUnionUpTo p y
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
⊢ ¬BallPackage.c p.toBallPackage (index p y) ∈ iUnionUpTo p y
have :
    p.index y =
      Classical.epsilon fun b : β => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b := by
  rw [TauPackage.index]; rfl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
this :
  index p y =
    Classical.epsilon fun b =>
      ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage b
⊢ ¬BallPackage.c p.toBallPackage
        (Classical.epsilon fun b =>
          ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage b) ∈
      iUnionUpTo p y
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
this :
  index p y =
    Classical.epsilon fun b =>
      ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage b
⊢ ¬BallPackage.c p.toBallPackage (index p y) ∈ iUnionUpTo p y
rw [this]
no goals
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
this :
  index p y =
    Classical.epsilon fun b =>
      ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage b
⊢ ¬BallPackage.c p.toBallPackage
        (Classical.epsilon fun b =>
          ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage b) ∈
      iUnionUpTo p y
exact (Classical.epsilon_spec h).1
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
⊢ (Classical.epsilon fun b =>
      (¬BallPackage.c p.toBallPackage b ∈
            ⋃ (j : { j // j < y }),
              ball (BallPackage.c p.toBallPackage (index p ↑j)) (BallPackage.r p.toBallPackage (index p ↑j))) ∧
        (⨆ (b :
            { b //
              ¬BallPackage.c p.toBallPackage b ∈
                  ⋃ (j : { j // j < y }),
                    ball (BallPackage.c p.toBallPackage (index p ↑j)) (BallPackage.r p.toBallPackage (index p ↑j)) }),
            BallPackage.r p.toBallPackage ↑b) ≤
          p.τ * BallPackage.r p.toBallPackage b) =
    Classical.epsilon fun b =>
      ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage b
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
⊢ index p y =
    Classical.epsilon fun b =>
      ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage b
rw [TauPackage.index]
no goals
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal
hxy : index p x = index p y
x_le_y : x ≤ y
H : x < y
h : ∃ x, ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage x
⊢ (Classical.epsilon fun b =>
      (¬BallPackage.c p.toBallPackage b ∈
            ⋃ (j : { j // j < y }),
              ball (BallPackage.c p.toBallPackage (index p ↑j)) (BallPackage.r p.toBallPackage (index p ↑j))) ∧
        (⨆ (b :
            { b //
              ¬BallPackage.c p.toBallPackage b ∈
                  ⋃ (j : { j // j < y }),
                    ball (BallPackage.c p.toBallPackage (index p ↑j)) (BallPackage.r p.toBallPackage (index p ↑j)) }),
            BallPackage.r p.toBallPackage ↑b) ≤
          p.τ * BallPackage.r p.toBallPackage b) =
    Classical.epsilon fun b =>
      ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p y ∧ R p y ≤ p.τ * BallPackage.r p.toBallPackage b
rfl