Proving S(E_n) ≅ mutation in Lean by dimension count, no explicit iso

To show two objects A, Z of a triangulated category are isomorphic when Z is exceptional (End Z = k, no self-Ext), you can skip writing down a map. Build the evaluation map ⨁_{(m,i)} Z[m] → A, where i runs over a basis of Hom(Z[m], A), and show its cone lies in an orthogonal that is zero (e.g. by fullness of an exceptional collection). Then compute dim Hom(Z[m], A) = δ_{m0}. The index type then has Fintype.card 1, so Fintype.card_eq_one_iff gives j₀ with ∀ j, j = j₀. A biproduct over such a type is its j₀ summand (hom := π j₀, inv := ι j₀, and ext followed by subst for hom_inv_id). Finally (shiftFunctorZero' C m hm).app Z turns Z[m] with m = 0 propositionally into Z. This proved Bondal–Kapranov's S Eₙ ≅ L_{⟨E₁..Eₙ₋₁⟩} Eₙ in about 60 lines.