-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst : CommSemiring R
inst_1 : Semiring R₁
inst_2 : Semiring S₁
inst_3 : Semiring R₂
inst_4 : Semiring S₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
inst_7 : Module S₁ N₂
inst_8 : Module S₂ N₂
inst_9 : SMulCommClass S₁ R N₂
inst_10 : SMulCommClass S₂ R N₂
inst_11 : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst_12 : Fintype n
inst_13 : Fintype m
inst_14 : DecidableEq n
inst_15 : DecidableEq m
f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
i : n
j : m
simp_rw :
  Eq.{u_10 + 1} (α := N₂)
    ((((toLinearMap₂'Aux σ₁ σ₂
                  (((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
                          Pi.single (M := fun (j : m) ↦ R₂) j 1 :
                        (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
                      (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
                    f) :
                (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂)
              (Pi.single (M := fun (j : n) ↦ R₁) i 1) :
            (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        (Pi.single (M := fun (j : m) ↦ R₂) j 1) :
      N₂)
    ((((f : (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂) (Pi.single (M := fun (j : n) ↦ R₁) i 1) : (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        (Pi.single (M := fun (j : m) ↦ R₂) j 1) :
      N₂)
simp_rw₁ :
  Eq.{u_10 + 1} (α := N₂)
    (((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
              Pi.single (M := fun (j : m) ↦ R₂) j 1 :
            (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
          (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
        f i j :
      N₂)
    ((((f : (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂) (Pi.single (M := fun (j : n) ↦ R₁) i 1) : (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        (Pi.single (M := fun (j : m) ↦ R₂) j 1) :
      N₂)
⊢ Eq.{u_10 + 1} (α := N₂)
    ((((toLinearMap₂'Aux σ₁ σ₂
                  (((toMatrix₂Aux R (fun (i : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) i 1) fun (j : m) ↦
                          Pi.single (M := fun (j : m) ↦ R₂) j 1 :
                        (((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂) :
                      (a : ((j : n) → R₁) →ₛₗ[σ₁] ((j : m) → R₂) →ₛₗ[σ₂] N₂) → Matrix n m N₂)
                    f) :
                (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂)
              ((Pi.basisFun R₁ n : (a : n) → n → R₁) i) :
            (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        ((Pi.basisFun R₂ m : (a : m) → m → R₂) j : m → R₂) :
      N₂)
    ((((f : (a : n → R₁) → (m → R₂) →ₛₗ[σ₂] N₂) ((Pi.basisFun R₁ n : (a : n) → n → R₁) i) : (m → R₂) →ₛₗ[σ₂] N₂) :
          (a : m → R₂) → N₂)
        ((Pi.basisFun R₂ m : (a : m) → m → R₂) j : m → R₂) :
      N₂)

Tactic:
simp_rw [Pi.basisFun_apply, Matrix.toLinearMap₂'Aux_single, LinearMap.toMatrix₂Aux_apply]

Premises used: Matrix.toLinearMap₂'Aux_single, Pi.basisFun_apply, LinearMap.toMatrix₂Aux_apply