∀ (name : String) (kind : Lean.Lsp.SymbolKind) (tags? : Option (Array Lean.Lsp.SymbolTag)) (detail? : Option String)
  (uri : Lean.Lsp.DocumentUri) (range selectionRange : Lean.Lsp.Range) (data? : Option Lean.Json) (name_1 : String)
  (kind_1 : Lean.Lsp.SymbolKind) (tags?_1 : Option (Array Lean.Lsp.SymbolTag)) (detail?_1 : Option String)
  (uri_1 : Lean.Lsp.DocumentUri) (range_1 selectionRange_1 : Lean.Lsp.Range) (data?_1 : Option Lean.Json),
  ({ name := name, kind := kind, tags? := tags?, detail? := detail?, uri := uri, range := range,
        selectionRange := selectionRange, data? := data? } =
      { name := name_1, kind := kind_1, tags? := tags?_1, detail? := detail?_1, uri := uri_1, range := range_1,
        selectionRange := selectionRange_1, data? := data?_1 }) =
    (name = name_1 ∧
      kind = kind_1 ∧
        tags? = tags?_1 ∧
          detail? = detail?_1 ∧ uri = uri_1 ∧ range = range_1 ∧ selectionRange = selectionRange_1 ∧ data? = data?_1)