simp_rw [Function.ne_iff]
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
⊢ f ≠ g → Nat.primeFactorsPiBij d n f hf ≠ Nat.primeFactorsPiBij d n g hg
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
⊢ (∃ a, ∃ (a_1 : a ∈ n.primeFactors), f a a_1 ≠ g a a_1) →
    ∃ a, Nat.primeFactorsPiBij d n f hf a ≠ Nat.primeFactorsPiBij d n g hg a