lean_workbook_plus_62015

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Inductive step: $3^{2(k+1)+1}+2^{k+3}= 9(3^{2k+1} + 2^{k+2}) - 7(2^{k+2})$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_62015 (k : ℕ) : 3^(2 * (k + 1) + 1) + 2^(k + 3) = 9 * (3^(2 * k + 1) + 2^(k + 2)) - 7 * (2^(k + 2))   :=  by sorry

Source