Theorem: Tutorial.nestedInterval_not_HasFinSubCover (Solution/Advanced/Analysis/Lecture3.lean)

State before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
⊢ ¬HasFinSubCover U (Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2)
Tactic:
by_cases H : HasFinSubCover U (Icc (α n) ((α n + β n) / 2))
State after:
case pos
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U (Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2)

case neg
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : ¬HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U (Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2)

State before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U (Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2)
Tactic:
case pos =>
  rw [nestedInterval, nestedIntervalSucc_right H]
  apply not_HasFinSubCover_concat ?_ H
  apply nestedInterval_not_HasFinSubCover h n
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : ¬HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U (Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2)
Tactic:
case neg =>
  rw [nestedInterval, nestedIntervalSucc_left H]
  apply H
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U (Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2)
Tactic:
rw [nestedInterval, nestedIntervalSucc_right H]
State after:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U
      (Icc (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).1
        (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).2)

State before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U
      (Icc (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).1
        (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).2)
Tactic:
apply not_HasFinSubCover_concat ?_ H
State after:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U
      (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).2)

State before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U
      (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).2)
Tactic:
apply nestedInterval_not_HasFinSubCover h n
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : ¬HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U (Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2)
Tactic:
rw [nestedInterval, nestedIntervalSucc_left H]
State after:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : ¬HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U
      (Icc ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).1
        ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).2)

State before:
ι : Type
U : ι → Set ℝ
h : ¬HasFinSubCover U (Icc (nestedInterval U 0).1 (nestedInterval U 0).2)
n : ℕ
H : ¬HasFinSubCover U (Icc (nestedInterval U n).1 (((nestedInterval U n).1 + (nestedInterval U n).2) / 2))
⊢ ¬HasFinSubCover U
      (Icc ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).1
        ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).2)
Tactic:
apply H
State after:
no goals