R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ ∑ x : n × n, M x.fst x.snd • Matrix.map (fun i' j' => if x.fst = i' ∧ x.snd = j' then 1 else 0) ↑(algebraMap R A) = M
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ ↑(toFunAlgHom R A n) (invFun R A n M) = M
simp only [invFun, AlgHom.map_sum, stdBasisMatrix, apply_ite ↑(algebraMap R A), smul_eq_mul,
  mul_boole, toFunAlgHom_apply, RingHom.map_zero, RingHom.map_one, Matrix.map_apply,
  Pi.smul_def]
case h.e'_3
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ M =
    ∑ x : n,
      ∑ y : n,
        M (x, y).fst (x, y).snd •
          Matrix.map (fun i' j' => if (x, y).fst = i' ∧ (x, y).snd = j' then 1 else 0) ↑(algebraMap R A)
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ ∑ x : n × n, M x.fst x.snd • Matrix.map (fun i' j' => if x.fst = i' ∧ x.snd = j' then 1 else 0) ↑(algebraMap R A) = M
convert Finset.sum_product (β := Matrix n n A)
case h.e'_3
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ ∑ i : n, ∑ j : n, stdBasisMatrix i j (M i j) =
    ∑ x : n,
      ∑ y : n,
        M (x, y).fst (x, y).snd •
          Matrix.map (fun i' j' => if (x, y).fst = i' ∧ (x, y).snd = j' then 1 else 0) ↑(algebraMap R A)
case h.e'_3
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ M =
    ∑ x : n,
      ∑ y : n,
        M (x, y).fst (x, y).snd •
          Matrix.map (fun i' j' => if (x, y).fst = i' ∧ (x, y).snd = j' then 1 else 0) ↑(algebraMap R A)
conv_lhs => rw [matrix_eq_sum_std_basis M]
case h.e'_3
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
i : n
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
a b : n
⊢ stdBasisMatrix i j (M i j) a b =
    (M (i, j).fst (i, j).snd •
        Matrix.map (fun i' j' => if (i, j).fst = i' ∧ (i, j).snd = j' then 1 else 0) ↑(algebraMap R A))
      a b
case h.e'_3
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ ∑ i : n, ∑ j : n, stdBasisMatrix i j (M i j) =
    ∑ x : n,
      ∑ y : n,
        M (x, y).fst (x, y).snd •
          Matrix.map (fun i' j' => if (x, y).fst = i' ∧ (x, y).snd = j' then 1 else 0) ↑(algebraMap R A)
refine Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => Matrix.ext fun a b => ?_
case h.e'_3
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
i : n
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
a b : n
⊢ (if i = a ∧ j = b then M i j else 0) = M i j • ↑(algebraMap R A) (if i = a ∧ j = b then 1 else 0)
case h.e'_3
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
i : n
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
a b : n
⊢ stdBasisMatrix i j (M i j) a b =
    (M (i, j).fst (i, j).snd •
        Matrix.map (fun i' j' => if (i, j).fst = i' ∧ (i, j).snd = j' then 1 else 0) ↑(algebraMap R A))
      a b
simp only [stdBasisMatrix, smul_apply, Matrix.map_apply]
no goals
case h.e'_3
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
i : n
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
a b : n
⊢ (if i = a ∧ j = b then M i j else 0) = M i j • ↑(algebraMap R A) (if i = a ∧ j = b then 1 else 0)
split_ifs <;> aesop