have exists_unique := fun (p : ℕ) (hp : p ∈ n.primeFactors) =>
  (finMulAntidiagonal_exists_unique_prime_dvd hn
    (mem_primeFactors_iff_mem_factors.mp hp) t ht)
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
⊢ ∃ 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
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