{𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {K : Submodule 𝕜 E} →
            {motive : K.HasOrthogonalProjection → Sort u} →
              (t : K.HasOrthogonalProjection) →
                ((exists_orthogonal : ∀ (v : E), ∃ w ∈ K, v - w ∈ Kᗮ) → motive ⋯) → motive t