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

State before:
ι : Type
U : ι → Set ℝ
⊢ (nestedInterval U 0).2 - (nestedInterval U 0).1 = (2 ^ 0)⁻¹
Tactic:
simp [nestedInterval]
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
⊢ (nestedInterval U (n + 1)).2 - (nestedInterval U (n + 1)).1 = (2 ^ (n + 1))⁻¹
Tactic:
have ih := nestedInterval_len n
State after:
ι : Type
U : ι → Set ℝ
n : ℕ
ih : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
⊢ (nestedInterval U (n + 1)).2 - (nestedInterval U (n + 1)).1 = (2 ^ (n + 1))⁻¹

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
ih : (nestedInterval U n).2 - (nestedInterval U n).1 = (2 ^ n)⁻¹
⊢ (nestedInterval U (n + 1)).2 - (nestedInterval U (n + 1)).1 = (2 ^ (n + 1))⁻¹
Tactic:
rcases nestedIntervalSucc_eq_or_eq U (α n) (β n) with H | H <;>
  rw [nestedInterval, H] <;> field_simp at ih ⊢ <;>
    calc _ = (β n - α n) * 2 ^ n * 2 := by ring
         _ = 2                       := by rw [ih]; ring
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
H :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
ih : ((nestedInterval U n).2 - (nestedInterval U n).1) * 2 ^ n = 1
⊢ ((nestedInterval U n).2 * 2 - ((nestedInterval U n).1 + (nestedInterval U n).2)) * 2 ^ (n + 1) =
    ((nestedInterval U n).2 - (nestedInterval U n).1) * 2 ^ n * 2
Tactic:
ring
State after:
no goals

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
H :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
ih : ((nestedInterval U n).2 - (nestedInterval U n).1) * 2 ^ n = 1
⊢ ((nestedInterval U n).2 - (nestedInterval U n).1) * 2 ^ n * 2 = 2
Tactic:
rw [ih]
State after:
ι : Type
U : ι → Set ℝ
n : ℕ
H :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
ih : ((nestedInterval U n).2 - (nestedInterval U n).1) * 2 ^ n = 1
⊢ 1 * 2 = 2

State before:
ι : Type
U : ι → Set ℝ
n : ℕ
H :
  nestedIntervalSucc U (nestedInterval U n).1 (nestedInterval U n).2 =
    (((nestedInterval U n).1 + (nestedInterval U n).2) / 2, (nestedInterval U n).2)
ih : ((nestedInterval U n).2 - (nestedInterval U n).1) * 2 ^ n = 1
⊢ 1 * 2 = 2
Tactic:
ring
State after:
no goals