{𝕜 : Type u_4} →
  {F : Type u_5} →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module 𝕜 F] →
          {motive : PreInnerProductSpace.Core 𝕜 F → Sort u} →
            (t : PreInnerProductSpace.Core 𝕜 F) →
              ((toInner : Inner 𝕜 F) →
                  (conj_inner_symm : ∀ (x y : F), (starRingEnd 𝕜) (inner 𝕜 y x) = inner 𝕜 x y) →
                    (re_inner_nonneg : ∀ (x : F), 0 ≤ RCLike.re (inner 𝕜 x x)) →
                      (add_left : ∀ (x y z : F), inner 𝕜 (x + y) z = inner 𝕜 x z + inner 𝕜 y z) →
                        (smul_left : ∀ (x y : F) (r : 𝕜), inner 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner 𝕜 x y) →
                          motive
                            { toInner := toInner, conj_inner_symm := conj_inner_symm,
                              re_inner_nonneg := re_inner_nonneg, add_left := add_left, smul_left := smul_left }) →
                motive t