-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.mk.injEq : ∀ (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)