p : Char → Bool
l m r : List Char
acc : List String
⊢ (if h : atEnd { data := l ++ m ++ r } { byteIdx := utf8Len l + utf8Len m } = true then
      let r := extract { data := l ++ m ++ r } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc;
      List.reverse r
    else
      let_fun this :=
        (_ :
          utf8ByteSize { data := l ++ m ++ r } -
              (next { data := l ++ m ++ r } { byteIdx := utf8Len l + utf8Len m }).byteIdx <
            utf8ByteSize { data := l ++ m ++ r } - { byteIdx := utf8Len l + utf8Len m }.byteIdx);
      if p (get { data := l ++ m ++ r } { byteIdx := utf8Len l + utf8Len m }) = true then
        let i' := next { data := l ++ m ++ r } { byteIdx := utf8Len l + utf8Len m };
        splitAux { data := l ++ m ++ r } p i' i'
          (extract { data := l ++ m ++ r } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc)
      else
        splitAux { data := l ++ m ++ r } p { byteIdx := utf8Len l }
          (next { data := l ++ m ++ r } { byteIdx := utf8Len l + utf8Len m }) acc) =
    List.reverse acc ++ List.map mk (List.splitOnP.go p r (List.reverse m))
p : Char → Bool
l m r : List Char
acc : List String
⊢ splitAux { data := l ++ m ++ r } p { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } acc =
    List.reverse acc ++ List.map mk (List.splitOnP.go p r (List.reverse m))
unfold splitAux
p : Char → Bool
l m r : List Char
acc : List String
⊢ (if h : r = [] then
      List.reverse acc ++
        [extract { data := l ++ (m ++ r) } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m }]
    else
      if p (get { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m }) = true then
        splitAux { data := l ++ (m ++ r) } p (next { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m })
          (next { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m })
          (extract { data := l ++ (m ++ r) } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc)
      else
        splitAux { data := l ++ (m ++ r) } p { byteIdx := utf8Len l }
          (next { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m }) acc) =
    List.reverse acc ++ List.map mk (List.splitOnP.go p r (List.reverse m))
p : Char → Bool
l m r : List Char
acc : List String
⊢ (if h : atEnd { data := l ++ m ++ r } { byteIdx := utf8Len l + utf8Len m } = true then
      let r := extract { data := l ++ m ++ r } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc;
      List.reverse r
    else
      let_fun this :=
        (_ :
          utf8ByteSize { data := l ++ m ++ r } -
              (next { data := l ++ m ++ r } { byteIdx := utf8Len l + utf8Len m }).byteIdx <
            utf8ByteSize { data := l ++ m ++ r } - { byteIdx := utf8Len l + utf8Len m }.byteIdx);
      if p (get { data := l ++ m ++ r } { byteIdx := utf8Len l + utf8Len m }) = true then
        let i' := next { data := l ++ m ++ r } { byteIdx := utf8Len l + utf8Len m };
        splitAux { data := l ++ m ++ r } p i' i'
          (extract { data := l ++ m ++ r } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc)
      else
        splitAux { data := l ++ m ++ r } p { byteIdx := utf8Len l }
          (next { data := l ++ m ++ r } { byteIdx := utf8Len l + utf8Len m }) acc) =
    List.reverse acc ++ List.map mk (List.splitOnP.go p r (List.reverse m))
simp [by simpa using atEnd_of_valid (l ++ m) r]
case inl
p : Char → Bool
l m r : List Char
acc : List String
h✝ : r = []
⊢ List.reverse acc ++
      [extract { data := l ++ (m ++ r) } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m }] =
    List.reverse acc ++ List.map mk (List.splitOnP.go p r (List.reverse m))

case inr
p : Char → Bool
l m r : List Char
acc : List String
h✝ : ¬r = []
⊢ (if p (get { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m }) = true then
      splitAux { data := l ++ (m ++ r) } p (next { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m })
        (next { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m })
        (extract { data := l ++ (m ++ r) } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc)
    else
      splitAux { data := l ++ (m ++ r) } p { byteIdx := utf8Len l }
        (next { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m }) acc) =
    List.reverse acc ++ List.map mk (List.splitOnP.go p r (List.reverse m))
p : Char → Bool
l m r : List Char
acc : List String
⊢ (if h : r = [] then
      List.reverse acc ++
        [extract { data := l ++ (m ++ r) } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m }]
    else
      if p (get { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m }) = true then
        splitAux { data := l ++ (m ++ r) } p (next { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m })
          (next { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m })
          (extract { data := l ++ (m ++ r) } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc)
      else
        splitAux { data := l ++ (m ++ r) } p { byteIdx := utf8Len l }
          (next { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m }) acc) =
    List.reverse acc ++ List.map mk (List.splitOnP.go p r (List.reverse m))
split
no goals
p : Char → Bool
l m r : List Char
acc : List String
⊢ ?m.101335
simpa using atEnd_of_valid (l ++ m) r
case inl
p : Char → Bool
l m : List Char
acc : List String
⊢ List.reverse acc ++
      [extract { data := l ++ (m ++ []) } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m }] =
    List.reverse acc ++ List.map mk (List.splitOnP.go p [] (List.reverse m))
case inl
p : Char → Bool
l m r : List Char
acc : List String
h✝ : r = []
⊢ List.reverse acc ++
      [extract { data := l ++ (m ++ r) } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m }] =
    List.reverse acc ++ List.map mk (List.splitOnP.go p r (List.reverse m))
subst r
no goals
case inl
p : Char → Bool
l m : List Char
acc : List String
⊢ List.reverse acc ++
      [extract { data := l ++ (m ++ []) } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m }] =
    List.reverse acc ++ List.map mk (List.splitOnP.go p [] (List.reverse m))
simpa using extract_of_valid l m []
case inr.intro.intro
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝ : ¬c :: r = []
⊢ (if p (get { data := l ++ (m ++ c :: r) } { byteIdx := utf8Len l + utf8Len m }) = true then
      splitAux { data := l ++ (m ++ c :: r) } p
        (next { data := l ++ (m ++ c :: r) } { byteIdx := utf8Len l + utf8Len m })
        (next { data := l ++ (m ++ c :: r) } { byteIdx := utf8Len l + utf8Len m })
        (extract { data := l ++ (m ++ c :: r) } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc)
    else
      splitAux { data := l ++ (m ++ c :: r) } p { byteIdx := utf8Len l }
        (next { data := l ++ (m ++ c :: r) } { byteIdx := utf8Len l + utf8Len m }) acc) =
    List.reverse acc ++ List.map mk (List.splitOnP.go p (c :: r) (List.reverse m))
case inr
p : Char → Bool
l m r : List Char
acc : List String
h✝ : ¬r = []
⊢ (if p (get { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m }) = true then
      splitAux { data := l ++ (m ++ r) } p (next { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m })
        (next { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m })
        (extract { data := l ++ (m ++ r) } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc)
    else
      splitAux { data := l ++ (m ++ r) } p { byteIdx := utf8Len l }
        (next { data := l ++ (m ++ r) } { byteIdx := utf8Len l + utf8Len m }) acc) =
    List.reverse acc ++ List.map mk (List.splitOnP.go p r (List.reverse m))
obtain ⟨c, r, rfl⟩ := r.exists_cons_of_ne_nil ‹_›
case inr.intro.intro
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝ : ¬c :: r = []
⊢ (if p c = true then
      splitAux { data := l ++ (m ++ c :: r) } p { byteIdx := utf8Len l + utf8Len m + csize c }
        { byteIdx := utf8Len l + utf8Len m + csize c } ({ data := m } :: acc)
    else
      splitAux { data := l ++ (m ++ c :: r) } p { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m + csize c }
        acc) =
    List.reverse acc ++
      List.map mk (if p c = true then m :: List.splitOnP.go p r [] else List.splitOnP.go p r (c :: List.reverse m))
case inr.intro.intro
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝ : ¬c :: r = []
⊢ (if p (get { data := l ++ (m ++ c :: r) } { byteIdx := utf8Len l + utf8Len m }) = true then
      splitAux { data := l ++ (m ++ c :: r) } p
        (next { data := l ++ (m ++ c :: r) } { byteIdx := utf8Len l + utf8Len m })
        (next { data := l ++ (m ++ c :: r) } { byteIdx := utf8Len l + utf8Len m })
        (extract { data := l ++ (m ++ c :: r) } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc)
    else
      splitAux { data := l ++ (m ++ c :: r) } p { byteIdx := utf8Len l }
        (next { data := l ++ (m ++ c :: r) } { byteIdx := utf8Len l + utf8Len m }) acc) =
    List.reverse acc ++ List.map mk (List.splitOnP.go p (c :: r) (List.reverse m))
simp [List.splitOnP.go, by simpa using (⟨
  get_of_valid (l++m) (c::r), next_of_valid (l++m) c r, extract_of_valid l m (c::r)⟩ : _∧_∧_)]
case inr.intro.intro.inl
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝¹ : ¬c :: r = []
h✝ : p c = true
⊢ splitAux { data := l ++ (m ++ c :: r) } p { byteIdx := utf8Len l + utf8Len m + csize c }
      { byteIdx := utf8Len l + utf8Len m + csize c } ({ data := m } :: acc) =
    List.reverse acc ++ List.map mk (m :: List.splitOnP.go p r [])

case inr.intro.intro.inr
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝¹ : ¬c :: r = []
h✝ : ¬p c = true
⊢ splitAux { data := l ++ (m ++ c :: r) } p { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m + csize c }
      acc =
    List.reverse acc ++ List.map mk (List.splitOnP.go p r (c :: List.reverse m))
case inr.intro.intro
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝ : ¬c :: r = []
⊢ (if p c = true then
      splitAux { data := l ++ (m ++ c :: r) } p { byteIdx := utf8Len l + utf8Len m + csize c }
        { byteIdx := utf8Len l + utf8Len m + csize c } ({ data := m } :: acc)
    else
      splitAux { data := l ++ (m ++ c :: r) } p { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m + csize c }
        acc) =
    List.reverse acc ++
      List.map mk (if p c = true then m :: List.splitOnP.go p r [] else List.splitOnP.go p r (c :: List.reverse m))
split
no goals
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝ : ¬c :: r = []
⊢ ?m.103548
simpa using (⟨
get_of_valid (l++m) (c::r), next_of_valid (l++m) c r, extract_of_valid l m (c::r)⟩ : _∧_∧_)
no goals
case inr.intro.intro.inl
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝¹ : ¬c :: r = []
h✝ : p c = true
⊢ splitAux { data := l ++ (m ++ c :: r) } p { byteIdx := utf8Len l + utf8Len m + csize c }
      { byteIdx := utf8Len l + utf8Len m + csize c } ({ data := m } :: acc) =
    List.reverse acc ++ List.map mk (m :: List.splitOnP.go p r [])
simpa [Nat.add_assoc] using splitAux_of_valid p (l++m++[c]) [] r (⟨m⟩::acc)
no goals
case inr.intro.intro.inr
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝¹ : ¬c :: r = []
h✝ : ¬p c = true
⊢ splitAux { data := l ++ (m ++ c :: r) } p { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m + csize c }
      acc =
    List.reverse acc ++ List.map mk (List.splitOnP.go p r (c :: List.reverse m))
simpa [Nat.add_assoc] using splitAux_of_valid p l (m++[c]) r acc