-- Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
theorem Matrix.Represents.mul {A A' : Matrix ι ι R} {f f' : Module.End R M} (h : A.Represents b f)
    (h' : Matrix.Represents b A' f') : (A * A').Represents b (f * f')

Proof state:
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
b : ι → M
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i✝ : ι
⊢ (((LinearMap.llcomp R (ι → R) (ι → R) M) ((Fintype.linearCombination R R) b))
          (algEquivMatrix'.symm A * algEquivMatrix'.symm A') ∘ₗ
        LinearMap.single R (fun i => R) i✝)
      1 =
    ((PiToModule.fromEnd R b) (f * f') ∘ₗ LinearMap.single R (fun i => R) i✝) 1

Tactic:
dsimp [PiToModule.fromEnd]

Result:
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
b : ι → M
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i✝ : ι
⊢ ((Fintype.linearCombination R R) b) ((algEquivMatrix'.symm A) ((algEquivMatrix'.symm A') (Pi.single i✝ 1))) =
    f (f' (((Fintype.linearCombination R R) b) (Pi.single i✝ 1)))

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
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.linearCombination R R) b) ∘ₗ algEquivMatrix'.symm.toLinearMap)
      (A * A') =
    (PiToModule.fromEnd R b) (f * f')

Tactic:
rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, _root_.map_mul]

Result:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
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.linearCombination R R) b))
      (algEquivMatrix'.symm A * algEquivMatrix'.symm A') =
    (PiToModule.fromEnd R b) (f * f')

Proof state:
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
b : ι → M
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i✝ : ι
⊢ ((Fintype.linearCombination R R) b) ((algEquivMatrix'.symm A) ((algEquivMatrix'.symm A') (Pi.single i✝ 1))) =
    ((Fintype.linearCombination R R) b) (A *ᵥ A' *ᵥ Pi.single i✝ 1)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
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')

Tactic:
delta Matrix.Represents PiToModule.fromMatrix

Result:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
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.linearCombination R R) b) ∘ₗ algEquivMatrix'.symm.toLinearMap)
      (A * A') =
    (PiToModule.fromEnd R b) (f * f')

Proof state:
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
b : ι → M
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i✝ : ι
⊢ ((Fintype.linearCombination R R) b) ((algEquivMatrix'.symm A) ((algEquivMatrix'.symm A') (Pi.single i✝ 1))) =
    f (f' (((Fintype.linearCombination R R) b) (Pi.single i✝ 1)))

Tactic:
rw [← h'.congr_fun, ← h.congr_fun]

Result:
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
b : ι → M
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i✝ : ι
⊢ ((Fintype.linearCombination R R) b) ((algEquivMatrix'.symm A) ((algEquivMatrix'.symm A') (Pi.single i✝ 1))) =
    ((Fintype.linearCombination R R) b) (A *ᵥ A' *ᵥ Pi.single i✝ 1)

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
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.linearCombination R R) b))
      (algEquivMatrix'.symm A * algEquivMatrix'.symm A') =
    (PiToModule.fromEnd R b) (f * f')

Tactic:
ext

Result:
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
b : ι → M
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i✝ : ι
⊢ (((LinearMap.llcomp R (ι → R) (ι → R) M) ((Fintype.linearCombination R R) b))
          (algEquivMatrix'.symm A * algEquivMatrix'.symm A') ∘ₗ
        LinearMap.single R (fun i => R) i✝)
      1 =
    ((PiToModule.fromEnd R b) (f * f') ∘ₗ LinearMap.single R (fun i => R) i✝) 1