Theorem: sumDrop_four (ListPowersProblem.lean)

State before:
⊢ sumDrop 4 pnats = powers 4
Tactic:
funext i
State after:
case h
i : ℕ
⊢ sumDrop 4 pnats i = powers 4 i

State before:
case h
i : ℕ
⊢ sumDrop 4 pnats i = powers 4 i
Tactic:
simp only [sumDrop, powers, pow_succ, pow_zero, mul_one, 
  dropEveryNth_eq_fun, pnats, Nat.div_one
]
State after:
case h
i : ℕ
⊢ sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * (i + 1)))

State before:
case h
i : ℕ
⊢ sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * (i + 1)))
Tactic:
induction' i with i ih
State after:
case h.zero

⊢ sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) Nat.zero =
    (Nat.zero + 1) * ((Nat.zero + 1) * ((Nat.zero + 1) * (Nat.zero + 1)))

case h.succ
i : ℕ
ih :
  sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * (i + 1)))
⊢ sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) (Nat.succ i) =
    (Nat.succ i + 1) * ((Nat.succ i + 1) * ((Nat.succ i + 1) * (Nat.succ i + 1)))

State before:
case h.zero

⊢ sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) Nat.zero =
    (Nat.zero + 1) * ((Nat.zero + 1) * ((Nat.zero + 1) * (Nat.zero + 1)))
Tactic:
rfl
State after:
no goals

State before:
case h.succ
i : ℕ
ih :
  sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * (i + 1)))
⊢ sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) (Nat.succ i) =
    (Nat.succ i + 1) * ((Nat.succ i + 1) * ((Nat.succ i + 1) * (Nat.succ i + 1)))
Tactic:
sorry
State after:
no goals