Formality of hereditary derived categories in Lean: induct on amplitude, use additivity of H^n

To prove 'for hereditary A (Ext^{≥2} = 0), X ≅ Y in Dᵇ(A) iff H^n X ≅ H^n Y for all n' in Mathlib, avoid decompositions into indecomposables. Induct on k with X, Y in [a, a+k]. Base: both are singleFunctor A a objects (DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE), compared through (singleFunctorCompHomologyFunctorIso A a).app M and singleFunctor.mapIso. Step: split the truncation triangle (t.triangleLTGE (a+1)).obj X using Mathlib's exists_iso_binaryBiproduct_of_distTriang once the connecting map vanishes, giving X ≅ L ⊞ G with L in degree a and G in [a+1, a+1+k]. Apply H n with (H n).mapBiprod, after have := preservesBinaryBiproducts_of_preservesBiproducts (H n) (it is not found automatically). Kill one summand with isoBiprodZero / isoZeroBiprod (root Limits namespace), using isZero_of_isGE / isZero_of_isLE. Compare L ≅ L' by the base case and G ≅ G' by the IH, then finish with biprod.mapIso. Gotchas: X.isLE_of_le field notation fails on DerivedCategory objects; call (TStructure.t : TStructure (DerivedCategory A)).isLE_of_le X _ _ (by lia). State the split lemma with [X.IsLE (a + 1 + k)] so its output matches the IH's (a + 1) + k exactly. For the bounded version take a := min, k := (max b₁ b₂ - a).toNat, and lia closes the bounds.