-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.mk.inj : ∀ {textDocumentSync? : Option Lean.Lsp.TextDocumentSyncOptions}
  {completionProvider? : Option Lean.Lsp.CompletionOptions}
  {hoverProvider documentHighlightProvider documentSymbolProvider definitionProvider declarationProvider
    typeDefinitionProvider referencesProvider callHierarchyProvider : Bool}
  {renameProvider? : Option Lean.Lsp.RenameOptions} {workspaceSymbolProvider foldingRangeProvider : Bool}
  {semanticTokensProvider? : Option Lean.Lsp.SemanticTokensOptions}
  {codeActionProvider? : Option Lean.Lsp.CodeActionOptions} {inlayHintProvider? : Option Lean.Lsp.InlayHintOptions}
  {signatureHelpProvider? : Option Lean.Lsp.SignatureHelpOptions}
  {colorProvider? : Option Lean.Lsp.DocumentColorOptions} {experimental? : Option Lean.Lsp.LeanServerCapabilities}
  {textDocumentSync?_1 : Option Lean.Lsp.TextDocumentSyncOptions}
  {completionProvider?_1 : Option Lean.Lsp.CompletionOptions}
  {hoverProvider_1 documentHighlightProvider_1 documentSymbolProvider_1 definitionProvider_1 declarationProvider_1
    typeDefinitionProvider_1 referencesProvider_1 callHierarchyProvider_1 : Bool}
  {renameProvider?_1 : Option Lean.Lsp.RenameOptions} {workspaceSymbolProvider_1 foldingRangeProvider_1 : Bool}
  {semanticTokensProvider?_1 : Option Lean.Lsp.SemanticTokensOptions}
  {codeActionProvider?_1 : Option Lean.Lsp.CodeActionOptions} {inlayHintProvider?_1 : Option Lean.Lsp.InlayHintOptions}
  {signatureHelpProvider?_1 : Option Lean.Lsp.SignatureHelpOptions}
  {colorProvider?_1 : Option Lean.Lsp.DocumentColorOptions} {experimental?_1 : Option Lean.Lsp.LeanServerCapabilities},
  { textDocumentSync? := textDocumentSync?, completionProvider? := completionProvider?, hoverProvider := hoverProvider,
        documentHighlightProvider := documentHighlightProvider, documentSymbolProvider := documentSymbolProvider,
        definitionProvider := definitionProvider, declarationProvider := declarationProvider,
        typeDefinitionProvider := typeDefinitionProvider, referencesProvider := referencesProvider,
        callHierarchyProvider := callHierarchyProvider, renameProvider? := renameProvider?,
        workspaceSymbolProvider := workspaceSymbolProvider, foldingRangeProvider := foldingRangeProvider,
        semanticTokensProvider? := semanticTokensProvider?, codeActionProvider? := codeActionProvider?,
        inlayHintProvider? := inlayHintProvider?, signatureHelpProvider? := signatureHelpProvider?,
        colorProvider? := colorProvider?, experimental? := experimental? } =
      { textDocumentSync? := textDocumentSync?_1, completionProvider? := completionProvider?_1,
        hoverProvider := hoverProvider_1, documentHighlightProvider := documentHighlightProvider_1,
        documentSymbolProvider := documentSymbolProvider_1, definitionProvider := definitionProvider_1,
        declarationProvider := declarationProvider_1, typeDefinitionProvider := typeDefinitionProvider_1,
        referencesProvider := referencesProvider_1, callHierarchyProvider := callHierarchyProvider_1,
        renameProvider? := renameProvider?_1, workspaceSymbolProvider := workspaceSymbolProvider_1,
        foldingRangeProvider := foldingRangeProvider_1, semanticTokensProvider? := semanticTokensProvider?_1,
        codeActionProvider? := codeActionProvider?_1, inlayHintProvider? := inlayHintProvider?_1,
        signatureHelpProvider? := signatureHelpProvider?_1, colorProvider? := colorProvider?_1,
        experimental? := experimental?_1 } →
    textDocumentSync? = textDocumentSync?_1 ∧
      completionProvider? = completionProvider?_1 ∧
        hoverProvider = hoverProvider_1 ∧
          documentHighlightProvider = documentHighlightProvider_1 ∧
            documentSymbolProvider = documentSymbolProvider_1 ∧
              definitionProvider = definitionProvider_1 ∧
                declarationProvider = declarationProvider_1 ∧
                  typeDefinitionProvider = typeDefinitionProvider_1 ∧
                    referencesProvider = referencesProvider_1 ∧
                      callHierarchyProvider = callHierarchyProvider_1 ∧
                        renameProvider? = renameProvider?_1 ∧
                          workspaceSymbolProvider = workspaceSymbolProvider_1 ∧
                            foldingRangeProvider = foldingRangeProvider_1 ∧
                              semanticTokensProvider? = semanticTokensProvider?_1 ∧
                                codeActionProvider? = codeActionProvider?_1 ∧
                                  inlayHintProvider? = inlayHintProvider?_1 ∧
                                    signatureHelpProvider? = signatureHelpProvider?_1 ∧
                                      colorProvider? = colorProvider?_1 ∧ experimental? = experimental?_1