invalid pattern, constructor or constant marked with '[match

Stream: mathlib4

[Yury G. Kudryashov]

I get a strange error at https://github.com/leanprover-community/sphere-eversion/blob/lean4/SphereEversion/ToMathlib/Analysis/Calculus.lean#L126 :

invalid pattern, constructor or constant marked with '[match_pattern]' expected

What does it mean? How do I fix this?

[Yury G. Kudryashov]

More details: the error disappears if I replace ψ with a.

[Yury G. Kudryashov]

The offending theorem was

nonrec theorem Differentiable.fderiv_partial_fst {φ : E → F → G}
    (hF : Differentiable 𝕜 (uncurry φ)) :
    (↿(∂₁ 𝕜 φ)) = (fun (ψ : (E × F →L[𝕜] G)) ↦ ψ.comp (inl 𝕜 E F)) ∘ (fderiv 𝕜 <| uncurry φ) := by
  ext1 ⟨y, t⟩; exact fderiv_partial_fst (hF ⟨y, t⟩).hasFDerivAt

I fixed compile by using docs#ContinuousLinearMap.precomp

[Yury G. Kudryashov]

Got another error, again with letter ψ. What makes it special?

[Yury G. Kudryashov]

Found it! (Not really) scoped notation in OperatorNorm.

[Yury G. Kudryashov]

#6143