-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkChainResult.go.eq_def : ∀ (tac1 : Lean.TSyntax `tactic) (tacss2 : Array (Array (Lean.TSyntax `tactic))) (i : ℕ)
  (acc : List (Lean.TSyntax `tactic)) (kind? : Option Lean.SyntaxNodeKind),
  Lean.Elab.Tactic.Try.mkChainResult.go✝ tac1 tacss2 i acc kind? = do
    let __do_lift ← get
    let __do_lift_1 ← read
    if __do_lift.size > __do_lift_1.config.max then pure ()
      else
        if h : i < tacss2.size then
          if tacss2[i].isEmpty = true then do
            let __do_lift ←
              do
                let info ← Lean.MonadRef.mkInfoFromRefPos
                let _ ← Lean.getCurrMacroScope
                let _ ← Lean.MonadQuotation.getContext
                pure { raw := Lean.Syntax.node1 info `Lean.Parser.Tactic.tacticSorry (Lean.Syntax.atom info "sorry") }
            Lean.Elab.Tactic.Try.mkChainResult.go✝ tac1 tacss2 (i + 1) (__do_lift :: acc) kind?
          else do
            forIn tacss2[i] PUnit.unit fun tac __s =>
                match kind? with
                | some kind =>
                  if (tac.raw.getKind == kind) = true then do
                    Lean.Elab.Tactic.Try.mkChainResult.go✝ tac1 tacss2 (i + 1) (tac :: acc) kind?
                    pure (ForInStep.yield PUnit.unit)
                  else pure (ForInStep.yield PUnit.unit)
                | x => do
                  Lean.Elab.Tactic.Try.mkChainResult.go✝ tac1 tacss2 (i + 1) (tac :: acc) kind?
                  pure (ForInStep.yield PUnit.unit)
            pure ()
        else
          have tacs2 := acc.toArray.reverse;
          if (kind?.isSome && Lean.Elab.Tactic.Try.isOnlyAndNonOnly✝ tacs2) = true then pure ()
          else do
            let __do_lift ← liftM (Lean.Elab.Tactic.Try.mergeAll?✝ tacs2)
            have __do_jp :
              Lean.TSyntax `tactic → StateT (Array (Lean.TSyntax `tactic)) Lean.Elab.Tactic.Try.TryTacticM Unit :=
              fun tac => modify fun x => x.push tac
            match __do_lift with
              | some tac2 => do
                let tac ←
                  do
                    let info ← Lean.MonadRef.mkInfoFromRefPos
                    let _ ← Lean.getCurrMacroScope
                    let _ ← Lean.MonadQuotation.getContext
                    pure
                        {
                          raw :=
                            Lean.Syntax.node3 info `Lean.Parser.Tactic.«tactic_<;>_» tac1.raw
                              (Lean.Syntax.atom info "<;>") tac2.raw }
                __do_jp tac
              | x => do
                let tacs2 ←
                  Array.mapM
                      (fun tac2 => do
                        let info ← Lean.MonadRef.mkInfoFromRefPos
                        let _ ← Lean.getCurrMacroScope
                        let _ ← Lean.MonadQuotation.getContext
                        pure
                            {
                              raw :=
                                Lean.Syntax.node2 info `Lean.cdot
                                  (Lean.Syntax.node1 info `Lean.cdotTk (Lean.Syntax.atom info "·"))
                                  (Lean.Syntax.node1 info `Lean.Parser.Tactic.tacticSeq
                                    (Lean.Syntax.node1 info `Lean.Parser.Tactic.tacticSeq1Indented
                                      (Lean.Syntax.node1 info `null tac2.raw))) })
                      tacs2
                let tac ←
                  do
                    let info ← Lean.MonadRef.mkInfoFromRefPos
                    let _ ← Lean.getCurrMacroScope
                    let _ ← Lean.MonadQuotation.getContext
                    pure
                        {
                          raw :=
                            Lean.Syntax.node2 info `Lean.cdot
                              (Lean.Syntax.node1 info `Lean.cdotTk (Lean.Syntax.atom info "·"))
                              (Lean.Syntax.node1 info `Lean.Parser.Tactic.tacticSeq
                                (Lean.Syntax.node1 info `Lean.Parser.Tactic.tacticSeq1Indented
                                  (Lean.Syntax.node info `null
                                    (#[tac1.raw, Lean.Syntax.node info `null #[]].append
                                      (Lean.Syntax.TSepArray.ofElems tacs2).elemsAndSeps)))) }
                __do_jp tac