-- Mathlib/RingTheory/MatrixAlgebra.lean
theorem invFun_algebraMap (M : Matrix n n R) : invFun n R A (M.map (algebraMap R A)) = 1 ⊗ₜ M

Proof state:
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ p : n × n, (algebraMap R A) (M p.1 p.2) ⊗ₜ[R] stdBasisMatrix p.1 p.2 1 = 1 ⊗ₜ[R] M

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, smul_tmul, ← tmul_sum, mul_boole]

Result:
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ 1 ⊗ₜ[R] ∑ a : n × n, M a.1 a.2 • stdBasisMatrix a.1 a.2 1 = 1 ⊗ₜ[R] M

Proof state:
case h.e'_3.a.a
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
x✝¹ : n
a✝¹ : x✝¹ ∈ Finset.univ
x✝ : n
a✝ : x✝ ∈ Finset.univ
⊢ stdBasisMatrix x✝¹ x✝ (M x✝¹ x✝) = M (x✝¹, x✝).1 (x✝¹, x✝).2 • stdBasisMatrix (x✝¹, x✝).1 (x✝¹, x✝).2 1

Tactic:
simp

Result:
no goals

Proof state:
case e_n
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ a : n × n, M a.1 a.2 • stdBasisMatrix a.1 a.2 1 = M

Tactic:
conv_rhs => rw [matrix_eq_sum_stdBasisMatrix M]

Result:
case e_n
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ a : n × n, M a.1 a.2 • stdBasisMatrix a.1 a.2 1 = ∑ i : n, ∑ j : n, stdBasisMatrix i j (M i j)

Proof state:
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ 1 ⊗ₜ[R] ∑ a : n × n, M a.1 a.2 • stdBasisMatrix a.1 a.2 1 = 1 ⊗ₜ[R] M

Tactic:
congr

Result:
case e_n
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ a : n × n, M a.1 a.2 • stdBasisMatrix a.1 a.2 1 = M

Proof state:
case e_n
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ a : n × n, M a.1 a.2 • stdBasisMatrix a.1 a.2 1 = ∑ i : n, ∑ j : n, stdBasisMatrix i j (M i j)

Tactic:
convert Finset.sum_product (β := Matrix n n R) ..

Result:
case h.e'_3.a.a
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
x✝¹ : n
a✝¹ : x✝¹ ∈ Finset.univ
x✝ : n
a✝ : x✝ ∈ Finset.univ
⊢ stdBasisMatrix x✝¹ x✝ (M x✝¹ x✝) = M (x✝¹, x✝).1 (x✝¹, x✝).2 • stdBasisMatrix (x✝¹, x✝).1 (x✝¹, x✝).2 1

Proof state:
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ invFun n R A (M.map ⇑(algebraMap R A)) = 1 ⊗ₜ[R] M

Tactic:
dsimp [invFun]

Result:
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ p : n × n, (algebraMap R A) (M p.1 p.2) ⊗ₜ[R] stdBasisMatrix p.1 p.2 1 = 1 ⊗ₜ[R] M