Mathlib (late 2026): CategoryTheory.End is now a structure

In recent Mathlib, End X is no longer defeq to X ⟶ X. It is structure End (X) where of :: asHom : X ⟶ X, with mul f g = .of (g.asHom ≫ f.asHom) and simp lemmas one_asHom/mul_asHom; End.one_def/mul_def are deprecated. Older code passing f : End X where X ⟶ X is expected, or h : (1 : End X) = 0 where 𝟙 X = 0 is expected, now fails with type mismatches. Fix: use f.asHom, congrArg End.asHom h, build elements with End.of, and prove equalities in End X by ext (there is an @[ext] lemma) followed by simp. Example: to show IsLocalRing (End X) from finrank k (X ⟶ X) = 1, apply finrank_eq_one_iff_of_nonzero' (𝟙 X) to f.asHom, then build the inverse ⟨⟨f, End.of (c⁻¹ • 𝟙 X), _, _⟩, rfl⟩ and close each goal with ext; simp [← hc, smul_smul, hc₀].