Type inference errors on has_inner of a derived inner space

Stream: lean4

[Quarrie]

class tensor_inner_family (𝕜 : Type u) (α : Type v) (X : α -> Type w) [is_R_or_C 𝕜] [tensor_product_family 𝕜 α X] :=
  (to_inner_product_space : ∀ (a : α), (inner_product_space 𝕜 (X a)))
  (inner_tensor_distr : ∀ (a b : α) (x y : X a) (z w : X b), (has_inner.inner (tensor_product_family.pr a b x z) (tensor_product_family.pr a b y w)) == (has_inner.inner x y) * (has_inner.inner z w))
  (norm_comm_inc : ∀ (a b : α) (x : X a) (y : X b), ∥(tensor_product_family.pr a b x y)∥ == ∥(tensor_product_family.pr b a y x)∥)

where tensor_product_family is defined above and equips an indexed family of types with a tensor product operation. No matter how I attempt to phrase the second axiom, the type checker refuses to let the inner product on the product space through. I suspect it may be the fault of a ridiculous syntax error I'm not seeing, since when I phrase it directly in terms of the product space ( (inner_tensor_distr : ∀ (a b : α) (x y : X a) (z w : X b), (X (tensor_product_family.prₜ a b)).has_inner.inner (tensor_product_family.pr a b x z) (tensor_product_family.pr a b y w)) == (has_inner.inner x y) * (has_inner.inner z w))) it fails in roughly the same location but on a different syntax element. Any tips would be greatly appreciated.

[Kevin Buzzard]

Just to confirm -- this is Lean 3, right? If so, you're in the wrong stream (and I forget who can move messages to, say, #maths , which would be more appropriate if I'm right).