case mk
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.77160
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
⊢ toMatrix (reindexEquiv e { i := t_i, j := t_j, hij := hij✝, c := c✝ }) =
    ↑(reindexAlgEquiv R e) (toMatrix { i := t_i, j := t_j, hij := hij✝, c := c✝ })
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.77160
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t : TransvectionStruct n R
⊢ toMatrix (reindexEquiv e t) = ↑(reindexAlgEquiv R e) (toMatrix t)
rcases t with ⟨t_i, t_j, _⟩
case mk.a.h
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.77160
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
⊢ toMatrix (reindexEquiv e { i := t_i, j := t_j, hij := hij✝, c := c✝ }) a b =
    ↑(reindexAlgEquiv R e) (toMatrix { i := t_i, j := t_j, hij := hij✝, c := c✝ }) a b
case mk
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.77160
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
⊢ toMatrix (reindexEquiv e { i := t_i, j := t_j, hij := hij✝, c := c✝ }) =
    ↑(reindexAlgEquiv R e) (toMatrix { i := t_i, j := t_j, hij := hij✝, c := c✝ })
ext (a b)
case mk.a.h
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.77160
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
⊢ (1 + stdBasisMatrix (↑e t_i) (↑e t_j) c✝) a b = (1 + stdBasisMatrix t_i t_j c✝) (↑e.symm a) (↑e.symm b)
case mk.a.h
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.77160
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
⊢ toMatrix (reindexEquiv e { i := t_i, j := t_j, hij := hij✝, c := c✝ }) a b =
    ↑(reindexAlgEquiv R e) (toMatrix { i := t_i, j := t_j, hij := hij✝, c := c✝ }) a b
simp only [reindexEquiv, transvection, mul_boole, Algebra.id.smul_eq_mul, toMatrix_mk,
  submatrix_apply, reindex_apply, DMatrix.add_apply, Pi.smul_apply, reindexAlgEquiv_apply]
no goals
case mk.a.h
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.77160
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
⊢ (1 + stdBasisMatrix (↑e t_i) (↑e t_j) c✝) a b = (1 + stdBasisMatrix t_i t_j c✝) (↑e.symm a) (↑e.symm b)
by_cases ha : e t_i = a <;> by_cases hb : e t_j = b <;> by_cases hab : a = b <;>
  simp [ha, hb, hab, ← e.apply_eq_iff_eq_symm_apply, stdBasisMatrix]