-- Mathlib/MeasureTheory/Covering/Besicovitch.lean
theorem lastStep_nonempty :
    {i | ¬∃ b : β, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
this : p.index y = Classical.epsilon fun b => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b
⊢ p.c (p.index y) ∉ p.iUnionUpTo y

Tactic:
rw [this]

Result:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
this : p.index y = Classical.epsilon fun b => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b
⊢ p.c (Classical.epsilon fun b => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b) ∉ p.iUnionUpTo y

Proof state:
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
⊢ x = y

Tactic:
simp only [nonempty_def, not_exists, exists_prop, not_and, not_lt, not_le, mem_setOf_eq,
  not_forall] at h

Result:
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∀ (x : Ordinal.{u}), ∃ x_1, p.c x_1 ∉ p.iUnionUpTo x ∧ p.R x ≤ p.τ * p.r x_1
⊢ x = y

Proof state:
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
x y : Ordinal.{u}
hxy : p.index x = p.index y
this : ∀ ⦃x y : Ordinal.{u}⦄, p.index x = p.index y → x ≤ y → x = y
x_le_y : ¬x ≤ y
⊢ x = y

Tactic:
exact (this hxy.symm (le_of_not_le x_le_y)).symm

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
⊢ p.index y = Classical.epsilon fun b => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b

Tactic:
rw [TauPackage.index]

Result:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
⊢ (Classical.epsilon fun b => p.c b ∉ ⋃ j, ball (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∧ ⨆ b, p.r ↑b ≤ p.τ * p.r b) =
    Classical.epsilon fun b => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
⊢ Function.Injective p.index

Tactic:
intro x y hxy

Result:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
x y : Ordinal.{u}
hxy : p.index x = p.index y
⊢ x = y

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
⊢ p.c (p.index y) ∉ p.iUnionUpTo y

Tactic:
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

Result:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
this : p.index y = Classical.epsilon fun b => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b
⊢ p.c (p.index y) ∉ p.iUnionUpTo y

Proof state:
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
A : p.c (p.index y) ∉ ball (p.c (p.index x)) (p.r (p.index x))
⊢ x = y

Tactic:
simp? [hxy] at A says simp only [hxy, mem_ball, dist_self, not_lt] at A

Result:
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
A : p.r (p.index y) ≤ 0
⊢ x = y

Proof state:
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
A : p.r (p.index y) ≤ 0
⊢ x = y

Tactic:
exact (lt_irrefl _ ((p.rpos (p.index y)).trans_le A)).elim

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
x : Ordinal.{u}
hxy : p.index x = p.index x
x_le_y : x ≤ x
⊢ x = x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
⊢ {i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty

Tactic:
by_contra h

Result:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
⊢ False

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
⊢ False

Tactic:
suffices H : Function.Injective p.index from not_injective_of_ordinal p.index H

Result:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
⊢ Function.Injective p.index

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
x y : Ordinal.{u}
hxy : p.index x = p.index y
⊢ x = y

Tactic:
wlog x_le_y : x ≤ y generalizing x y

Result:
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
x y : Ordinal.{u}
hxy : p.index x = p.index y
this : ∀ ⦃x y : Ordinal.{u}⦄, p.index x = p.index y → x ≤ y → x = y
x_le_y : ¬x ≤ y
⊢ x = y

α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
⊢ x = y

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
this : p.index y = Classical.epsilon fun b => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b
⊢ p.c (Classical.epsilon fun b => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b) ∉ p.iUnionUpTo y

Tactic:
exact (Classical.epsilon_spec h).1

Result:
no goals