-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.RevSplitIterator.instIteratorOfPure.match_1.eq_4 : ∀ {ρ : Type} {ρ_1 : ρ} {σ : String.Slice → Type} [inst : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ]
  {m : Type → Type u_1} {s : String.Slice}
  (motive : Std.IterM m String.Slice → Std.IterStep (Std.IterM m String.Slice) String.Slice → Sort u_2)
  (currPos : s.Pos) (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s))
  (h_1 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        (currPos_1 : s.Pos) →
          (s' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
            (out : String.Slice) →
              motive { internalState := String.Slice.RevSplitIterator.operating currPos s_2 }
                (Std.IterStep.yield { internalState := String.Slice.RevSplitIterator.operating currPos_1 s' } out))
  (h_2 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        (out : String.Slice) →
          motive { internalState := String.Slice.RevSplitIterator.operating currPos s_2 }
            (Std.IterStep.yield { internalState := String.Slice.RevSplitIterator.atEnd } out))
  (h_3 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        (currPos_1 : s.Pos) →
          (s' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
            motive { internalState := String.Slice.RevSplitIterator.operating currPos s_2 }
              (Std.IterStep.skip { internalState := String.Slice.RevSplitIterator.operating currPos_1 s' }))
  (h_4 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive { internalState := String.Slice.RevSplitIterator.operating currPos s_2 }
          (Std.IterStep.skip { internalState := String.Slice.RevSplitIterator.atEnd }))
  (h_5 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive { internalState := String.Slice.RevSplitIterator.operating currPos s_2 } Std.IterStep.done)
  (h_6 :
    (it : Std.IterM m String.Slice) →
      (out : String.Slice) →
        motive { internalState := String.Slice.RevSplitIterator.atEnd } (Std.IterStep.yield it out))
  (h_7 :
    (it : Std.IterM m String.Slice) →
      motive { internalState := String.Slice.RevSplitIterator.atEnd } (Std.IterStep.skip it))
  (h_8 : Unit → motive { internalState := String.Slice.RevSplitIterator.atEnd } Std.IterStep.done),
  (match { internalState := String.Slice.RevSplitIterator.operating currPos s_1 },
      Std.IterStep.skip { internalState := String.Slice.RevSplitIterator.atEnd } with
    | { internalState := String.Slice.RevSplitIterator.operating currPos s_2 },
      Std.IterStep.yield { internalState := String.Slice.RevSplitIterator.operating currPos_1 s' } out =>
      h_1 currPos s_2 currPos_1 s' out
    | { internalState := String.Slice.RevSplitIterator.operating currPos s },
      Std.IterStep.yield { internalState := String.Slice.RevSplitIterator.atEnd } out => h_2 currPos s out
    | { internalState := String.Slice.RevSplitIterator.operating currPos s_2 },
      Std.IterStep.skip { internalState := String.Slice.RevSplitIterator.operating currPos_1 s' } =>
      h_3 currPos s_2 currPos_1 s'
    | { internalState := String.Slice.RevSplitIterator.operating currPos s },
      Std.IterStep.skip { internalState := String.Slice.RevSplitIterator.atEnd } => h_4 currPos s
    | { internalState := String.Slice.RevSplitIterator.operating currPos s }, Std.IterStep.done => h_5 currPos s
    | { internalState := String.Slice.RevSplitIterator.atEnd }, Std.IterStep.yield it out => h_6 it out
    | { internalState := String.Slice.RevSplitIterator.atEnd }, Std.IterStep.skip it => h_7 it
    | { internalState := String.Slice.RevSplitIterator.atEnd }, Std.IterStep.done => h_8 ()) =
    h_4 currPos s_1