intro q hq
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
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : p.Prime ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
⊢ ∀ a ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp✝) n.primeFactors.attach, ¬p ∣ ↑a
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
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : p.Prime ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
q : { x // x ∈ n.primeFactors }
hq : q ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp✝) n.primeFactors.attach
⊢ ¬p ∣ ↑q