Lean/Mathlib: proving two cones are isomorphic via a universal-map lemma + exists_iso_of_arrow_iso

Situation: two distinguished triangles share an object L, e.g. R → L →a T₁ → R⟦1⟧ and F → L →b T₂ → F⟦1⟧, where a and b are both 'universal maps from L into a subcategory P' (precomposition with a is a bijection Hom(T₁, W) ≃ Hom(L, W) for every W in P, same for b, and T₁, T₂ ∈ P). Goal: R ≅ F.

1. A 10-line lemma: from the two bijectivity hypotheses get φ := preimage of b under (a ≫ ·), ψ := preimage of a under (b ≫ ·), and φ ≫ ψ = 𝟙 by injectivity of (a ≫ ·) applied to a ≫ φ ≫ ψ = a ≫ 𝟙 (close it with simp only [reassoc_of% hφ, hψ, comp_id]). Result: ∃ e : T₁ ≅ T₂, a ≫ e.hom = b. (Do dsimp only at hφ hψ first: the preimage equations come out as beta-redexes (fun u ↦ a ≫ u) φ = b.) 2. Rotate both triangles so the shared map is mor₁ (rot_of_distTriang), then Mathlib's Pretriangulated.exists_iso_of_arrow_iso T₁ T₂ hT₁ hT₂ (Arrow.isoMk (Iso.refl L) e comm) gives an iso of triangles; Triangle.π₃.mapIso extracts R⟦1⟧ ≅ F⟦1⟧ and (shiftFunctor C 1).preimageIso unshifts. Gotcha: the comm argument of Arrow.isoMk is stated with (Arrow.mk T.rotate.mor₁).hom etc.; by dsimp; rw [id_comp, he] fails with a Quiver.Hom type mismatch (T.rotate.obj₁ vs L), but the term (id_comp h).trans he.symm (or he.trans (comp_id _).symm for the other orientation) is accepted by defeq. Used to prove that left and right mutations of exceptional pairs are mutually inverse.