case a.h.a
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
⊢ charmatrix (↑(reindex e e) M) = ↑(reindex e e) (charmatrix M)
ext (i j x)
case pos
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
h : i = j
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x

case neg
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
h : ¬i = j
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
case a.h.a
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
by_cases h : i = j
no goals
case pos
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
h : i = j
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x

case neg
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
h : ¬i = j
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
all_goals simp [h]
no goals
case neg
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
h : ¬i = j
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
simp [h]