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

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
⊢ Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2 ⊆ Icc (nestedInterval U n).1 (nestedInterval U n).2
Tactic:
have := nestedInterval_le U n
State after:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
⊢ Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2 ⊆ Icc (nestedInterval U n).1 (nestedInterval U n).2

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
⊢ Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2 ⊆ Icc (nestedInterval U n).1 (nestedInterval U n).2
Tactic:
cases nestedIntervalSucc_eq_or_eq U (α n) (β n) with
| inl h =>
  apply Icc_subset_Icc (by rw [nestedInterval, h]) (by rw [nestedInterval, h]; dsimp only; linarith)
| inr h =>
  apply Icc_subset_Icc (by rw [nestedInterval, h]; dsimp only; linarith) (by rw [nestedInterval, h])
State after:
no goals

State before:
case inl
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2 ⊆ Icc (nestedInterval U n).1 (nestedInterval U n).2
Tactic:
apply Icc_subset_Icc (by rw [nestedInterval, h]) (by rw [nestedInterval, h]; dsimp only; linarith)
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ (nestedInterval U n).1 ≤ (nestedInterval U (n + 1)).1
Tactic:
rw [nestedInterval, h]
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ (nestedInterval U (n + 1)).2 ≤ (nestedInterval U n).2
Tactic:
rw [nestedInterval, h]
State after:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).2 ≤ (nestedInterval U n).2

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2).2 ≤ (nestedInterval U n).2
Tactic:
dsimp only
State after:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ≤ (nestedInterval U n).2

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    ((nestedInterval U n).1, ((nestedInterval U n).1 + (nestedInterval U n).2) / 2)
⊢ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 ≤ (nestedInterval U n).2
Tactic:
linarith
State after:
no goals

State before:
case inr
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ Icc (nestedInterval U (n + 1)).1 (nestedInterval U (n + 1)).2 ⊆ Icc (nestedInterval U n).1 (nestedInterval U n).2
Tactic:
apply Icc_subset_Icc (by rw [nestedInterval, h]; dsimp only; linarith) (by rw [nestedInterval, h])
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (nestedInterval U n).1 ≤ (nestedInterval U (n + 1)).1
Tactic:
rw [nestedInterval, h]
State after:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (nestedInterval U n).1 ≤ (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).1

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (nestedInterval U n).1 ≤ (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2).1
Tactic:
dsimp only
State after:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (nestedInterval U n).1 ≤ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (nestedInterval U n).1 ≤ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2
Tactic:
linarith
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
h :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
⊢ (nestedInterval U (n + 1)).2 ≤ (nestedInterval U n).2
Tactic:
rw [nestedInterval, h]
State after:
no goals