R : Type u_1
R₁ : Type ?u.1647539
R₂ : Type ?u.1647542
M : Type ?u.1647545
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type ?u.1647554
M₂' : Type u_4
n : Type u_5
m : Type u_7
n' : Type ?u.1647566
m' : Type u_6
ι : Type ?u.1647572
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₂' →ₗ[R] M₂
⊢ (↑(toMatrix b₁ b₁) id)ᵀ ⬝ ↑(toMatrix₂ b₁ b₂) B ⬝ ↑(toMatrix b₂' b₂) f =
    ↑(toMatrix₂ b₁ b₂) (comp B id) ⬝ ↑(toMatrix b₂' b₂) f
R : Type u_1
R₁ : Type ?u.1647539
R₂ : Type ?u.1647542
M : Type ?u.1647545
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type ?u.1647554
M₂' : Type u_4
n : Type u_5
m : Type u_7
n' : Type ?u.1647566
m' : Type u_6
ι : Type ?u.1647572
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₂' →ₗ[R] M₂
⊢ ↑(toMatrix₂ b₁ b₂') (compl₂ B f) = ↑(toMatrix₂ b₁ b₂) B ⬝ ↑(toMatrix b₂' b₂) f
rw [← LinearMap.comp_id B, ← LinearMap.compl₁₂, LinearMap.toMatrix₂_compl₁₂ b₁ b₂]
no goals
R : Type u_1
R₁ : Type ?u.1647539
R₂ : Type ?u.1647542
M : Type ?u.1647545
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type ?u.1647554
M₂' : Type u_4
n : Type u_5
m : Type u_7
n' : Type ?u.1647566
m' : Type u_6
ι : Type ?u.1647572
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₂' →ₗ[R] M₂
⊢ (↑(toMatrix b₁ b₁) id)ᵀ ⬝ ↑(toMatrix₂ b₁ b₂) B ⬝ ↑(toMatrix b₂' b₂) f =
    ↑(toMatrix₂ b₁ b₂) (comp B id) ⬝ ↑(toMatrix b₂' b₂) f
simp