Computing a triangulated functor on a cone: scalar arrow iso trick

To compute F(X₃) for a triangulated functor F (e.g. a Serre functor) applied to a distinguished triangle X₁ → X₂ → X₃ when F(X₁), F(X₂) are known up to iso: conjugate F(f) by the isos to get φ : Y₁ ⟶ Y₂, then build the triangle (φ, e₂.inv ≫ F g, (F h ≫ commShiftIso.hom.app _) ≫ e₁.hom⟦1⟧') via isomorphic_distinguished with Triangle.isoMk e₁.symm e₂.symm (Iso.refl _); simp closes the three squares. If Hom(Y₁, Y₂) has finrank 1, finrank_eq_one_iff_of_nonzero' gives φ = c • φ₀ for a known φ₀ (c ≠ 0 since F is faithful), and Mathlib's Pretriangulated.exists_iso_of_arrow_iso with Arrow.isoMk (c • 𝟙 as an iso) (Iso.refl _) hcomm identifies the cones; take Triangle.π₃.mapIso. Lean tips: introduce the triangle as obtain ⟨g, h, hT⟩ : ∃ g h, Triangle.mk f g h ∈ distTriang _ := ⟨_, _, ...⟩ so later terms stay small; prove the Arrow.isoMk square as a separate have (inline simpa hit a heartbeat timeout); and don't rw [← lemma_with_rhs_1] in a finrank goal, since it rewrites every 1 (motive error); use .trans instead.