∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (B₂ : LinearMap.BilinForm R₁ (n → R₁)), ((LinearMap.BilinForm.toMatrixAux fun j => Pi.single j 1) B₂).toBilin'Aux = B₂