-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
n : Type w
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : Invertible (α := R) 2
Q : QuadraticForm R (n → R)
i j : n
a :
  Eq.{u_3 + 1} (α := R)
    (Matrix.transpose
        (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
            (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
          (((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
                QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
              (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
            Q))
        i j :
      R)
    (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
          (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
              QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
            (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
          Q)
        i j :
      R)
a₁ :
  Eq.{u_3 + 1} (α := R)
    (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
          (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
              QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
            (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
          Q)
        j i :
      R)
    (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
          (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
              QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
            (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
          Q)
        i j :
      R)
a₂ :
  Eq.{u_3 + 1} (α := R)
    (((((((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
                        QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
                      (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
                    Q :
                  BilinMap R (n → R) R) :
                (a : n → R) → (n → R) →ₗ[R] R)
              (Pi.single (M := fun (a : n) ↦ R) j 1) :
            (n → R) →ₗ[R] R) :
          (a : n → R) → R)
        (Pi.single (M := fun (a : n) ↦ R) i 1) :
      R)
    (((LinearMap.toMatrix₂' R : ((n → R) →ₗ[R] (n → R) →ₗ[R] R) ≃ₗ[R] Matrix n n R) :
          (a : (n → R) →ₗ[R] (n → R) →ₗ[R] R) → Matrix n n R)
        (((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
              QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
            (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
          Q)
        i j :
      R)
a₃ :
  Eq.{u_3 + 1} (α := R)
    (((((((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
                        QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
                      (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
                    Q :
                  BilinMap R (n → R) R) :
                (a : n → R) → (n → R) →ₗ[R] R)
              (Pi.single (M := fun (a : n) ↦ R) j 1) :
            (n → R) →ₗ[R] R) :
          (a : n → R) → R)
        (Pi.single (M := fun (a : n) ↦ R) i 1) :
      R)
    (((((((QuadraticMap.associated (R := R) (M := n → R) (N := R) :
                        QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
                      (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
                    Q :
                  BilinMap R (n → R) R) :
                (a : n → R) → (n → R) →ₗ[R] R)
              (Pi.single (M := fun (a : n) ↦ R) i 1) :
            (n → R) →ₗ[R] R) :
          (a : n → R) → R)
        (Pi.single (M := fun (a : n) ↦ R) j 1) :
      R)
⊢ Q.toMatrix'.transpose i j = Q.toMatrix' i j
have a₄ : Eq.{u_3 + 1} (α := R)
  (((((((QuadraticMap.associatedHom R (R := R) (M := n → R) (N := R) :
                      QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
                    (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
                  Q :
                BilinMap R (n → R) R) :
              (a : n → R) → (n → R) →ₗ[R] R)
            (Pi.single (M := fun (a : n) ↦ R) i 1) :
          (n → R) →ₗ[R] R) :
        (a : n → R) → R)
      (Pi.single (M := fun (a : n) ↦ R) j 1) :
    R)
  (((((((QuadraticMap.associated (R := R) (M := n → R) (N := R) : QuadraticMap R (n → R) R →ₗ[R] BilinMap R (n → R) R) :
                    (a : QuadraticMap R (n → R) R) → BilinMap R (n → R) R)
                  Q :
                BilinMap R (n → R) R) :
              (a : n → R) → (n → R) →ₗ[R] R)
            (Pi.single (M := fun (a : n) ↦ R) i 1) :
          (n → R) →ₗ[R] R) :
        (a : n → R) → R)
      (Pi.single (M := fun (a : n) ↦ R) j 1) :
    R)
Tactic: rw [toMatrix', Matrix.transpose_apply, LinearMap.toMatrix₂'_apply, LinearMap.toMatrix₂'_apply,
    ← QuadraticMap.associated_isSymm]