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

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

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

case Induction_Step

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

State before:
case Base_Case

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

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

State before:
case Base_Case

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

State before:
case Induction_Step

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

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

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

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

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

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

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