[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
j : ι
⊢ ↑(↑(fromMatrix R b) A) (Pi.single j 1) = ∑ i : ι, A i j • b i
[PROOFSTEP]
rw [PiToModule.fromMatrix_apply, Fintype.total_apply, Matrix.mulVec_single]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
j : ι
⊢ ∑ i : ι, (fun i => A i j * 1) i • b i = ∑ i : ι, A i j • b i
[PROOFSTEP]
simp_rw [mul_one]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ ↑(↑(fromEnd R b) f) (Pi.single i 1) = ↑f (b i)
[PROOFSTEP]
rw [PiToModule.fromEnd_apply]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ ↑f (↑(↑(Fintype.total R R) b) (Pi.single i 1)) = ↑f (b i)
[PROOFSTEP]
congr
[GOAL]
case h.e_6.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ ↑(↑(Fintype.total R R) b) (Pi.single i 1) = b i
[PROOFSTEP]
convert Fintype.total_apply_single (S := R) R b i (1 : R)
[GOAL]
case h.e'_3
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ b i = 1 • b i
[PROOFSTEP]
rw [one_smul]
[GOAL]
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
⊢ Function.Injective ↑(fromEnd R b)
[PROOFSTEP]
intro x y e
[GOAL]
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
⊢ x = y
[PROOFSTEP]
ext m
[GOAL]
case h
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : M
⊢ ↑x m = ↑y m
[PROOFSTEP]
obtain ⟨m, rfl⟩ : m ∈ LinearMap.range (Fintype.total R R b) :=
  by
  rw [(Fintype.range_total R b).trans hb]
  exact Submodule.mem_top
[GOAL]
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : M
⊢ m ∈ LinearMap.range (↑(Fintype.total R R) b)
[PROOFSTEP]
rw [(Fintype.range_total R b).trans hb]
[GOAL]
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : M
⊢ m ∈ ⊤
[PROOFSTEP]
exact Submodule.mem_top
[GOAL]
case h.intro
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : ι → R
⊢ ↑x (↑(↑(Fintype.total R R) b) m) = ↑y (↑(↑(Fintype.total R R) b) m)
[PROOFSTEP]
exact (LinearMap.congr_fun e m : _)
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ Represents b A f ↔ ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ Represents b A f → ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
[PROOFSTEP]
intro h i
[GOAL]
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
i : ι
⊢ ∑ i_1 : ι, A i_1 i • b i_1 = ↑f (b i)
[PROOFSTEP]
have := LinearMap.congr_fun h (Pi.single i 1)
[GOAL]
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
i : ι
this : ↑(↑(PiToModule.fromMatrix R b) A) (Pi.single i 1) = ↑(↑(PiToModule.fromEnd R b) f) (Pi.single i 1)
⊢ ∑ i_1 : ι, A i_1 i • b i_1 = ↑f (b i)
[PROOFSTEP]
rwa [PiToModule.fromEnd_apply_single_one, PiToModule.fromMatrix_apply_single_one] at this 
[GOAL]
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ (∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)) → Represents b A f
[PROOFSTEP]
intro h
[GOAL]
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
⊢ Represents b A f
[PROOFSTEP]
refine LinearMap.pi_ext' (fun i => LinearMap.ext_ring ?_)
[GOAL]
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
i : ι
⊢ ↑(LinearMap.comp (↑(PiToModule.fromMatrix R b) A) (LinearMap.single i)) 1 =
    ↑(LinearMap.comp (↑(PiToModule.fromEnd R b) f) (LinearMap.single i)) 1
[PROOFSTEP]
simp_rw [LinearMap.comp_apply, LinearMap.coe_single, PiToModule.fromEnd_apply_single_one,
  PiToModule.fromMatrix_apply_single_one]
[GOAL]
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
i : ι
⊢ ∑ i_1 : ι, A i_1 i • b i_1 = ↑f (b i)
[PROOFSTEP]
apply h
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
⊢ Represents b (A * A') (f * f')
[PROOFSTEP]
delta Matrix.Represents PiToModule.fromMatrix
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
⊢ ↑(LinearMap.comp (↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b))
          (AlgEquiv.toLinearMap (AlgEquiv.symm algEquivMatrix')))
      (A * A') =
    ↑(PiToModule.fromEnd R b) (f * f')
[PROOFSTEP]
rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, _root_.map_mul]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
⊢ ↑(↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b))
      (↑(AlgEquiv.symm algEquivMatrix') A * ↑(AlgEquiv.symm algEquivMatrix') A') =
    ↑(PiToModule.fromEnd R b) (f * f')
[PROOFSTEP]
ext
[GOAL]
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i✝ : ι
⊢ ↑(LinearMap.comp
          (↑(↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b))
            (↑(AlgEquiv.symm algEquivMatrix') A * ↑(AlgEquiv.symm algEquivMatrix') A'))
          (LinearMap.single i✝))
      1 =
    ↑(LinearMap.comp (↑(PiToModule.fromEnd R b) (f * f')) (LinearMap.single i✝)) 1
[PROOFSTEP]
dsimp [PiToModule.fromEnd]
[GOAL]
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i✝ : ι
⊢ ↑(↑(Fintype.total R R) b)
      (↑(↑(AlgEquiv.symm algEquivMatrix') A) (↑(↑(AlgEquiv.symm algEquivMatrix') A') (Pi.single i✝ 1))) =
    ↑f (↑f' (↑(↑(Fintype.total R R) b) (Pi.single i✝ 1)))
[PROOFSTEP]
rw [← h'.congr_fun, ← h.congr_fun]
[GOAL]
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i✝ : ι
⊢ ↑(↑(Fintype.total R R) b)
      (↑(↑(AlgEquiv.symm algEquivMatrix') A) (↑(↑(AlgEquiv.symm algEquivMatrix') A') (Pi.single i✝ 1))) =
    ↑(↑(Fintype.total R R) b) (mulVec A (mulVec A' (Pi.single i✝ 1)))
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ Represents b 1 1
[PROOFSTEP]
delta Matrix.Represents PiToModule.fromMatrix
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ ↑(LinearMap.comp (↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b))
          (AlgEquiv.toLinearMap (AlgEquiv.symm algEquivMatrix')))
      1 =
    ↑(PiToModule.fromEnd R b) 1
[PROOFSTEP]
rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, _root_.map_one]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ ↑(↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b)) 1 = ↑(PiToModule.fromEnd R b) 1
[PROOFSTEP]
ext
[GOAL]
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
i✝ : ι
⊢ ↑(LinearMap.comp (↑(↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b)) 1) (LinearMap.single i✝)) 1 =
    ↑(LinearMap.comp (↑(PiToModule.fromEnd R b) 1) (LinearMap.single i✝)) 1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
⊢ Represents b (A + A') (f + f')
[PROOFSTEP]
delta Matrix.Represents at h h' ⊢
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : ↑(PiToModule.fromMatrix R b) A = ↑(PiToModule.fromEnd R b) f
h' : ↑(PiToModule.fromMatrix R b) A' = ↑(PiToModule.fromEnd R b) f'
⊢ ↑(PiToModule.fromMatrix R b) (A + A') = ↑(PiToModule.fromEnd R b) (f + f')
[PROOFSTEP]
rw [map_add, map_add, h, h']
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ Represents b 0 0
[PROOFSTEP]
delta Matrix.Represents
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ ↑(PiToModule.fromMatrix R b) 0 = ↑(PiToModule.fromEnd R b) 0
[PROOFSTEP]
rw [map_zero, map_zero]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
r : R
⊢ Represents b (r • A) (r • f)
[PROOFSTEP]
delta Matrix.Represents at h ⊢
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ↑(PiToModule.fromMatrix R b) A = ↑(PiToModule.fromEnd R b) f
r : R
⊢ ↑(PiToModule.fromMatrix R b) (r • A) = ↑(PiToModule.fromEnd R b) (r • f)
[PROOFSTEP]
rw [SMulHomClass.map_smul, SMulHomClass.map_smul, h]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
[PROOFSTEP]
have : ∀ x, f x ∈ LinearMap.range (Ideal.finsuppTotal ι M I b) :=
  by
  rw [Ideal.range_finsuppTotal, hb]
  exact fun x => hI (LinearMap.mem_range_self f x)
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∀ (x : M), ↑f x ∈ LinearMap.range (Ideal.finsuppTotal ι M I b)
[PROOFSTEP]
rw [Ideal.range_finsuppTotal, hb]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∀ (x : M), ↑f x ∈ I • ⊤
[PROOFSTEP]
exact fun x => hI (LinearMap.mem_range_self f x)
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
this : ∀ (x : M), ↑f x ∈ LinearMap.range (Ideal.finsuppTotal ι M I b)
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
[PROOFSTEP]
choose bM' hbM' using this
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
[PROOFSTEP]
let A : Matrix ι ι R := fun i j => bM' (b j) i
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
[PROOFSTEP]
have : A.Represents b f := by
  rw [Matrix.represents_iff']
  dsimp
  intro j
  specialize hbM' (b j)
  rwa [Ideal.finsuppTotal_apply_eq_of_fintype] at hbM' 
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ Represents b A f
[PROOFSTEP]
rw [Matrix.represents_iff']
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ ∀ (j : ι), ∑ i : ι, ↑(↑(bM' (b j)) i) • b i = ↑f (b j)
[PROOFSTEP]
intro j
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
j : ι
⊢ ∑ i : ι, ↑(↑(bM' (b j)) i) • b i = ↑f (b j)
[PROOFSTEP]
specialize hbM' (b j)
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
j : ι
hbM' : ↑(Ideal.finsuppTotal ι M I b) (bM' (b j)) = ↑f (b j)
⊢ ∑ i : ι, ↑(↑(bM' (b j)) i) • b i = ↑f (b j)
[PROOFSTEP]
rwa [Ideal.finsuppTotal_apply_eq_of_fintype] at hbM' 
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
this : Represents b A f
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
[PROOFSTEP]
exact
  ⟨⟨A, f, this⟩, Matrix.isRepresentation.eq_toEnd_of_represents R b hb ⟨A, f, this⟩ this, fun i j => (bM' (b j) i).prop⟩
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ Function.Surjective ↑(toEnd R b hb)
[PROOFSTEP]
intro f
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
⊢ ∃ a, ↑(toEnd R b hb) a = f
[PROOFSTEP]
obtain ⟨M, e, -⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R b hb f ⊤ (by simp)
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
⊢ LinearMap.range f ≤ ⊤ • ⊤
[PROOFSTEP]
simp
[GOAL]
case intro.intro
ι : Type u_1
inst✝⁴ : Fintype ι
M✝ : Type u_2
inst✝³ : AddCommGroup M✝
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M✝
I : Ideal R
b : ι → M✝
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M✝
M : { x // x ∈ isRepresentation R b }
e : ↑(toEnd R b hb) M = f
⊢ ∃ a, ↑(toEnd R b hb) a = f
[PROOFSTEP]
exact ⟨M, e⟩
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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
[PROOFSTEP]
classical
cases subsingleton_or_nontrivial R
· exact ⟨0, Polynomial.monic_of_subsingleton _, by simp⟩
obtain ⟨s : Finset M, hs : Submodule.span R (s : Set M) = ⊤⟩ :=
  Module.Finite.out (R := R) (M := M)
    -- Porting note: `H` was `rfl`
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
rw [← H]
refine' ⟨A.1.charpoly, A.1.charpoly_monic, _, _⟩
· rw [A.1.charpoly_natDegree_eq_dim]
  exact coeff_charpoly_mem_ideal_pow h
· rw [Polynomial.aeval_algHom_apply, ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) _)]
  congr 1
  ext1
  rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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
[PROOFSTEP]
exact ⟨0, Polynomial.monic_of_subsingleton _, by simp⟩
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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
[PROOFSTEP]
simp
[GOAL]
case inr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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
[PROOFSTEP]
obtain ⟨s : Finset M, hs : Submodule.span R (s : Set M) = ⊤⟩ :=
  Module.Finite.out (R := R) (M := M)
    -- Porting note: `H` was `rfl`
[GOAL]
case inr.intro
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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
[PROOFSTEP]
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
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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) = ⊤
[PROOFSTEP]
rw [Subtype.range_coe_subtype, Finset.setOf_mem, hs]
[GOAL]
case inr.intro.intro.intro
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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
⊢ ∃ p, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
[PROOFSTEP]
rw [← H]
[GOAL]
case inr.intro.intro.intro
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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
⊢ ∃ p,
    Monic p ∧
      (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧
        ↑(aeval (↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A))
            p =
          0
[PROOFSTEP]
refine' ⟨A.1.charpoly, A.1.charpoly_monic, _, _⟩
[GOAL]
case inr.intro.intro.intro.refine'_1
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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)
[PROOFSTEP]
rw [A.1.charpoly_natDegree_eq_dim]
[GOAL]
case inr.intro.intro.intro.refine'_1
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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)
[PROOFSTEP]
exact coeff_charpoly_mem_ideal_pow h
[GOAL]
case inr.intro.intro.intro.refine'_2
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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
[PROOFSTEP]
rw [Polynomial.aeval_algHom_apply, ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) _)]
[GOAL]
case inr.intro.intro.intro.refine'_2
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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.193133) 0
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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) = ⊤
[PROOFSTEP]
congr 1
[GOAL]
case inr.intro.intro.intro.refine'_2.h.e_6.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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
[PROOFSTEP]
ext1
[GOAL]
case inr.intro.intro.intro.refine'_2.h.e_6.h.a
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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
[PROOFSTEP]
rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
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
⊢ range f ≤ ⊤ • ⊤
[PROOFSTEP]
simp
