∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} {inst : CommSemiring R} {inst_1 : AddCommMonoid M₁}
  {inst_2 : AddCommMonoid M₂} {inst_3 : AddCommMonoid N} {inst_4 : Module R M₁} {inst_5 : Module R M₂}
  {inst_6 : Module R N} {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {toLinearEquiv : M₁ ≃ₗ[R] M₂}
  {map_app' : ∀ (m : M₁), Q₂ ((↑toLinearEquiv).toFun m) = Q₁ m} {toLinearEquiv_1 : M₁ ≃ₗ[R] M₂}
  {map_app'_1 : ∀ (m : M₁), Q₂ ((↑toLinearEquiv_1).toFun m) = Q₁ m},
  { toLinearEquiv := toLinearEquiv, map_app' := map_app' } =
      { toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 } →
    toLinearEquiv = toLinearEquiv_1