-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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)
⊢ (toMatrix b Q).transpose i j = toMatrix b Q i j
have 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)
Tactic: rw [toMatrix, Matrix.transpose_apply, LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂_apply,
    ← QuadraticMap.associated_isSymm]