Lean/Mathlib: Euler characteristic of Hom along a distinguished triangle without building the long exact sequence

To prove χ(E, -) = Σₙ (-1)ⁿ dim Hom(E⟦n⟧, -) is additive on a distinguished triangle X →f Y →g Z →h X⟦1⟧, don't assemble the LES as a ℤ-indexed complex. Instead: (1) one generic lemma per triangle T: dim Hom(W, T.obj₂) = rank(T.mor₁ ∘ -) + rank(T.mor₂ ∘ -), from LinearMap.finrank_range_add_finrank_ker (Linear.rightComp k W T.mor₂) plus ker = range via Triangle.coyoneda_exact₂ and comp_distTriang_mor_zero₁₂. Apply it to T, rot T and rot rot T (state the expected type explicitly with have h : finrank (W ⟶ X⟦1⟧) = r T.mor₃ + r (-T.mor₁⟦1⟧') := lemma _ (rot_of_distTriang _ (rot_of_distTriang _ hT)) W — rewriting inside T.rotate.rotate.mor₂ fails). (2) Rank invariances via one lemma: if g ∘ A = B ∘ f with A, B linear equivs then finrank (range g) = finrank (range f) (LinearMap.range_comp_of_range_eq_top, LinearMap.range_comp, LinearEquiv.finrank_map_eq); this gives rank(-φ)=rank φ, invariance under W ≅ W', and rank(φ⟦1⟧ ∘ -) on Hom(W⟦1⟧, -) = rank(φ ∘ -) on Hom(W, -). (3) Then dim Hom(E⟦n⟧,X) = r_h(n+1) + r_f(n), and the alternating sum telescopes: conv_rhs => rw [← finsum_comp_equiv (Equiv.addRight (1 : ℤ))] + Int.negOnePow_succ; finite supports via bounds r ≤ dim. For K₀ bases over ℤ: Matrix.det_of_isUpperTriangular + Matrix.linearIndependent_cols_of_isUnit + LinearIndependent.of_comp (Basis is Module.Basis now).