-- Lean 4 proof step from Mathlib.LinearAlgebra.Semisimple (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
K : Type u_3
inst_1 : Field K
inst_2 : Module K M
f : End K M
inst_3 : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})
this_1 : Module.Finite K R
this : IsReduced R
rw :
  Eq.{u_2 + 1} (α := End K M)
    (((aeval
              ((AlgHom.comp (B := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))
                    (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯)
                    (Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})) :
                  (a : K[X]) → End K M)
                p) :
            AlgHom.{u_3, u_3, u_2} K K[X] (End K M)) :
          (a : K[X]) → End K M)
        (minpoly K (B := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))
          ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f}) : (a : K[X]) → K[X] ⧸ Ideal.span {minpoly K f}) p :
            HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))) :
      End K M)
    (0 : End K M)
rw₁ :
  Eq.{u_2 + 1} (α := End K M)
    ((AlgHom.comp
            (AlgHom.comp (B := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))
              (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯)
              (Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})))
            (aeval p) :
          (a : K[X]) → End K M)
        (minpoly K (B := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))
          ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f}) : (a : K[X]) → K[X] ⧸ Ideal.span {minpoly K f}) p :
            HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))) :
      End K M)
    (0 : End K M)
rw₂ :
  Eq.{u_2 + 1} (α := End K M)
    ((AlgHom.comp (B := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))
            (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯)
            (Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})) :
          (a : K[X]) → End K M)
        ((aeval p : (a : K[X]) → K[X])
          (minpoly K (B := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))
            ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f}) : (a : K[X]) → K[X] ⧸ Ideal.span {minpoly K f}) p :
              HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f})))) :
      End K M)
    (0 : End K M)
⊢ Eq.{u_2 + 1} (α := End K M)
    (((aeval ((aeval f : (a : K[X]) → End K M) p) : AlgHom.{u_3, u_3, u_2} K K[X] (End K M)) : (a : K[X]) → End K M)
        (minpoly K (B := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))
          ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f}) : (a : K[X]) → K[X] ⧸ Ideal.span {minpoly K f}) p :
            HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))) :
      End K M)
    (0 : End K M)
have rw₃ : Eq.{u_2 + 1} (α := End K M)
  ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) sorry : (a : K[X] ⧸ Ideal.span {minpoly K f}) → End K M)
      ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f}) : (a : K[X]) → K[X] ⧸ Ideal.span {minpoly K f})
        ((aeval p : (a : K[X]) → K[X])
          (minpoly K (B := HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))
            ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f}) : (a : K[X]) → K[X] ⧸ Ideal.span {minpoly K f}) p :
              HasQuotient.Quotient K[X] (B := Ideal K[X]) (Ideal.span {minpoly K f}))))) :
    End K M)
  (0 : End K M)
Tactic: rw [← Ideal.Quotient.liftₐ_comp (.span {minpoly K f}) (aeval f)
        fun a h ↦ by rwa [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly] at h, aeval_algHom,
        AlgHom.comp_apply, AlgHom.comp_apply, ← aeval_algHom_apply, minpoly.aeval, map_zero]