case inl
k : ℕ
hk : k ≠ 0
⊢ minFac (1 ^ k) = minFac 1

case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
⊢ minFac (n ^ k) = minFac n
n k : ℕ
hk : k ≠ 0
⊢ minFac (n ^ k) = minFac n
rcases eq_or_ne n 1 with (rfl | hn)
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ minFac (n ^ k) = minFac n
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
⊢ minFac (n ^ k) = minFac n
have hnk : n ^ k ≠ 1 := fun hk' => hn ((pow_eq_one_iff hk).1 hk')
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ minFac n ≤ minFac (n ^ k)
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ minFac (n ^ k) = minFac n
apply (minFac_le_of_dvd (minFac_prime hn).two_le ((minFac_dvd n).pow hk)).antisymm
no goals
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ minFac n ≤ minFac (n ^ k)
apply
  minFac_le_of_dvd (minFac_prime hnk).two_le
    ((minFac_prime hnk).dvd_of_dvd_pow (minFac_dvd _))
no goals
case inl
k : ℕ
hk : k ≠ 0
⊢ minFac (1 ^ k) = minFac 1
simp