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

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

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
this : (nestedInterval U n).1 < (nestedInterval U n).2
⊢ (nestedInterval U (n + 1)).1 < (nestedInterval U (n + 1)).2
Tactic:
cases nestedIntervalSucc_eq_or_eq U (α n) (β n) with
| inl h => rw [nestedInterval, h]; dsimp only; linarith
| inr h => rw [nestedInterval, h]; dsimp only; linarith
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)
⊢ (nestedInterval U (n + 1)).1 < (nestedInterval U (n + 1)).2
Tactic:
rw [nestedInterval, h]
State after:
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)
⊢ ((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:
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)
⊢ ((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:
dsimp only
State after:
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)
⊢ (nestedInterval U n).1 < ((nestedInterval U n).1 + (nestedInterval U n).2) / 2

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)
⊢ (nestedInterval U n).1 < ((nestedInterval U n).1 + (nestedInterval U n).2) / 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)
⊢ (nestedInterval U (n + 1)).1 < (nestedInterval U (n + 1)).2
Tactic:
rw [nestedInterval, h]
State after:
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)
⊢ (((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:
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)
⊢ (((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:
dsimp only
State after:
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)
⊢ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 < (nestedInterval U n).2

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)
⊢ ((nestedInterval U n).1 + (nestedInterval U n).2) / 2 < (nestedInterval U n).2
Tactic:
linarith
State after:
no goals