-- Init.Data.String.Slice
String.Slice.SplitInclusiveIterator.instIteratorId.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] {pat : ρ}
  [inst_1 : String.Slice.Pattern.ToForwardSearcher pat σ] {s : String.Slice},
  String.Slice.SplitInclusiveIterator.instIteratorId =
    {
      IsPlausibleStep := fun x x_1 =>
        match x, x_1 with
        | { internalState := String.Slice.SplitInclusiveIterator.operating currPos s_1 },
          Std.IterStep.yield { internalState := String.Slice.SplitInclusiveIterator.operating currPos_1 s' } out =>
          s'.IsPlausibleSuccessorOf s_1
        | { internalState := String.Slice.SplitInclusiveIterator.operating currPos s },
          Std.IterStep.yield { internalState := String.Slice.SplitInclusiveIterator.atEnd } out => True
        | { internalState := String.Slice.SplitInclusiveIterator.operating currPos s_1 },
          Std.IterStep.skip { internalState := String.Slice.SplitInclusiveIterator.operating currPos_1 s' } =>
          s'.IsPlausibleSuccessorOf s_1
        | { internalState := String.Slice.SplitInclusiveIterator.operating currPos s },
          Std.IterStep.skip { internalState := String.Slice.SplitInclusiveIterator.atEnd } => False
        | { internalState := String.Slice.SplitInclusiveIterator.operating currPos s }, Std.IterStep.done => True
        | { internalState := String.Slice.SplitInclusiveIterator.atEnd }, Std.IterStep.yield it out => False
        | { internalState := String.Slice.SplitInclusiveIterator.atEnd }, Std.IterStep.skip it => False
        | { internalState := String.Slice.SplitInclusiveIterator.atEnd }, Std.IterStep.done => True,
      step := fun x =>
        match x with
        | { internalState := String.Slice.SplitInclusiveIterator.operating currPos searcher } =>
          match h : searcher.step with
          | ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ =>
            have slice := s.slice! currPos endPos;
            let nextIt := { internalState := String.Slice.SplitInclusiveIterator.operating endPos searcher' };
            pure (Std.Shrink.deflate ⟨Std.IterStep.yield nextIt slice, ⋯⟩)
          | ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ =>
            pure
              (Std.Shrink.deflate
                ⟨Std.IterStep.skip { internalState := String.Slice.SplitInclusiveIterator.operating currPos searcher' },
                  ⋯⟩)
          | ⟨Std.IterStep.skip searcher', hps⟩ =>
            pure
              (Std.Shrink.deflate
                ⟨Std.IterStep.skip { internalState := String.Slice.SplitInclusiveIterator.operating currPos searcher' },
                  ⋯⟩)
          | ⟨Std.IterStep.done, property⟩ =>
            if (currPos != s.endPos) = true then
              have slice := s.sliceFrom currPos;
              pure
                (Std.Shrink.deflate
                  ⟨Std.IterStep.yield { internalState := String.Slice.SplitInclusiveIterator.atEnd } slice, ⋯⟩)
            else pure (Std.Shrink.deflate ⟨Std.IterStep.done, ⋯⟩)
        | { internalState := String.Slice.SplitInclusiveIterator.atEnd } =>
          pure (Std.Shrink.deflate ⟨Std.IterStep.done, ⋯⟩) }