-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem prev : ∀ {it}, ValidFor (c :: l) r it → ValidFor l (c :: r) it.prev
  | it, h => by
    cases h.out'
    have := prev_of_valid l.reverse c r
    simp only [utf8Len_reverse] at this
    simp only [Iterator.prev, List.reverse_cons, List.append_assoc, List.singleton_append,
      utf8Len_append, utf8Len_reverse, utf8Len_cons, utf8Len_nil, Nat.zero_add, this]
    exact .of_eq _ (by simp [List.reverseAux_eq]) (by simp)

Proof state:
c : Char
l r : List Char
it : Iterator
h : ValidFor (c :: l) r it
⊢ ValidFor l (c :: r) it.prev

Tactic:
cases h.out'

Result:
case refl
c : Char
l r : List Char
h : ValidFor (c :: l) r { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }
⊢ ValidFor l (c :: r) { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }.prev

Proof state:
case refl
c : Char
l r : List Char
h : ValidFor (c :: l) r { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }
this : { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l + c.utf8Size } = { byteIdx := utf8Len l }
⊢ ValidFor l (c :: r) { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }.prev

Tactic:
simp only [Iterator.prev, List.reverse_cons, List.append_assoc, List.singleton_append,
  utf8Len_append, utf8Len_reverse, utf8Len_cons, utf8Len_nil, Nat.zero_add, this]

Result:
case refl
c : Char
l r : List Char
h : ValidFor (c :: l) r { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }
this : { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l + c.utf8Size } = { byteIdx := utf8Len l }
⊢ ValidFor l (c :: r) { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l } }

Proof state:
case refl
c : Char
l r : List Char
h : ValidFor (c :: l) r { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }
⊢ ValidFor l (c :: r) { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }.prev

Tactic:
have := prev_of_valid l.reverse c r

Result:
case refl
c : Char
l r : List Char
h : ValidFor (c :: l) r { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }
this :
  { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l.reverse + c.utf8Size } = { byteIdx := utf8Len l.reverse }
⊢ ValidFor l (c :: r) { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }.prev

Proof state:
c : Char
l r : List Char
h : ValidFor (c :: l) r { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }
this : { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l + c.utf8Size } = { byteIdx := utf8Len l }
⊢ { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l } }.s.data = l.reverseAux (c :: r)

Tactic:
simp [List.reverseAux_eq]

Result:
no goals

Proof state:
case refl
c : Char
l r : List Char
h : ValidFor (c :: l) r { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }
this :
  { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l.reverse + c.utf8Size } = { byteIdx := utf8Len l.reverse }
⊢ ValidFor l (c :: r) { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }.prev

Tactic:
simp only [utf8Len_reverse] at this

Result:
case refl
c : Char
l r : List Char
h : ValidFor (c :: l) r { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }
this : { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l + c.utf8Size } = { byteIdx := utf8Len l }
⊢ ValidFor l (c :: r) { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }.prev

Proof state:
case refl
c : Char
l r : List Char
h : ValidFor (c :: l) r { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }
this : { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l + c.utf8Size } = { byteIdx := utf8Len l }
⊢ ValidFor l (c :: r) { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l } }

Tactic:
exact .of_eq _ (by simp [List.reverseAux_eq]) (by simp)

Result:
no goals

Proof state:
c : Char
l r : List Char
h : ValidFor (c :: l) r { s := { data := (c :: l).reverse ++ r }, i := { byteIdx := utf8Len (c :: l).reverse } }
this : { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l + c.utf8Size } = { byteIdx := utf8Len l }
⊢ { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l } }.i.byteIdx = utf8Len l

Tactic:
simp

Result:
no goals