-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
Goal:
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
inl :
  Subsingleton R →
    ∃ (p : R[X]),
      p.Monic ∧
        p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
          (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
            Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
              (0 : Module.End R M)
inr inr₁ :
  Nontrivial R →
    ∃ (p : R[X]),
      p.Monic ∧
        p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
          (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
            Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
              (0 : Module.End R M)
inr₂ :
  Nontrivial R →
    ∀ (s : Finset M) (hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤)
      (hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤),
      ∃ (p : R[X]),
        p.Monic ∧
          p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
            (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
              Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
                (0 : Module.End R M)
inr₃ :
  Nontrivial R →
    ∀ (s : Finset M) (hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤)
      (hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
      (this :
        Eq.{u_2 + 1} (α := Submodule R M)
          (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤),
      ∃ (p : R[X]),
        p.Monic ∧
          p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
            (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
              Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
                (0 : Module.End R M)
⊢ ∃ (p : R[X]),
    p.Monic ∧
      p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
        (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
          Eq.{u_2 + 1} (α := Module.End R M) ((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M)
            (0 : Module.End R M)
have inr₄ : Nontrivial R →
  ∀ (s : Finset M) (hs_card : s.card = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤)
    (hs_span : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤)
    (this :
      Eq.{u_2 + 1} (α := Submodule R M)
        (Submodule.span R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) ⊤)
    (A : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
    (h : ∀ (i j : ↥s), (↑A : Matrix (↥s) (↥s) R) i j ∈ I)
    (hI :
      range (R := R) (M := M) (τ₁₂ := RingHom.id R)
          ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
              (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
            A) ≤
        HSMul.hSMul (β := Submodule R M) I ⊤),
    ∃ (p : R[X]),
      p.Monic ∧
        p.natDegree = Submodule.spanFinrank.{u_2, u_3} (R := R) (M := M) ⊤ ∧
          (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧
            Eq.{u_2 + 1} (α := Module.End R M)
              (((aeval
                        ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
                            (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
                          A) :
                      AlgHom.{u_3, u_3, u_2} R R[X] (Module.End R M)) :
                    (a : R[X]) → Module.End R M)
                  p :
                Module.End R M)
              (0 : Module.End R M)
Tactic: classical
    cases subsingleton_or_nontrivial R
    · exact ⟨0, by simp [nontriviality]⟩
    obtain ⟨s, hs_card, hs_span⟩ :=
      Submodule.FG.exists_span_finset_card_eq_spanFinrank (R := R) (M := M) Module.Finite.fg_top
    have : Submodule.span R (Set.range ((↑) : s → M)) = ⊤ := by simp [hs_span]
    obtain ⟨A, rfl, h⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R ((↑) : s → M) this f I hI
    refine ⟨A.1.charpoly, A.1.charpoly_monic, by simp [hs_card],
            by simpa using coeff_charpoly_mem_ideal_pow h, ?_⟩
    rw [Polynomial.aeval_algHom_apply,
      ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) this)]
    congr 1
    ext1
    rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]
Cleared hypotheses: f, hI