universe issues in semiAdjoint.pi_rule

[lecopivo]

The theorem semiAdjoint.pi_rule does not have correct universes as for some reason K and X have the same universe level.

#check semiAdjoint.pi_rule

returns

SciLean.semiAdjoint.pi_rule.{u_3, u_2, u_1} (K : Type u_1) [inst : IsROrC K] {X : Type u_1}
  [inst¹ : SemiInnerProductSpace K X] {ι : Type u_3} [inst² : EnumType ι] {E : ι → Type u_2}
  [inst³ : (i : ι) → SemiInnerProductSpace K (E i)] (f : X → (i : ι) → E i)
  (hf : ∀ (i : ι), HasSemiAdjoint K fun x => f x i) :
  (semiAdjoint K fun x i => f x i) = fun x' =>  ∑ i, semiAdjoint K (fun x => f x i) (x' i)

This cases issue when proving GetElem.getElem.arg_xs.revDerivUpdate_rule_pi