choose f hf hf_unique using exists_unique
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
exists_unique : ∀ p ∈ n.primeFactors, ∃! i, p ∣ t i
⊢ ∃ g, ∃ (hg : g ∈ n.primeFactors.pi fun x => univ), Nat.primeFactorsPiBij d n g hg = t
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
⊢ ∃ g, ∃ (hg : g ∈ n.primeFactors.pi fun x => univ), Nat.primeFactorsPiBij d n g hg = t