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

State before:
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
⊢ Icc (nestedInterval U j).1 (nestedInterval U j).2 ⊆ Icc (nestedInterval U i).1 (nestedInterval U i).2
Tactic:
rw [(Nat.add_sub_of_le hij).symm]
State after:
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
⊢ Icc (nestedInterval U (i + (j - i))).1 (nestedInterval U (i + (j - i))).2 ⊆
    Icc (nestedInterval U i).1 (nestedInterval U i).2

State before:
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
⊢ Icc (nestedInterval U (i + (j - i))).1 (nestedInterval U (i + (j - i))).2 ⊆
    Icc (nestedInterval U i).1 (nestedInterval U i).2
Tactic:
set k := j - i
State after:
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
k : ℕ := j - i
⊢ Icc (nestedInterval U (i + k)).1 (nestedInterval U (i + k)).2 ⊆ Icc (nestedInterval U i).1 (nestedInterval U i).2

State before:
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
k : ℕ := j - i
⊢ Icc (nestedInterval U (i + k)).1 (nestedInterval U (i + k)).2 ⊆ Icc (nestedInterval U i).1 (nestedInterval U i).2
Tactic:
induction k with
| zero => apply rfl.subset
| succ k ih => intro x hx; apply ih (nestedIntervalSeq_is_nested_succ U (i + k) hx)
State after:
no goals

State before:
case zero
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
k : ℕ := j - i
⊢ Icc (nestedInterval U (i + Nat.zero)).1 (nestedInterval U (i + Nat.zero)).2 ⊆
    Icc (nestedInterval U i).1 (nestedInterval U i).2
Tactic:
apply rfl.subset
State after:
no goals

State before:
case succ
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
k✝ : ℕ := j - i
k : ℕ
ih : Icc (nestedInterval U (i + k)).1 (nestedInterval U (i + k)).2 ⊆ Icc (nestedInterval U i).1 (nestedInterval U i).2
⊢ Icc (nestedInterval U (i + Nat.succ k)).1 (nestedInterval U (i + Nat.succ k)).2 ⊆
    Icc (nestedInterval U i).1 (nestedInterval U i).2
Tactic:
intro x hx
State after:
case succ
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
k✝ : ℕ := j - i
k : ℕ
ih : Icc (nestedInterval U (i + k)).1 (nestedInterval U (i + k)).2 ⊆ Icc (nestedInterval U i).1 (nestedInterval U i).2
x : ℝ
hx : x ∈ Icc (nestedInterval U (i + Nat.succ k)).1 (nestedInterval U (i + Nat.succ k)).2
⊢ x ∈ Icc (nestedInterval U i).1 (nestedInterval U i).2

State before:
case succ
ι : Type
U : ι → Set ℝ
i j : ℕ
hij : i ≤ j
k✝ : ℕ := j - i
k : ℕ
ih : Icc (nestedInterval U (i + k)).1 (nestedInterval U (i + k)).2 ⊆ Icc (nestedInterval U i).1 (nestedInterval U i).2
x : ℝ
hx : x ∈ Icc (nestedInterval U (i + Nat.succ k)).1 (nestedInterval U (i + Nat.succ k)).2
⊢ x ∈ Icc (nestedInterval U i).1 (nestedInterval U i).2
Tactic:
apply ih (nestedIntervalSeq_is_nested_succ U (i + k) hx)
State after:
no goals