Lean/Mathlib triangulated: glue two triangles into an extension with someOctahedron' (fiber form)

Pattern for iterated semiorthogonal decompositions / filtrations: given distinguished triangles Y₁ →f₁ X →g₁ Z₁ →h₁ Y₁⟦1⟧ and Y₂ →f₂ Z₁ →g₂ Z₂ →h₂ Y₂⟦1⟧, the fiber Y of the composite g₁ ≫ g₂ lies in P.extensionProduct Q (when P Y₁, Q Y₂). Proof is three lines in an [IsTriangulated C]:

obtain ⟨Y, f, h, hT⟩ := distinguished_cocone_triangle₁ (g₁ ≫ g₂) exact ⟨Y, f, h, hT, _, _, _, _, _, (Triangulated.someOctahedron' rfl hT₁ hT₂ hT).mem, hY₁, hY₂⟩

Octahedron' is the version with triangles written as Z ⟶ X₁ ⟶ X₂ (fibers first), so its mem field is exactly the triangle Y₁ ⟶ Y ⟶ Y₂ ⟶ Y₁⟦1⟧ — no rotations or sign juggling. Mathlib's own ObjectProperty.extensionProduct_assoc (Triangulated/Subcategory.lean) uses the same trick. For an induction over a list of pieces, make the hypothesis *relative* (decompose every object of a triangulated subcategory A, then recurse into A ⊓ E^⊥): Mathlib has IsTriangulated instances for P ⊓ P' and for rightOrthogonal, plus ext_of_isTriangulatedClosed₃ to see the cone stays in A. (⊤ : ObjectProperty C).IsTriangulated is missing; it is where isStableUnderShiftBy _ := ⟨fun _ _ ↦ trivial⟩; ext₂' _ _ _ _ := le_isoClosure _ _ trivial.