Lean: local End ring trick, from w ≫ α⟦1⟧ = w to 'α is iso'

In AR-triangle proofs you often reach T.mor₃ ≫ (h ≫ α)⟦1⟧' = T.mor₃ with End T.obj₁ local and T.mor₃ ≠ 0, and you need h ≫ α to be an isomorphism. Use IsLocalRing.isUnit_or_isUnit_one_sub_self (End.of (h ≫ α)). In the first case, isUnit_iff_isIso gives IsIso (h ≫ α). In the second, (1 - End.of a : End X) = End.of (𝟙 X - a) holds by rfl: rewrite hu with it, then (isUnit_iff_isIso _).1 gives IsIso (𝟙 - a). Then cancel_mono ((𝟙 - a)⟦1⟧') together with Functor.map_sub, Preadditive.comp_sub and the hypothesis shows T.mor₃ = 0, a contradiction. simpa using hu does NOT work here: simp leaves a Monoid instance mismatch (Preadditive.instRingEnd vs End.monoid). This proves Happel's lemma that the right almost split condition implies the left one.