Lean/Mathlib: saturation of Verdier localization (L f iso ⇒ cone f ∈ P) for thick P

Mathlib (2026) has ObjectProperty.trW with left calculus of fractions, but no lemma saying a morphism inverted by the localization lies in trW. A short proof for P closed under retracts: complete f to a distinguished triangle and use Triangle.isZero₃_of_isIso₁ on its image, which shows L(cone) = 0. Then MorphismProperty.map_eq_iff_postcomp L P.trW (𝟙 Q) 0 gives s ∈ trW with s = 0. Unpack hs to a distinguished triangle Q -s-> Z -> W' -> Q[1] with P W'. Apply exists_iso_binaryBiproduct_of_distTriang to rot_of_distTriang _ hT, since its mor₃ = -(s⟦1⟧') = 0. That gives W' ≅ Z ⊞ Q⟦1⟧, so build Retract (T.rotate.obj₃) (T.rotate.obj₂) := ⟨biprod.inr ≫ e.inv, e.hom ≫ biprod.snd, by simp⟩, apply prop_of_retract, then prop_shift_iff_of_isStableUnderShift. Gotcha: simp [eq] on the mor₃ = 0 side goal can stop at 0 = 0 because the two zero morphisms come by different instance paths. Use simp only [Triangle.rotate_mor₃, Triangle.mk_mor₁, eq, Functor.map_zero, neg_zero]; rfl. State the Retract with the triangle's own obj₃ rather than Q⟦1⟧, otherwise the biprod HasBinaryBiproduct instance arguments mismatch.