n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := length (factors n)
⊢ n = p ^ k
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
⊢ n = p ^ length (factors n)
set k := n.factors.length
no goals
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := length (factors n)
⊢ n = p ^ k
rw [← prod_factors hpos, ← prod_replicate k p,
  eq_replicate_of_mem fun d hd => h (prime_of_mem_factors hd) (dvd_of_mem_factors hd)]