case a.h
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
⊢ ↑(stdBasis R n m) (i, j) = stdBasisMatrix i j 1
ext (a b)
case pos
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b

case neg
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : ¬j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b

case pos
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b

case neg
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : ¬j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
case a.h
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
by_cases hi : i = a <;> by_cases hj : j = b
case pos
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := a, snd := b } a b = 1
case pos
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
simp [stdBasis, hi, hj, Basis.coe_reindex, comp_apply, Equiv.sigmaEquivProd_symm_apply,
  StdBasisMatrix.apply_same]
case pos
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := a, snd := b }.fst) (↑(Pi.basisFun R m) { fst := a, snd := b }.snd) a
      b =
    1
case pos
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := a, snd := b } a b = 1
erw [Pi.basis_apply]
no goals
case pos
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := a, snd := b }.fst) (↑(Pi.basisFun R m) { fst := a, snd := b }.snd) a
      b =
    1
simp
case neg
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : ¬j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := a, snd := j } a b = 0
case neg
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : ¬j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
simp only [stdBasis, hi, Basis.coe_reindex, comp_apply, Equiv.sigmaEquivProd_symm_apply,
  hj, and_false, not_false_iff, StdBasisMatrix.apply_of_ne]
case neg
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : ¬j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := a, snd := j }.fst) (↑(Pi.basisFun R m) { fst := a, snd := j }.snd) a
      b =
    0
case neg
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : ¬j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := a, snd := j } a b = 0
erw [Pi.basis_apply]
no goals
case neg
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : ¬j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := a, snd := j }.fst) (↑(Pi.basisFun R m) { fst := a, snd := j }.snd) a
      b =
    0
simp [hj]
case pos
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := i, snd := b } a b = 0
case pos
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
simp only [stdBasis, hj, Basis.coe_reindex, comp_apply, Equiv.sigmaEquivProd_symm_apply,
  hi, and_true, not_false_iff, StdBasisMatrix.apply_of_ne]
case pos
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := i, snd := b }.fst) (↑(Pi.basisFun R m) { fst := i, snd := b }.snd) a
      b =
    0
case pos
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := i, snd := b } a b = 0
erw [Pi.basis_apply]
no goals
case pos
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := i, snd := b }.fst) (↑(Pi.basisFun R m) { fst := i, snd := b }.snd) a
      b =
    0
simp [hi, hj, Ne.symm hi, LinearMap.stdBasis_ne]
case neg
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : ¬j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := i, snd := j } a b = 0
case neg
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : ¬j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
simp only [stdBasis, Basis.coe_reindex, comp_apply, Equiv.sigmaEquivProd_symm_apply,
  hi, hj, and_self, not_false_iff, StdBasisMatrix.apply_of_ne]
case neg
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : ¬j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := i, snd := j }.fst) (↑(Pi.basisFun R m) { fst := i, snd := j }.snd) a
      b =
    0
case neg
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : ¬j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := i, snd := j } a b = 0
erw [Pi.basis_apply]
no goals
case neg
R : Type u_3
m : Type u_2
n : Type u_1
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : ¬j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := i, snd := j }.fst) (↑(Pi.basisFun R m) { fst := i, snd := j }.snd) a
      b =
    0
simp [hi, hj, Ne.symm hj, Ne.symm hi, LinearMap.stdBasis_ne]