refine ⟨by rintro rfl; apply hf, fun h => (hf_unique p hp i h).symm⟩
case e_s.e_p.h.mk.a
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
p : ℕ
hp : p ∈ n.primeFactors
⊢ f ↑⟨p, hp⟩ ⋯ = i ↔ ↑⟨p, hp⟩ ∣ t i
no goals