∀ (𝕜 : Type u_2) [inst : RCLike 𝕜] (E : Type u_1) [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E], Fintype.card ↥(Classical.choose ⋯) = Fintype.card ↥(Classical.choose ⋯)