case zero
n : ℕ
hk : zero ≠ 0
⊢ List.toFinset (factors (n ^ zero)) = List.toFinset (factors n)

case succ
n n✝ : ℕ
hk : succ n✝ ≠ 0
⊢ List.toFinset (factors (n ^ succ n✝)) = List.toFinset (factors n)
n k : ℕ
hk : k ≠ 0
⊢ List.toFinset (factors (n ^ k)) = List.toFinset (factors n)
cases k
no goals
case succ
n n✝ : ℕ
hk : succ n✝ ≠ 0
⊢ List.toFinset (factors (n ^ succ n✝)) = List.toFinset (factors n)
rw [pow_succ_factors_toFinset]
no goals
case zero
n : ℕ
hk : zero ≠ 0
⊢ List.toFinset (factors (n ^ zero)) = List.toFinset (factors n)
simp at hk