{motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
  {motive_2 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
    {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
      {motive_4 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
        {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
          {motive_6 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
            ((toSnapshot : Lean.Language.Snapshot) →
                (stx : Lean.Syntax) →
                  (inner? : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                    (finished : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticFinishedSnapshot) →
                      (next : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                        motive_2 inner? →
                          motive_3 next →
                            motive_1
                              { toSnapshot := toSnapshot, stx := stx, inner? := inner?, finished := finished,
                                next := next }) →
              motive_2 none →
                ((val : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
                    motive_4 val → motive_2 (some val)) →
                  ((toList : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                      motive_5 toList → motive_3 { toList := toList }) →
                    ((stx? : Option Lean.Syntax) →
                        (reportingRange : Lean.Language.SnapshotTask.ReportingRange) →
                          (cancelTk? : Option IO.CancelToken) →
                            (task : Task Lean.Elab.Tactic.TacticParsedSnapshot) →
                              motive_6 task →
                                motive_4
                                  { stx? := stx?, reportingRange := reportingRange, cancelTk? := cancelTk?,
                                    task := task }) →
                      motive_5 [] →
                        ((head : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
                            (tail : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                              motive_4 head → motive_5 tail → motive_5 (head :: tail)) →
                          ((get : Lean.Elab.Tactic.TacticParsedSnapshot) → motive_1 get → motive_6 { get := get }) →
                            (t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) → motive_3 t