case a.h
R : Type u_3
R₁ : Type u_4
R₂ : Type u_5
M : Type ?u.137024
M₁ : Type ?u.137027
M₂ : Type ?u.137030
M₁' : Type ?u.137033
M₂' : Type ?u.137036
n : Type u_1
m : Type u_2
n' : Type ?u.137045
m' : Type ?u.137048
ι : Type ?u.137051
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 : Matrix n m R
i : n
j : m
⊢ ↑(toMatrix₂Aux (fun i => ↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1) fun j =>
          ↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1)
      (toLinearMap₂'Aux σ₁ σ₂ f) i j =
    f i j
R : Type u_3
R₁ : Type u_4
R₂ : Type u_5
M : Type ?u.137024
M₁ : Type ?u.137027
M₂ : Type ?u.137030
M₁' : Type ?u.137033
M₂' : Type ?u.137036
n : Type u_1
m : Type u_2
n' : Type ?u.137045
m' : Type ?u.137048
ι : Type ?u.137051
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 : Matrix n m R
⊢ ↑(toMatrix₂Aux (fun i => ↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1) fun j =>
          ↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1)
      (toLinearMap₂'Aux σ₁ σ₂ f) =
    f
ext (i j)
no goals
case a.h
R : Type u_3
R₁ : Type u_4
R₂ : Type u_5
M : Type ?u.137024
M₁ : Type ?u.137027
M₂ : Type ?u.137030
M₁' : Type ?u.137033
M₂' : Type ?u.137036
n : Type u_1
m : Type u_2
n' : Type ?u.137045
m' : Type ?u.137048
ι : Type ?u.137051
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 : Matrix n m R
i : n
j : m
⊢ ↑(toMatrix₂Aux (fun i => ↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1) fun j =>
          ↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1)
      (toLinearMap₂'Aux σ₁ σ₂ f) i j =
    f i j
simp_rw [LinearMap.toMatrix₂Aux_apply, Matrix.toLinearMap₂'Aux_stdBasis]