-- Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
theorem LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul
    [Module.Finite R M] (f : Module.End R M) (I : Ideal R) (hI : LinearMap.range f ≤ I • ⊤) :
    ∃ p : R[X], p.Monic ∧ (∀ k, p.coeff k ∈ I ^ (p.natDegree - k)) ∧ Polynomial.aeval f p = 0

Proof state:
case inr
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
⊢ ∃ p, p.Monic ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (aeval f) p = 0

Tactic:
obtain ⟨s : Finset M, hs : Submodule.span R (s : Set M) = ⊤⟩ :=
  Module.Finite.fg_top (R := R) (M := M)

Result:
case inr.intro
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
⊢ ∃ p, p.Monic ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (aeval f) p = 0

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
⊢ ∃ p, p.Monic ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (aeval f) p = 0

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Subsingleton R
⊢ ∃ p, p.Monic ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (aeval f) p = 0

case inr
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
⊢ ∃ p, p.Monic ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (aeval f) p = 0

Proof state:
case inr.intro.intro.intro.refine_1
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : ↥(isRepresentation R Subtype.val)
H : (isRepresentation.toEnd R Subtype.val ⋯) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∀ (k : ℕ), (↑A).charpoly.coeff k ∈ I ^ (Fintype.card { x // x ∈ s } - k)

Tactic:
exact coeff_charpoly_mem_ideal_pow h

Result:
no goals

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
⊢ Submodule.span R (Set.range Subtype.val) = ⊤

Tactic:
rw [Subtype.range_coe_subtype, Finset.setOf_mem, hs]

Result:
no goals

Proof state:
case inr.intro.intro.intro.refine_2.h.e_6.h.a
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : ↥(isRepresentation R Subtype.val)
H : (isRepresentation.toEnd R Subtype.val ⋯) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ↑((aeval A) (↑A).charpoly) = ↑0

Tactic:
rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]

Result:
no goals

Proof state:
case inr.intro.intro.intro.refine_2
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : ↥(isRepresentation R Subtype.val)
H : (isRepresentation.toEnd R Subtype.val ⋯) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ (aeval ((isRepresentation.toEnd R Subtype.val ⋯) A)) (↑A).charpoly = 0

Tactic:
rw [Polynomial.aeval_algHom_apply,
  ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) _)]

Result:
case inr.intro.intro.intro.refine_2
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : ↥(isRepresentation R Subtype.val)
H : (isRepresentation.toEnd R Subtype.val ⋯) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ (isRepresentation.toEnd R Subtype.val ⋯) ((aeval A) (↑A).charpoly) =
    (isRepresentation.toEnd R Subtype.val ?m.156307) 0

M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : ↥(isRepresentation R Subtype.val)
H : (isRepresentation.toEnd R Subtype.val ⋯) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ Submodule.span R (Set.range Subtype.val) = ⊤

Proof state:
case inr.intro.intro.intro.refine_2
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : ↥(isRepresentation R Subtype.val)
H : (isRepresentation.toEnd R Subtype.val ⋯) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ (isRepresentation.toEnd R Subtype.val ⋯) ((aeval A) (↑A).charpoly) =
    (isRepresentation.toEnd R Subtype.val ?m.156307) 0

M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : ↥(isRepresentation R Subtype.val)
H : (isRepresentation.toEnd R Subtype.val ⋯) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ Submodule.span R (Set.range Subtype.val) = ⊤

Tactic:
congr 1

Result:
case inr.intro.intro.intro.refine_2.h.e_6.h
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : ↥(isRepresentation R Subtype.val)
H : (isRepresentation.toEnd R Subtype.val ⋯) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ (aeval A) (↑A).charpoly = 0

Proof state:
case inr.intro.intro.intro.refine_2.h.e_6.h
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : ↥(isRepresentation R Subtype.val)
H : (isRepresentation.toEnd R Subtype.val ⋯) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ (aeval A) (↑A).charpoly = 0

Tactic:
ext1

Result:
case inr.intro.intro.intro.refine_2.h.e_6.h.a
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : ↥(isRepresentation R Subtype.val)
H : (isRepresentation.toEnd R Subtype.val ⋯) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ↑((aeval A) (↑A).charpoly) = ↑0

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Subsingleton R
⊢ (∀ (k : ℕ), coeff 0 k ∈ I ^ (natDegree 0 - k)) ∧ (aeval f) 0 = 0

Tactic:
simp

Result:
no goals