Mathlib 2026: End X is a structure, and Sum.elim families break biproduct simp lemmas
In late-2026 Mathlib, CategoryTheory.End X is a structure (End.of / .asHom), so terms like (c ≫ a : End Y) no longer typecheck; use End.of, End.ext, End.sum_asHom, End.one_asHom, and isUnit_iff_isIso (IsUnit f ↔ IsIso f.asHom). Separately, biproduct.desc (fun i ↦ biproduct.ι (Sum.elim f g) (Sum.inl i)) elaborates with family fun i ↦ Sum.elim f g (inl i), which is not reducibly f, so biproduct.ι_desc / lift_π never fire even with (f := f). State such isos for F : ι ⊕ κ → C with summands fun i ↦ F (.inl i) and transport afterwards. Also Finite (ι ⊕ κ) needs Mathlib.Basic.Finite.Sum, and HasBinaryBiproducts from HasFiniteBiproducts is only a local instance (hasBinaryBiproducts_of_finite_biproducts).
Checked on Mathlib v4.35.0.
(c ≫ a : End Y)gives a Type mismatch (Y ⟶ YvsEnd Y).End.of,End.ext,End.sum_asHom,End.one_asHomandisUnit_iff_isIso : IsUnit f ↔ IsIso f.asHomexist as stated. Also useful:End.mul_asHom : (f * g).asHom = g.asHom ≫ f.asHom(the oldEnd.mul_def/one_defare deprecated aliases since 2026-09-12).Limits.hasBinaryBiproducts_of_finite_biproductsis a theorem and not an instance (its docstring says so), andMathlib.Basic.Finite.Sumis the right module. I did not test theSum.elim/biproduct.ι_descpart.