∀ (stx : Lean.TSyntax `tactic) (msg : Lean.MessageData) (stx_1 : Lean.TSyntax `tactic) (msg_1 : Lean.MessageData),
  (Mathlib.TacticAnalysis.TerminalReplacementOutcome.error✝ stx msg =
      Mathlib.TacticAnalysis.TerminalReplacementOutcome.error✝¹ stx_1 msg_1) =
    (stx = stx_1 ∧ msg = msg_1)