Theorem: sumDrop_five (ListPowersProblem.lean)

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

State before:
case h
i : ℕ
⊢ sumDrop 5 pnats i = powers 5 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 => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * ((i + 1) * (i + 1))))

State before:
case h
i : ℕ
⊢ sum (fun i => sum (fun i => sum (fun i => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i)) i =
    (i + 1) * ((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 => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i)) Nat.zero =
    (Nat.zero + 1) * ((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 => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * ((i + 1) * (i + 1))))
⊢ sum (fun i => sum (fun i => sum (fun i => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i))
      (Nat.succ i) =
    (Nat.succ i + 1) * ((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 => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i)) Nat.zero =
    (Nat.zero + 1) * ((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 => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * ((i + 1) * (i + 1))))
⊢ sum (fun i => sum (fun i => sum (fun i => sum (fun i => i + i / 4 + 1) (i + i / 3)) (i + i / 2)) (i + i))
      (Nat.succ i) =
    (Nat.succ i + 1) * ((Nat.succ i + 1) * ((Nat.succ i + 1) * ((Nat.succ i + 1) * (Nat.succ i + 1))))
Tactic:
sorry
State after:
no goals