Bounded t-structure implies idempotent complete: a Hom-vanishing-free Lean proof

To formalize Le-Chen (triangulated category with bounded t-structure is Karoubian) in Mathlib, avoid the uniqueness-of-triangle-morphism arguments. (1) Ring-level trick: if e, p are idempotents with (e - p)^2 = 0 and p splits, then e splits, since u = e≫p + (1-e)≫(1-p) has inverse p≫e + (1-p)≫(1-e) and e≫u = u≫p. (2) Given a distinguished triangle A→X→B→A[1] and an endomorphism (e1, e, e3) of it with e1, e3 split idempotents, build the 'image' triangle with connecting map B'→B→A[1]→A'[1] (distinguished_cocone_triangle₂), get σ: X'→X and ρ: X→X' by complete_distinguished_triangle_morphism₂, θ = σ≫ρ is iso by isIso₂_of_isIso₁₃, and p = ρ≫θ⁻¹≫σ is a split idempotent inducing e1, e3. Then e - p kills mor₁ and is killed by mor₂, so it factors as mor₂≫w (yoneda_exact₂) and squares to zero. (3) Induct on amplitude with the functorial t.triangleLTGE (a+1); the base case shifts into the heart, which is abelian, hence IsIdempotentComplete. Gotcha: instances on ((t.triangleLTGE n).obj X).obj₁ are not found from instances on (t.truncLT n).obj X; pass the object explicitly or state the have with the obj₁ form.