case inl
k : ℕ
⊢ List.toFinset (factors (0 ^ (k + 1))) = List.toFinset (factors 0)

case inr
n k : ℕ
hn : n ≠ 0
⊢ List.toFinset (factors (n ^ (k + 1))) = List.toFinset (factors n)
n k : ℕ
⊢ List.toFinset (factors (n ^ (k + 1))) = List.toFinset (factors n)
rcases eq_or_ne n 0 with (rfl | hn)
case inr.zero
n : ℕ
hn : n ≠ 0
⊢ List.toFinset (factors (n ^ (zero + 1))) = List.toFinset (factors n)

case inr.succ
n : ℕ
hn : n ≠ 0
k : ℕ
ih : List.toFinset (factors (n ^ (k + 1))) = List.toFinset (factors n)
⊢ List.toFinset (factors (n ^ (succ k + 1))) = List.toFinset (factors n)
case inr
n k : ℕ
hn : n ≠ 0
⊢ List.toFinset (factors (n ^ (k + 1))) = List.toFinset (factors n)
induction' k with k ih
no goals
case inl
k : ℕ
⊢ List.toFinset (factors (0 ^ (k + 1))) = List.toFinset (factors 0)
simp
no goals
case inr.zero
n : ℕ
hn : n ≠ 0
⊢ List.toFinset (factors (n ^ (zero + 1))) = List.toFinset (factors n)
simp
no goals
case inr.succ
n : ℕ
hn : n ≠ 0
k : ℕ
ih : List.toFinset (factors (n ^ (k + 1))) = List.toFinset (factors n)
⊢ List.toFinset (factors (n ^ (succ k + 1))) = List.toFinset (factors n)
rw [pow_succ', factors_mul_toFinset hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]