∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {ι₁ : Type u_6}
  {ι₂ : Type u_7} {b₁ : Module.Basis ι₁ 𝕜 E} {b₂ : Module.Basis ι₂ 𝕜 F},
  Orthonormal 𝕜 ⇑b₁ → Orthonormal 𝕜 ⇑b₂ → Orthonormal 𝕜 ⇑(b₁.tensorProduct b₂)