push away the sorry

src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import linear_algebra.bilinear_form.tensor_product
+import linear_algebra.quadratic_form.basic
+import data.is_R_or_C.basic
 
 universes u v w
 variables {ι : Type*} {R : Type*} {M₁ M₂ : Type*}
@@ -30,4 +32,15 @@ tensor_product.ext' $ λ x₁ x₂, tensor_product.ext' $ λ y₁ y₂,
 
 end comm_semiring
 
-end bilin_form
+end bilin_form
+
+namespace quadratic_form
+variables [add_comm_group M₁] [add_comm_group M₂]
+variables [module ℝ M₁] [module ℝ M₂]
+
+lemma _root_.quadratic_form.pos_def.tmul {B₁ : bilin_form ℝ M₁} {B₂ : bilin_form ℝ M₂}
+  (hB₁ : B₁.to_quadratic_form.pos_def) (hB₂ : B₂.to_quadratic_form.pos_def) :
+  (B₁.tmul B₂).to_quadratic_form.pos_def :=
+sorry
+
+end quadratic_form

src/for_mathlib/linear_algebra/tensor_product/inner_product_space.lean

@@ -7,21 +7,23 @@ variables [inner_product_space ℝ V] [inner_product_space ℝ W]
 
 open_locale tensor_product
 
+lemma is_symm_bilin_form_of_real_inner : (bilin_form_of_real_inner : bilin_form ℝ V).is_symm :=
+λ x y, real_inner_comm _ _
+
+lemma pos_def_bilin_form_of_real_inner :
+  (bilin_form_of_real_inner : bilin_form ℝ V).to_quadratic_form.pos_def :=
+λ x hx, lt_of_le_of_ne' real_inner_self_nonneg (inner_self_ne_zero.mpr hx)
+
 noncomputable instance : inner_product_space.core ℝ (V ⊗[ℝ] W) :=
 { inner := λ x y, bilin_form_of_real_inner.tmul bilin_form_of_real_inner x y,
   conj_symm := λ x y,
-    bilin_form.is_symm.tmul (λ x y, real_inner_comm _ _) (λ x y, real_inner_comm _ _) y x,
+    bilin_form.is_symm.tmul is_symm_bilin_form_of_real_inner is_symm_bilin_form_of_real_inner y x,
   nonneg_re := λ x, begin
     simp only [is_R_or_C.re_to_real],
-    induction x using tensor_product.induction_on with v w x y hx hy,
-    { simp only [bilin_form.zero_right] },
-    { simp only [bilin_form.tmul.equations._eqn_1, bilin_form_of_real_inner_apply,
-        bilin_form.tensor_distrib_tmul],
-      exact mul_nonneg real_inner_self_nonneg real_inner_self_nonneg, },
-    { simp only [bilin_form.add_left, bilin_form.add_right],
-      sorry },
+    exact (pos_def_bilin_form_of_real_inner.tmul pos_def_bilin_form_of_real_inner).nonneg _, 
   end,
-  definite := sorry,
+  definite := λ x hx,
+    (pos_def_bilin_form_of_real_inner.tmul pos_def_bilin_form_of_real_inner).anisotropic _ hx,
   add_left := bilin_form.add_left,
   smul_left := λ _ _ _, bilin_form.bilin_smul_left _ _ _ _ }