exact hfg rfl
case h.a
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
q : { x // x ∈ n.primeFactors }
hp✝ : ↑q ∈ n.primeFactors
hp : (↑q).Prime ∧ ↑q ∣ n ∧ n ≠ 0
hfg : f (↑q) hp✝ ≠ f (↑q) hp✝
hq : q ∈ filter (fun p => g ↑p ⋯ = f (↑q) hp✝) n.primeFactors.attach
⊢ False
no goals