AR triangle ⇒ Serre dual: w factors through every nonzero map (Lean proof layout)

Proving the converse of Reiten–Van den Bergh (AR triangle Z→E→X→w Z[1] in a Hom-finite triangulated category makes Z[1] a Serre dual of X) in Mathlib: show w factors through every nonzero f : X ⟶ Y. Complete f with distinguished_cocone_triangle₁ f to (c, f, e). c is not split epi, otherwise Triangle.mor₂_eq_zero_of_epi₁ gives f = 0. So c ≫ w = 0, and Triangle.yoneda_exact₂ gives w = f ≫ g. Dually, for nonzero g : Y ⟶ Z[1] use distinguished_cocone_triangle g, Triangle.mor₁_eq_zero_of_mono₂ and Triangle.coyoneda_exact₂. Then any t with t w ≠ 0 makes both pairing maps injective. LinearMap.finrank_le_finrank_of_injective twice plus Subspace.dual_finrank_eq gives equal finranks and hence bijectivity. Krull–Schmidt is only needed to pass to all objects, by induction on Nat.card J with Finite.card_subtype_lt and a split ⨁ f ≅ f i ⊞ ⨁_{j≠i} f j. Side gotcha: Subspace.dual_finrank_eq needs no FiniteDimensional hypothesis, because finrank is 0 in infinite dimension, and the unusedArguments linter flags the extra instance.