-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
N : Type u_5
n : Type w
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Invertible (α := R) 2
inst_4 : AddCommGroup N
inst_5 : Module R N
b : Basis n R N
Q : QuadraticForm R N
i j : n
a :
  Eq.{u_3 + 1} (α := R)
    (Matrix.transpose
        ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
          (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
                QuadraticMap R N R →ₗ[R] BilinMap R N R) :
              (a : QuadraticMap R N R) → BilinMap R N R)
            Q))
        i j :
      R)
    ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
              QuadraticMap R N R →ₗ[R] BilinMap R N R) :
            (a : QuadraticMap R N R) → BilinMap R N R)
          Q)
        i j :
      R)
a₁ :
  Eq.{u_3 + 1} (α := R)
    ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
              QuadraticMap R N R →ₗ[R] BilinMap R N R) :
            (a : QuadraticMap R N R) → BilinMap R N R)
          Q)
        j i :
      R)
    ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
              QuadraticMap R N R →ₗ[R] BilinMap R N R) :
            (a : QuadraticMap R N R) → BilinMap R N R)
          Q)
        i j :
      R)
a₂ :
  Eq.{u_3 + 1} (α := R)
    (((((((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
                        QuadraticMap R N R →ₗ[R] BilinMap R N R) :
                      (a : QuadraticMap R N R) → BilinMap R N R)
                    Q :
                  BilinMap R N R) :
                (a : N) → N →ₗ[R] R)
              ((b : (a : n) → N) j) :
            N →ₗ[R] R) :
          (a : N) → R)
        ((b : (a : n) → N) i : N) :
      R)
    ((LinearMap.toMatrix₂ b b : (a : N →ₗ[R] N →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
              QuadraticMap R N R →ₗ[R] BilinMap R N R) :
            (a : QuadraticMap R N R) → BilinMap R N R)
          Q)
        i j :
      R)
a₃ :
  Eq.{u_3 + 1} (α := R)
    (((((((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
                        QuadraticMap R N R →ₗ[R] BilinMap R N R) :
                      (a : QuadraticMap R N R) → BilinMap R N R)
                    Q :
                  BilinMap R N R) :
                (a : N) → N →ₗ[R] R)
              ((b : (a : n) → N) j) :
            N →ₗ[R] R) :
          (a : N) → R)
        ((b : (a : n) → N) i : N) :
      R)
    (((((((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
                        QuadraticMap R N R →ₗ[R] BilinMap R N R) :
                      (a : QuadraticMap R N R) → BilinMap R N R)
                    Q :
                  BilinMap R N R) :
                (a : N) → N →ₗ[R] R)
              ((b : (a : n) → N) i) :
            N →ₗ[R] R) :
          (a : N) → R)
        ((b : (a : n) → N) j : N) :
      R)
a₄ a₅ :
  Eq.{u_3 + 1} (α := R)
    (((((((QuadraticMap.associatedHom.{u_3, u_3, u_5, u_3} R (R := R) (M := N) (N := R) :
                        QuadraticMap R N R →ₗ[R] BilinMap R N R) :
                      (a : QuadraticMap R N R) → BilinMap R N R)
                    Q :
                  BilinMap R N R) :
                (a : N) → N →ₗ[R] R)
              ((b : (a : n) → N) i) :
            N →ₗ[R] R) :
          (a : N) → R)
        ((b : (a : n) → N) j : N) :
      R)
    (((((((QuadraticMap.associated.{u_3, u_5, u_3} (R := R) (M := N) (N := R) :
                        QuadraticMap R N R →ₗ[R] BilinMap R N R) :
                      (a : QuadraticMap R N R) → BilinMap R N R)
                    Q :
                  BilinMap R N R) :
                (a : N) → N →ₗ[R] R)
              ((b : (a : n) → N) i) :
            N →ₗ[R] R) :
          (a : N) → R)
        ((b : (a : n) → N) j : N) :
      R)
⊢ (toMatrix b Q).transpose i j = toMatrix b Q i j

Tactic:
rw [toMatrix, Matrix.transpose_apply, LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂_apply,
    ← QuadraticMap.associated_isSymm]

Premises used: QuadraticForm.toMatrix, LinearMap.toMatrix₂_apply, Matrix.transpose_apply, QuadraticMap.associated_isSymm