case intro.intro.intro.intro
R : Type ?u.14
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Prime p
hk : 0 < k
⊢ Nat.minFac (p ^ k) ^ ↑(Nat.factorization (p ^ k)) (Nat.minFac (p ^ k)) = p ^ k
R : Type ?u.14
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
hn : IsPrimePow n
⊢ Nat.minFac n ^ ↑(Nat.factorization n) (Nat.minFac n) = n
obtain ⟨p, k, hp, hk, rfl⟩ := hn
case intro.intro.intro.intro
R : Type ?u.14
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ Nat.minFac (p ^ k) ^ ↑(Nat.factorization (p ^ k)) (Nat.minFac (p ^ k)) = p ^ k
case intro.intro.intro.intro
R : Type ?u.14
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Prime p
hk : 0 < k
⊢ Nat.minFac (p ^ k) ^ ↑(Nat.factorization (p ^ k)) (Nat.minFac (p ^ k)) = p ^ k
rw [← Nat.prime_iff] at hp
no goals
case intro.intro.intro.intro
R : Type ?u.14
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ Nat.minFac (p ^ k) ^ ↑(Nat.factorization (p ^ k)) (Nat.minFac (p ^ k)) = p ^ k
rw [hp.pow_minFac hk.ne', hp.factorization_pow, Finsupp.single_eq_same]