∀ {α : Type} {range : Lean.Lsp.Range} {fullRange? : Option Lean.Lsp.Range}
  {severity? : Option Lean.Lsp.DiagnosticSeverity} {isSilent? : Option Bool} {code? : Option Lean.Lsp.DiagnosticCode}
  {source? : Option String} {message : α} {tags? : Option (Array Lean.Lsp.DiagnosticTag)}
  {leanTags? : Option (Array Lean.Lsp.LeanDiagnosticTag)}
  {relatedInformation? : Option (Array Lean.Lsp.DiagnosticRelatedInformation)} {data? : Option Lean.Json}
  {range_1 : Lean.Lsp.Range} {fullRange?_1 : Option Lean.Lsp.Range} {severity?_1 : Option Lean.Lsp.DiagnosticSeverity}
  {isSilent?_1 : Option Bool} {code?_1 : Option Lean.Lsp.DiagnosticCode} {source?_1 : Option String} {message_1 : α}
  {tags?_1 : Option (Array Lean.Lsp.DiagnosticTag)} {leanTags?_1 : Option (Array Lean.Lsp.LeanDiagnosticTag)}
  {relatedInformation?_1 : Option (Array Lean.Lsp.DiagnosticRelatedInformation)} {data?_1 : Option Lean.Json},
  { range := range, fullRange? := fullRange?, severity? := severity?, isSilent? := isSilent?, code? := code?,
        source? := source?, message := message, tags? := tags?, leanTags? := leanTags?,
        relatedInformation? := relatedInformation?, data? := data? } =
      { range := range_1, fullRange? := fullRange?_1, severity? := severity?_1, isSilent? := isSilent?_1,
        code? := code?_1, source? := source?_1, message := message_1, tags? := tags?_1, leanTags? := leanTags?_1,
        relatedInformation? := relatedInformation?_1, data? := data?_1 } →
    range = range_1 ∧
      fullRange? = fullRange?_1 ∧
        severity? = severity?_1 ∧
          isSilent? = isSilent?_1 ∧
            code? = code?_1 ∧
              source? = source?_1 ∧
                message = message_1 ∧
                  tags? = tags?_1 ∧
                    leanTags? = leanTags?_1 ∧ relatedInformation? = relatedInformation?_1 ∧ data? = data?_1