by_contra hij
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
⊢ j = i
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ False