dsimp only [Nat.primeFactorsPiBij]
case h
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
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ Nat.primeFactorsPiBij d n f hf (f p hp) ≠ Nat.primeFactorsPiBij d n g hg (f p hp)
case h
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
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ∏ p ∈ filter (fun p_1 => f ↑p_1 ⋯ = f p hp) n.primeFactors.attach, ↑p ≠
    ∏ p ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp) n.primeFactors.attach, ↑p