-- Mathlib/Algebra/Azumaya/Matrix.lean
lemma AlgHom.mulLeftRightMatrix.comp_inv :
    (AlgHom.mulLeftRight R (Matrix n n R)).toLinearMap.comp
    (AlgHom.mulLeftRightMatrix_inv R n) = .id

Proof state:
case h.a
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
i j k l : n
⊢ (∑ x : (n × n) × n × n,
        f (stdBasisMatrix x.1.2 x.2.1 1) x.1.1 x.2.2 •
          ((mulLeftRight R (Matrix n n R)).toLinearMap
              (stdBasisMatrix x.1.1 x.1.2 1 ⊗ₜ[R] op (stdBasisMatrix x.2.1 x.2.2 1)))
            (stdBasisMatrix i j 1))
      k l =
    f (stdBasisMatrix i j 1) k l

Tactic:
simp [sum_apply, Matrix.mul_apply, Finset.sum_mul, Finset.mul_sum, stdBasisMatrix,
  Fintype.sum_prod_type, ite_and]

Result:
no goals

Proof state:
case h
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
⊢ ∀ (i : n × n),
    (((mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ mulLeftRightMatrix_inv R n) f) ((stdBasis R n n) i) =
      (LinearMap.id f) ((stdBasis R n n) i)

Tactic:
intro ⟨i, j⟩

Result:
case h
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
i j : n
⊢ (((mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ mulLeftRightMatrix_inv R n) f) ((stdBasis R n n) (i, j)) =
    (LinearMap.id f) ((stdBasis R n n) (i, j))

Proof state:
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ (mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ mulLeftRightMatrix_inv R n = LinearMap.id

Tactic:
ext f : 1

Result:
case h
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
⊢ ((mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ mulLeftRightMatrix_inv R n) f = LinearMap.id f

Proof state:
case h
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
i j : n
⊢ ∑ x : (n × n) × n × n,
      f (stdBasisMatrix x.1.2 x.2.1 1) x.1.1 x.2.2 •
        ((mulLeftRight R (Matrix n n R)).toLinearMap
            (stdBasisMatrix x.1.1 x.1.2 1 ⊗ₜ[R] op (stdBasisMatrix x.2.1 x.2.2 1)))
          (stdBasisMatrix i j 1) =
    f (stdBasisMatrix i j 1)

Tactic:
ext k l

Result:
case h.a
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
i j k l : n
⊢ (∑ x : (n × n) × n × n,
        f (stdBasisMatrix x.1.2 x.2.1 1) x.1.1 x.2.2 •
          ((mulLeftRight R (Matrix n n R)).toLinearMap
              (stdBasisMatrix x.1.1 x.1.2 1 ⊗ₜ[R] op (stdBasisMatrix x.2.1 x.2.2 1)))
            (stdBasisMatrix i j 1))
      k l =
    f (stdBasisMatrix i j 1) k l

Proof state:
case h
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
⊢ ((mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ mulLeftRightMatrix_inv R n) f = LinearMap.id f

Tactic:
apply Basis.ext (Matrix.stdBasis _ _ _)

Result:
case h
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
⊢ ∀ (i : n × n),
    (((mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ mulLeftRightMatrix_inv R n) f) ((stdBasis R n n) i) =
      (LinearMap.id f) ((stdBasis R n n) i)

Proof state:
case h
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
i j : n
⊢ (((mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ mulLeftRightMatrix_inv R n) f) ((stdBasis R n n) (i, j)) =
    (LinearMap.id f) ((stdBasis R n n) (i, j))

Tactic:
simp only [LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, map_sum,
  _root_.map_smul, stdBasis_eq_stdBasisMatrix, LinearMap.coeFn_sum, Finset.sum_apply,
  LinearMap.smul_apply, LinearMap.id_coe, id_eq]

Result:
case h
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
i j : n
⊢ ∑ x : (n × n) × n × n,
      f (stdBasisMatrix x.1.2 x.2.1 1) x.1.1 x.2.2 •
        ((mulLeftRight R (Matrix n n R)).toLinearMap
            (stdBasisMatrix x.1.1 x.1.2 1 ⊗ₜ[R] op (stdBasisMatrix x.2.1 x.2.2 1)))
          (stdBasisMatrix i j 1) =
    f (stdBasisMatrix i j 1)