α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
⊢ BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
⊢ BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
have A : ∀ z : β, p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep := by
  have : p.lastStep ∈ {i | ¬∃ b : β, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b} :=
    csInf_mem p.lastStep_nonempty
  simpa only [not_exists, mem_setOf_eq, not_and_or, not_le, not_not_mem]
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
⊢ False
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
⊢ BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
by_contra h
case inl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
⊢ False

case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
⊢ False
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
⊢ False
rcases A x with (H | H)
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
⊢ False
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
⊢ False
have Rpos : 0 < p.R p.lastStep := by
  apply lt_trans (mul_pos (_root_.zero_lt_one.trans p.one_lt_tau) (p.rpos _)) H
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
⊢ False
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
⊢ False
have B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep := by
  conv_rhs => rw [← one_mul (p.R p.lastStep)]
  exact mul_lt_mul (inv_lt_one p.one_lt_tau) le_rfl Rpos zero_le_one
case inr.intro.intro.inl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
y : β
hy1 : ¬BallPackage.c p.toBallPackage y ∈ iUnionUpTo p (lastStep p)
hy2 : p.τ⁻¹ * R p (lastStep p) < BallPackage.r p.toBallPackage y
Hy : BallPackage.c p.toBallPackage y ∈ iUnionUpTo p (lastStep p)
⊢ False

case inr.intro.intro.inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
y : β
hy1 : ¬BallPackage.c p.toBallPackage y ∈ iUnionUpTo p (lastStep p)
hy2 : p.τ⁻¹ * R p (lastStep p) < BallPackage.r p.toBallPackage y
Hy : p.τ * BallPackage.r p.toBallPackage y < R p (lastStep p)
⊢ False
case inr.intro.intro
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
y : β
hy1 : ¬BallPackage.c p.toBallPackage y ∈ iUnionUpTo p (lastStep p)
hy2 : p.τ⁻¹ * R p (lastStep p) < BallPackage.r p.toBallPackage y
⊢ False
rcases A y with (Hy | Hy)
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
this :
  lastStep p ∈
    {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
⊢ ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
⊢ ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
have : p.lastStep ∈ {i | ¬∃ b : β, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b} :=
  csInf_mem p.lastStep_nonempty
no goals
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
this :
  lastStep p ∈
    {i | ¬∃ b, ¬BallPackage.c p.toBallPackage b ∈ iUnionUpTo p i ∧ R p i ≤ p.τ * BallPackage.r p.toBallPackage b}
⊢ ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
simpa only [not_exists, mem_setOf_eq, not_and_or, not_le, not_not_mem]
no goals
case inl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
⊢ False
exact h H
no goals
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
⊢ 0 < R p (lastStep p)
apply lt_trans (mul_pos (_root_.zero_lt_one.trans p.one_lt_tau) (p.rpos _)) H
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
⊢ p.τ⁻¹ * R p (lastStep p) < 1 * R p (lastStep p)
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
⊢ p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
conv_rhs => rw [← one_mul (p.R p.lastStep)]
no goals
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
⊢ p.τ⁻¹ * R p (lastStep p) < 1 * R p (lastStep p)
exact mul_lt_mul (inv_lt_one p.one_lt_tau) le_rfl Rpos zero_le_one
case refine_2
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
this : ∃ a, (a ∈ range fun b => BallPackage.r p.toBallPackage ↑b) ∧ p.τ⁻¹ * R p (lastStep p) < a
⊢ ∃ y,
    ¬BallPackage.c p.toBallPackage y ∈ iUnionUpTo p (lastStep p) ∧
      p.τ⁻¹ * R p (lastStep p) < BallPackage.r p.toBallPackage y

case refine_1
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
⊢ Set.Nonempty (range fun b => BallPackage.r p.toBallPackage ↑b)
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
⊢ ∃ y,
    ¬BallPackage.c p.toBallPackage y ∈ iUnionUpTo p (lastStep p) ∧
      p.τ⁻¹ * R p (lastStep p) < BallPackage.r p.toBallPackage y
have := exists_lt_of_lt_csSup ?_ B
case refine_1
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
⊢ Set.Nonempty univ
case refine_1
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
⊢ Set.Nonempty (range fun b => BallPackage.r p.toBallPackage ↑b)
rw [← image_univ, nonempty_image_iff]
no goals
case refine_1
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
⊢ Set.Nonempty univ
exact ⟨⟨_, h⟩, mem_univ _⟩
no goals
case refine_2
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
this : ∃ a, (a ∈ range fun b => BallPackage.r p.toBallPackage ↑b) ∧ p.τ⁻¹ * R p (lastStep p) < a
⊢ ∃ y,
    ¬BallPackage.c p.toBallPackage y ∈ iUnionUpTo p (lastStep p) ∧
      p.τ⁻¹ * R p (lastStep p) < BallPackage.r p.toBallPackage y
simpa only [exists_prop, mem_range, exists_exists_and_eq_and, Subtype.exists,
Subtype.coe_mk]
no goals
case inr.intro.intro.inl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
y : β
hy1 : ¬BallPackage.c p.toBallPackage y ∈ iUnionUpTo p (lastStep p)
hy2 : p.τ⁻¹ * R p (lastStep p) < BallPackage.r p.toBallPackage y
Hy : BallPackage.c p.toBallPackage y ∈ iUnionUpTo p (lastStep p)
⊢ False
exact hy1 Hy
case inr.intro.intro.inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
y : β
hy1 : ¬BallPackage.c p.toBallPackage y ∈ iUnionUpTo p (lastStep p)
hy2 : R p (lastStep p) / p.τ < BallPackage.r p.toBallPackage y
Hy : p.τ * BallPackage.r p.toBallPackage y < R p (lastStep p)
⊢ False
case inr.intro.intro.inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
y : β
hy1 : ¬BallPackage.c p.toBallPackage y ∈ iUnionUpTo p (lastStep p)
hy2 : p.τ⁻¹ * R p (lastStep p) < BallPackage.r p.toBallPackage y
Hy : p.τ * BallPackage.r p.toBallPackage y < R p (lastStep p)
⊢ False
rw [← div_eq_inv_mul] at hy2
case inr.intro.intro.inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
y : β
hy1 : ¬BallPackage.c p.toBallPackage y ∈ iUnionUpTo p (lastStep p)
hy2 : R p (lastStep p) / p.τ < BallPackage.r p.toBallPackage y
Hy : p.τ * BallPackage.r p.toBallPackage y < R p (lastStep p)
this : R p (lastStep p) ≤ p.τ * BallPackage.r p.toBallPackage y
⊢ False
case inr.intro.intro.inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
y : β
hy1 : ¬BallPackage.c p.toBallPackage y ∈ iUnionUpTo p (lastStep p)
hy2 : R p (lastStep p) / p.τ < BallPackage.r p.toBallPackage y
Hy : p.τ * BallPackage.r p.toBallPackage y < R p (lastStep p)
⊢ False
have := (div_le_iff' (_root_.zero_lt_one.trans p.one_lt_tau)).1 hy2.le
no goals
case inr.intro.intro.inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A :
  ∀ (z : β),
    BallPackage.c p.toBallPackage z ∈ iUnionUpTo p (lastStep p) ∨
      p.τ * BallPackage.r p.toBallPackage z < R p (lastStep p)
h : ¬BallPackage.c p.toBallPackage x ∈ iUnionUpTo p (lastStep p)
H : p.τ * BallPackage.r p.toBallPackage x < R p (lastStep p)
Rpos : 0 < R p (lastStep p)
B : p.τ⁻¹ * R p (lastStep p) < R p (lastStep p)
y : β
hy1 : ¬BallPackage.c p.toBallPackage y ∈ iUnionUpTo p (lastStep p)
hy2 : R p (lastStep p) / p.τ < BallPackage.r p.toBallPackage y
Hy : p.τ * BallPackage.r p.toBallPackage y < R p (lastStep p)
this : R p (lastStep p) ≤ p.τ * BallPackage.r p.toBallPackage y
⊢ False
exact lt_irrefl _ (Hy.trans_le this)