case inl
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Subsingleton R
⊢ ∃ p, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0

case inr
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
⊢ ∃ p, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
⊢ ∃ p, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
cases subsingleton_or_nontrivial R
case inr.intro
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
case inr
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
⊢ ∃ p, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
obtain ⟨s : Finset M, hs : Submodule.span R (s : Set M) = ⊤⟩ := Module.Finite.out
case inr.intro.intro.intro
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val ?m.197024) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∃ p, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
case inr.intro
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
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
case inr.intro.intro.intro
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val ?m.197024) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∃ p,
    Monic p ∧
      (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧
        ↑(aeval (↑(Matrix.isRepresentation.toEnd R Subtype.val ?m.197024) A)) p = 0

ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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) = ⊤
case inr.intro.intro.intro
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val ?m.197024) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∃ p, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
rw [← H]
case inr.intro.intro.intro.refine'_1
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∀ (k : ℕ), coeff (Matrix.charpoly ↑A) k ∈ I ^ (natDegree (Matrix.charpoly ↑A) - k)

case inr.intro.intro.intro.refine'_2
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ↑(aeval (↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A))
      (Matrix.charpoly ↑A) =
    0
case inr.intro.intro.intro
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val ?m.197024) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∃ p,
    Monic p ∧
      (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧
        ↑(aeval (↑(Matrix.isRepresentation.toEnd R Subtype.val ?m.197024) A)) p = 0

ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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) = ⊤
refine' ⟨A.1.charpoly, A.1.charpoly_monic, _, _⟩
no goals
case inl
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Subsingleton R
⊢ ∃ p, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
exact ⟨0, Polynomial.monic_of_subsingleton _, by simp⟩
no goals
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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
simp
no goals
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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) = ⊤
rw [Subtype.range_coe_subtype, Finset.setOf_mem, hs]
case inr.intro.intro.intro.refine'_1
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∀ (k : ℕ), coeff (Matrix.charpoly ↑A) k ∈ I ^ (Fintype.card { x // x ∈ s } - k)
case inr.intro.intro.intro.refine'_1
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∀ (k : ℕ), coeff (Matrix.charpoly ↑A) k ∈ I ^ (natDegree (Matrix.charpoly ↑A) - k)
rw [A.1.charpoly_natDegree_eq_dim]
no goals
case inr.intro.intro.intro.refine'_1
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∀ (k : ℕ), coeff (Matrix.charpoly ↑A) k ∈ I ^ (Fintype.card { x // x ∈ s } - k)
exact coeff_charpoly_mem_ideal_pow h
case inr.intro.intro.intro.refine'_2
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤))
      (↑(aeval A) (Matrix.charpoly ↑A)) =
    ↑(Matrix.isRepresentation.toEnd R Subtype.val ?m.199967) 0

ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ Submodule.span R (Set.range Subtype.val) = ⊤
case inr.intro.intro.intro.refine'_2
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ↑(aeval (↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A))
      (Matrix.charpoly ↑A) =
    0
rw [Polynomial.aeval_algHom_apply,
  ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) _)]
case inr.intro.intro.intro.refine'_2.h.e_6.h
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ↑(aeval A) (Matrix.charpoly ↑A) = 0
case inr.intro.intro.intro.refine'_2
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤))
      (↑(aeval A) (Matrix.charpoly ↑A)) =
    ↑(Matrix.isRepresentation.toEnd R Subtype.val ?m.199967) 0

ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ Submodule.span R (Set.range Subtype.val) = ⊤
congr 1
case inr.intro.intro.intro.refine'_2.h.e_6.h.a
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ↑(↑(aeval A) (Matrix.charpoly ↑A)) = ↑0
case inr.intro.intro.intro.refine'_2.h.e_6.h
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ↑(aeval A) (Matrix.charpoly ↑A) = 0
ext1
no goals
case inr.intro.intro.intro.refine'_2.h.e_6.h.a
ι : Type ?u.186389
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
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 : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ↑(↑(aeval A) (Matrix.charpoly ↑A)) = ↑0
rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]