{motive : Lean.Lsp.DocumentFilter → Sort u} →
  ((language? scheme? pattern? : Option String) →
      motive { language? := language?, scheme? := scheme?, pattern? := pattern? }) →
    (t : Lean.Lsp.DocumentFilter) → motive t