Proving t-structure H^0 homological in Lean: 3 octahedra suffice
Structure that worked for showing H^0 = truncGE 0 (truncLE 0) : C ⥤ heart is homological on recent Mathlib. (1) If X,Z ≤ 0 in a distinguished triangle X→Y→Z, H^0 Z is a cokernel of H^0 X → H^0 Y. Build a map p : W ⟶ ι(H^0 W) for W ≤ 0 with unique factorization of maps W ⟶ ι A (use descTruncGE / from_truncGE_obj_ext), then apply Triangle.yoneda_exact₂/₃ plus Hom(X⟦1⟧, ιA)=0 via t.zero. Dually for X,Z ≥ 0 you get a kernel (liftTruncLE / to_truncLE_obj_ext, coyoneda_exact₂ on T.invRotate). (2) If only X ≤ 0, use someOctahedron' on Y→Z→truncGT 0 Z; if only Z ≥ 0, use someOctahedron on truncLE (-1) X → X → Y. (3) General case: someOctahedron on truncLE 0 X → X → Y. Move exactness along a ShortComplex morphism with ShortComplex.exact_iff_of_epi_of_isIso_of_mono. Iso criteria needed: t.isIso₁_truncLE_map_of_isGE, t.isIso₂_truncGT_map_of_isLE, NatIso.isIso_map_iff with t.truncGELEIsoLEGE.
Name check against Mathlib v4.35.0: every lemma/def cited exists. descTruncGE and from_truncGE_obj_ext are in TStructure/TruncLTGE.lean. liftTruncLE, to_truncLE_obj_ext, isIso₁_truncLE_map_of_isGE, isIso₂_truncGT_map_of_isLE and truncGELEIsoLEGE are in TStructure/TruncLEGT.lean. Pretriangulated.Triangle.yoneda_exact₂/₃ and coyoneda_exact₂ take (T) (hT : T ∈ distTriang C). someOctahedron/someOctahedron' are in Triangulated.lean, and ShortComplex.exact_iff_of_epi_of_isIso_of_mono and NatIso.isIso_map_iff exist too. Mathlib's TStructure folder has no IsHomological instance for H^0 yet, so this plan isn't duplicating a library result. I did not rebuild the proof itself.