R : Type u_2
R₁ : Type u_1
R₂ : Type u_4
M : Type ?u.119507
M₁ : Type ?u.119510
M₂ : Type ?u.119513
M₁' : Type ?u.119516
M₂' : Type ?u.119519
n : Type u_3
m : Type u_5
n' : Type ?u.119528
m' : Type ?u.119531
ι : Type ?u.119534
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R₁ M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] R
i : n
j : m
⊢ ↑(↑(toLinearMap₂'Aux σ₁ σ₂
              (↑(toMatrix₂Aux (fun i => ↑(stdBasis R₁ (fun x => R₁) i) 1) fun j => ↑(stdBasis R₂ (fun x => R₂) j) 1) f))
          (↑(Pi.basisFun R₁ n) i))
      (↑(Pi.basisFun R₂ m) j) =
    ↑(↑f (↑(Pi.basisFun R₁ n) i)) (↑(Pi.basisFun R₂ m) j)
R : Type u_2
R₁ : Type u_1
R₂ : Type u_4
M : Type ?u.119507
M₁ : Type ?u.119510
M₂ : Type ?u.119513
M₁' : Type ?u.119516
M₂' : Type ?u.119519
n : Type u_3
m : Type u_5
n' : Type ?u.119528
m' : Type ?u.119531
ι : Type ?u.119534
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R₁ M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] R
⊢ toLinearMap₂'Aux σ₁ σ₂
      (↑(toMatrix₂Aux (fun i => ↑(stdBasis R₁ (fun x => R₁) i) 1) fun j => ↑(stdBasis R₂ (fun x => R₂) j) 1) f) =
    f
refine' ext_basis (Pi.basisFun R₁ n) (Pi.basisFun R₂ m) fun i j => _
no goals
R : Type u_2
R₁ : Type u_1
R₂ : Type u_4
M : Type ?u.119507
M₁ : Type ?u.119510
M₂ : Type ?u.119513
M₁' : Type ?u.119516
M₂' : Type ?u.119519
n : Type u_3
m : Type u_5
n' : Type ?u.119528
m' : Type ?u.119531
ι : Type ?u.119534
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R₁ M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
σ₁ : R₁ →+* R
σ₂ : R₂ →+* R
f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] R
i : n
j : m
⊢ ↑(↑(toLinearMap₂'Aux σ₁ σ₂
              (↑(toMatrix₂Aux (fun i => ↑(stdBasis R₁ (fun x => R₁) i) 1) fun j => ↑(stdBasis R₂ (fun x => R₂) j) 1) f))
          (↑(Pi.basisFun R₁ n) i))
      (↑(Pi.basisFun R₂ m) j) =
    ↑(↑f (↑(Pi.basisFun R₁ n) i)) (↑(Pi.basisFun R₂ m) j)
simp_rw [Pi.basisFun_apply, Matrix.toLinearMap₂'Aux_stdBasis, LinearMap.toMatrix₂Aux_apply]