Theorem: HTPI.Example_6_1_1 (HTPILib/Chap6.lean)

State before:
⊢ ∀ (n : ℕ), Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1
Tactic:
by_induc
State after:
case Base_Case

⊢ Sum i from 0 to 0, 2 ^ i = 2 ^ (0 + 1) - 1

case Induction_Step

⊢ ∀ (n : ℕ), Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1 → Sum i from 0 to n + 1, 2 ^ i = 2 ^ (n + 1 + 1) - 1

State before:
case Base_Case

⊢ Sum i from 0 to 0, 2 ^ i = 2 ^ (0 + 1) - 1
Tactic:
rewrite [sum_base]
State after:
case Base_Case

⊢ 2 ^ 0 = 2 ^ (0 + 1) - 1

State before:
case Base_Case

⊢ 2 ^ 0 = 2 ^ (0 + 1) - 1
Tactic:
rfl
State after:
no goals

State before:
case Induction_Step

⊢ ∀ (n : ℕ), Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1 → Sum i from 0 to n + 1, 2 ^ i = 2 ^ (n + 1 + 1) - 1
Tactic:
fix n : Nat
State after:
case Induction_Step
n : ℕ
⊢ Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1 → Sum i from 0 to n + 1, 2 ^ i = 2 ^ (n + 1 + 1) - 1

State before:
case Induction_Step
n : ℕ
⊢ Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1 → Sum i from 0 to n + 1, 2 ^ i = 2 ^ (n + 1 + 1) - 1
Tactic:
assume ih : Sum i from 0 to n, (2 : Int) ^ i =
    (2 : Int) ^ (n + 1) - (1 : Int)
State after:
case Induction_Step
n : ℕ
ih : Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1
⊢ Sum i from 0 to n + 1, 2 ^ i = 2 ^ (n + 1 + 1) - 1

State before:
case Induction_Step
n : ℕ
ih : Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1
⊢ Sum i from 0 to n + 1, 2 ^ i = 2 ^ (n + 1 + 1) - 1
Tactic:
show Sum i from 0 to n + 1, (2 : Int) ^ i =
    (2 : Int) ^ (n + 1 + 1) - (1 : Int) from
  calc Sum i from 0 to n + 1, (2 : Int) ^ i
    _ = (Sum i from 0 to n, (2 : Int) ^ i)
        + (2 : Int) ^ (n + 1) := by rw [sum_from_zero_step]
    _ = (2 : Int) ^ (n + 1) - (1 : Int)
        + (2 : Int) ^ (n + 1) := by rw [ih]
    _ = (2 : Int) ^ (n + 1 + 1) - (1 : Int) := by ring
State after:
no goals

State before:
n : ℕ
ih : Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1
⊢ Sum i from 0 to n + 1, 2 ^ i = (Sum i from 0 to n, 2 ^ i) + 2 ^ (n + 1)
Tactic:
rw [sum_from_zero_step]
State after:
no goals

State before:
n : ℕ
ih : Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1
⊢ (Sum i from 0 to n, 2 ^ i) + 2 ^ (n + 1) = 2 ^ (n + 1) - 1 + 2 ^ (n + 1)
Tactic:
rw [ih]
State after:
no goals

State before:
n : ℕ
ih : Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1
⊢ 2 ^ (n + 1) - 1 + 2 ^ (n + 1) = 2 ^ (n + 1 + 1) - 1
Tactic:
ring
State after:
no goals