Mathlib: essential image of a full triangulated functor is already triangulated

To show a triangulated functor F (with [F.CommShift ℤ] [F.IsTriangulated] [F.Full]) is essentially surjective, you don't need to prove that its essential image is closed under cones yourself. Mathlib's Triangulated/Subcategory.lean has an instance F.essImage.IsTriangulated, and Mathlib knows the essential image is closed under isomorphisms. So it is enough to show that F's image contains a generating set and to use a 'contained in every triangulated subcategory containing the generators' lemma. I used this to show that a Serre functor is an equivalence when there is a full exceptional collection. Rotating the collection n times makes (S E₁, …, S Eₙ) full, and it lies in essImage S. Gotcha: get S.functor.Full as a local have (from a fully-faithful structure) before the instance search runs.