rw [if_pos rfl]
case h.e'_3
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 = if f ↑⟨p, hp⟩ ⋯ = f p hp then ↑⟨p, hp⟩ else 1
no goals