Theorem: fermat_product (FormalBook/Chapter_01.lean)

State before:
n : ℕ
⊢ ∏ k ∈ range n, F k = F n - 2
Tactic:
induction' n with n hn
State after:
case zero

⊢ ∏ k ∈ range 0, F k = F 0 - 2

case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ ∏ k ∈ range (n + 1), F k = F (n + 1) - 2

State before:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ ∏ k ∈ range (n + 1), F k = F (n + 1) - 2
Tactic:
rw [prod_range_succ, hn]
State after:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (F n - 2) * F n = F (n + 1) - 2

State before:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (F n - 2) * F n = F (n + 1) - 2
Tactic:
unfold F
State after:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (2 ^ 2 ^ n + 1 - 2) * (2 ^ 2 ^ n + 1) = 2 ^ 2 ^ (n + 1) + 1 - 2

State before:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (2 ^ 2 ^ n + 1 - 2) * (2 ^ 2 ^ n + 1) = 2 ^ 2 ^ (n + 1) + 1 - 2
Tactic:
rw [mul_comm, (show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by aesop),  ← Nat.sq_sub_sq]
State after:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (2 ^ 2 ^ n) ^ 2 - 1 ^ 2 = 2 ^ 2 ^ (n + 1) + 1 - 2

State before:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (2 ^ 2 ^ n) ^ 2 - 1 ^ 2 = 2 ^ 2 ^ (n + 1) + 1 - 2
Tactic:
ring_nf
State after:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ 2 ^ (2 ^ n * 2) - 1 = 1 + 2 ^ (2 ^ n * 2) - 2

State before:
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ 2 ^ (2 ^ n * 2) - 1 = 1 + 2 ^ (2 ^ n * 2) - 2
Tactic:
omega
State after:
no goals

State before:
case zero

⊢ ∏ k ∈ range 0, F k = F 0 - 2
Tactic:
trivial
State after:
no goals

State before:
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1
Tactic:
aesop
State after:
no goals