-- 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.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

Tactic:
obtain ⟨A, H, h⟩ :=
  Matrix.isRepresentation.toEnd_exists_mem_ideal R ((↑) : s → M)
    (by rw [Subtype.range_coe_subtype, Finset.setOf_mem, hs]) f I hI

Result:
case inr.intro.intro.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 = ⊤
A : ↥(isRepresentation R Subtype.val)
H : (isRepresentation.toEnd R Subtype.val ⋯) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∃ 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 ^ ((↑A).charpoly.natDegree - k)

Tactic:
rw [A.1.charpoly_natDegree_eq_dim]

Result:
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)

Proof state:
case inr.intro.intro.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 = ⊤
A : ↥(isRepresentation R Subtype.val)
H : (isRepresentation.toEnd R Subtype.val ⋯) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∃ p, p.Monic ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (aeval f) p = 0

Tactic:
rw [← H]

Result:
case inr.intro.intro.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 = ⊤
A : ↥(isRepresentation R Subtype.val)
H : (isRepresentation.toEnd R Subtype.val ⋯) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∃ p,
    p.Monic ∧
      (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (aeval ((isRepresentation.toEnd R Subtype.val ⋯) A)) p = 0

Proof state:
case inr.intro.intro.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 = ⊤
A : ↥(isRepresentation R Subtype.val)
H : (isRepresentation.toEnd R Subtype.val ⋯) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∃ p,
    p.Monic ∧
      (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (aeval ((isRepresentation.toEnd R Subtype.val ⋯) A)) p = 0

Tactic:
refine ⟨A.1.charpoly, A.1.charpoly_monic, ?_, ?_⟩

Result:
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 ^ ((↑A).charpoly.natDegree - k)

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

Proof state:
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

Tactic:
exact ⟨0, Polynomial.monic_of_subsingleton _, by simp⟩

Result:
no goals