∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] {K L M N : QuadraticModuleCat R} (f : K ⟶ L) (g : M ⟶ N),
  QuadraticModuleCat.Hom.toIsometry (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
    (QuadraticModuleCat.Hom.toIsometry f).tmul (QuadraticModuleCat.Hom.toIsometry g)