R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.456748
l : Type ?u.456751
m : Type u_3
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ ↑f (↑(stdBasis R (fun x => R) j) 1) i = ↑f (fun j' => if j' = j then 1 else 0) i
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.456748
l : Type ?u.456751
m : Type u_3
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ ↑toMatrix' f i j = ↑f (fun j' => if j' = j then 1 else 0) i
simp only [LinearMap.toMatrix', LinearEquiv.coe_mk, of_apply]
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.456748
l : Type ?u.456751
m : Type u_3
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ ↑f (↑(stdBasis R (fun x => R) j) 1) = ↑f fun j' => if j' = j then 1 else 0
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.456748
l : Type ?u.456751
m : Type u_3
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ ↑f (↑(stdBasis R (fun x => R) j) 1) i = ↑f (fun j' => if j' = j then 1 else 0) i
refine congr_fun ?_ _
case h.e_6.h
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.456748
l : Type ?u.456751
m : Type u_3
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ ↑(stdBasis R (fun x => R) j) 1 = fun j' => if j' = j then 1 else 0
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.456748
l : Type ?u.456751
m : Type u_3
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ ↑f (↑(stdBasis R (fun x => R) j) 1) = ↑f fun j' => if j' = j then 1 else 0
congr
case h.e_6.h.h
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.456748
l : Type ?u.456751
m : Type u_3
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
⊢ ↑(stdBasis R (fun x => R) j) 1 j' = if j' = j then 1 else 0
case h.e_6.h
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.456748
l : Type ?u.456751
m : Type u_3
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ ↑(stdBasis R (fun x => R) j) 1 = fun j' => if j' = j then 1 else 0
ext j'
case h.e_6.h.h.inl
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.456748
l : Type ?u.456751
m : Type u_3
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
h : j' = j
⊢ ↑(stdBasis R (fun x => R) j) 1 j' = 1

case h.e_6.h.h.inr
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.456748
l : Type ?u.456751
m : Type u_3
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
h : ¬j' = j
⊢ ↑(stdBasis R (fun x => R) j) 1 j' = 0
case h.e_6.h.h
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.456748
l : Type ?u.456751
m : Type u_3
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
⊢ ↑(stdBasis R (fun x => R) j) 1 j' = if j' = j then 1 else 0
split_ifs with h
no goals
case h.e_6.h.h.inr
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.456748
l : Type ?u.456751
m : Type u_3
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
h : ¬j' = j
⊢ ↑(stdBasis R (fun x => R) j) 1 j' = 0
apply stdBasis_ne _ _ _ _ h
no goals
case h.e_6.h.h.inl
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.456748
l : Type ?u.456751
m : Type u_3
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
h : j' = j
⊢ ↑(stdBasis R (fun x => R) j) 1 j' = 1
rw [h, stdBasis_same]