rw [mul_comm, (show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by aesop),  ← Nat.sq_sub_sq]
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
case succ
n : ℕ
hn : ∏ k ∈ range n, F k = F n - 2
⊢ (2 ^ 2 ^ n) ^ 2 - 1 ^ 2 = 2 ^ 2 ^ (n + 1) + 1 - 2