-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
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)
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)
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 ⊤),
      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)
            (↑A : Matrix (↥s) (↥s) R).charpoly :
          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)))) ⊤)
      (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 ⊤),
      Eq.{u_2 + 1} (α := Module.End R M)
        ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
              (a : ↥(isRepresentation R Subtype.val)) → Module.End R M)
            ((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly) :
          Module.End R M)
        ((isRepresentation.toEnd R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) this :
              (a : ↥(isRepresentation R Subtype.val)) → 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)))) ⊤)
      (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 ⊤),
      Eq (α := ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
        ((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly :
          ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
        (0 : ↥(isRepresentation R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
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 ⊤),
      Eq (α := Matrix.{u_2, u_2, u_3} (↥s) (↥s) R)
        (↑((aeval A : (a : R[X]) → ↥(isRepresentation R Subtype.val)) (↑A : Matrix (↥s) (↥s) R).charpoly) :
          Matrix (↥s) (↥s) R)
        (↑0 : Matrix (↥s) (↥s) 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)

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]

Premises used: Submodule.FG.exists_span_finset_card_eq_spanFinrank, Module.Finite.fg_top, Polynomial.aeval_subalgebra_coe, subsingleton_or_nontrivial, Subalgebra.coe_zero, Matrix.aeval_self_charpoly, Polynomial.aeval_algHom_apply, rfl