[GOAL]
n k : ℕ
⊢ List.toFinset (factors (n ^ (k + 1))) = List.toFinset (factors n)
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
k : ℕ
⊢ List.toFinset (factors (0 ^ (k + 1))) = List.toFinset (factors 0)
[PROOFSTEP]
simp
[GOAL]
case inr
n k : ℕ
hn : n ≠ 0
⊢ List.toFinset (factors (n ^ (k + 1))) = List.toFinset (factors n)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case inr.zero
n : ℕ
hn : n ≠ 0
⊢ List.toFinset (factors (n ^ (zero + 1))) = List.toFinset (factors n)
[PROOFSTEP]
simp
[GOAL]
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)
[PROOFSTEP]
rw [pow_succ', factors_mul_toFinset hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]
[GOAL]
n k : ℕ
hk : k ≠ 0
⊢ List.toFinset (factors (n ^ k)) = List.toFinset (factors n)
[PROOFSTEP]
cases k
[GOAL]
case zero
n : ℕ
hk : zero ≠ 0
⊢ List.toFinset (factors (n ^ zero)) = List.toFinset (factors n)
[PROOFSTEP]
simp at hk 
[GOAL]
case succ
n n✝ : ℕ
hk : succ n✝ ≠ 0
⊢ List.toFinset (factors (n ^ succ n✝)) = List.toFinset (factors n)
[PROOFSTEP]
rw [pow_succ_factors_toFinset]
[GOAL]
p k : ℕ
hk : k ≠ 0
hp : Prime p
⊢ List.toFinset (factors (p ^ k)) = {p}
[PROOFSTEP]
simp [pow_factors_toFinset p hk, factors_prime hp]
