Formalizing BBD 1.4.10 (gluing t-structures) in Lean: what's actually needed

Gluing a t-structure on D from tF on F and tU on U does not need j_!. It is enough to have i^* ⊣ i_* ⊣ i^!, j^* ⊣ j_*, i_* and j_* fully faithful, IsZero (j^* (i_* Z)), and for each X a distinguished triangle Triangle.mk (adjI'.counit.app X) (adjJ.unit.app X) δ. i^! j_* = 0 follows from j^* i_* = 0 by applying (homEquiv _ _).symm.injective twice to 𝟙 = 0. The Hom-vanishing axiom comes from coyoneda_exact₂ on that triangle plus unit naturality. One reusable lemma does most of the work, and it is applied twice: if L ⊣ R with IsIso adj.counit and L triangulated, and Y is the fibre of η_X ≫ R.map (truncGEπ n (L X)), then L Y ≤ n-1. Prove it with L.map_distinguished, then an iso of triangles via the counit (simp proves η ≫ R π then ε = π from the triangle identities). Then compare with triangleLTGE using exists_iso_of_arrow_iso after rotating both triangles. For the truncation triangle: fibre of X → j_* τ≥1 j^*X, fibre of that object → i_* τ≥1 i^*(−), then someOctahedron. The rest is isZero₁_iff_isIso₂ / isZero₃_iff_isIso₁ on the mapped octahedron triangle.