{α : Type} →
  {P : Sort u} →
    {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' : 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 := range, fullRange? := fullRange?, severity? := severity?,
                                                      isSilent? := isSilent?, code? := code?, source? := source?,
                                                      message := message, tags? := tags?, leanTags? := leanTags?,
                                                      relatedInformation? := relatedInformation?, data? := data? } =
                                                    { range := range', fullRange? := fullRange?',
                                                      severity? := severity?', isSilent? := isSilent?', code? := code?',
                                                      source? := source?', message := message', tags? := tags?',
                                                      leanTags? := leanTags?',
                                                      relatedInformation? := relatedInformation?', data? := data?' } →
                                                  (range = range' →
                                                      fullRange? = fullRange?' →
                                                        severity? = severity?' →
                                                          isSilent? = isSilent?' →
                                                            code? = code?' →
                                                              source? = source?' →
                                                                message ≍ message' →
                                                                  tags? = tags?' →
                                                                    leanTags? = leanTags?' →
                                                                      relatedInformation? = relatedInformation?' →
                                                                        data? = data?' → P) →
                                                    P