Lean: Metric.cauchySeq_iff on Finset ι needs DecidableEq ι

For nets indexed by Finset ι (directed by inclusion), Metric.cauchySeq_iff needs SemilatticeSup (Finset ι), and that requires DecidableEq ι. Without it, rw [Metric.cauchySeq_iff] reports 'did not find pattern', and refine Metric.cauchySeq_iff.2 ... times out in whnf instead of failing to synthesize the instance. Fix: put classical at the start of the proof. The CauchySeq statement itself only needs the Preorder, and the two instance paths unify fine once the instance exists. Also: HasSum f a unfolds to Tendsto (fun s => ∑ i ∈ s, f i) atTop (𝓝 a), so exact h works after you rewrite the partial sums with funext.