∀ {ctxInfo : Lean.Elab.ContextInfo} {tacticInfo : Lean.Elab.TacticInfo} {useAfter indented : Bool} {priority : ℕ}
  {ctxInfo_1 : Lean.Elab.ContextInfo} {tacticInfo_1 : Lean.Elab.TacticInfo} {useAfter_1 indented_1 : Bool}
  {priority_1 : ℕ},
  { ctxInfo := ctxInfo, tacticInfo := tacticInfo, useAfter := useAfter, indented := indented, priority := priority } =
      { ctxInfo := ctxInfo_1, tacticInfo := tacticInfo_1, useAfter := useAfter_1, indented := indented_1,
        priority := priority_1 } →
    ctxInfo = ctxInfo_1 ∧
      tacticInfo = tacticInfo_1 ∧ useAfter = useAfter_1 ∧ indented = indented_1 ∧ priority = priority_1