ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
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')
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
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')
delta Matrix.Represents PiToModule.fromMatrix
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
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')
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
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')
rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, _root_.map_mul]
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
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
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
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')
ext
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
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)))
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
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
dsimp [PiToModule.fromEnd]
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
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)))
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
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)))
rw [← h'.congr_fun, ← h.congr_fun]
no goals
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
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)))
rfl