refine ⟨i, hi, ?_⟩
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
⊢ ∃! i, p ∣ f 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
⊢ ∀ (y : Fin d), (fun i => p ∣ f i) y → y = i