-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem setCurr' : ∀ {it}, ValidFor l r it →
    ValidFor l (r.modifyHead fun _ => c) (it.setCurr c)
  | it, h => by
    cases h.out'
    simp only [setCurr, utf8Len_reverse]
    refine .of_eq _ ?_ (by simp)
    have := set_of_valid l.reverse r c
    simp only [utf8Len_reverse] at this; simp [List.reverseAux_eq, this]

Proof state:
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }
this :
  { data := l.reverse ++ r }.set { byteIdx := utf8Len l.reverse } c =
    { data := l.reverse ++ List.modifyHead (fun x => c) r }
⊢ { s := { data := l.reverse ++ r }.set { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data =
    l.reverseAux (List.modifyHead (fun x => c) r)

Tactic:
simp only [utf8Len_reverse] at this

Result:
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }
this :
  { data := l.reverse ++ r }.set { byteIdx := utf8Len l } c = { data := l.reverse ++ List.modifyHead (fun x => c) r }
⊢ { s := { data := l.reverse ++ r }.set { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data =
    l.reverseAux (List.modifyHead (fun x => c) r)

Proof state:
l r : List Char
c : Char
h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }
⊢ { s := { data := l.reverse ++ r }.set { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.i.byteIdx =
    utf8Len l

Tactic:
simp

Result:
no goals

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

Tactic:
refine .of_eq _ ?_ (by simp)

Result:
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }
⊢ { s := { data := l.reverse ++ r }.set { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data =
    l.reverseAux (List.modifyHead (fun x => c) r)

Proof state:
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }
⊢ { s := { data := l.reverse ++ r }.set { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data =
    l.reverseAux (List.modifyHead (fun x => c) r)

Tactic:
have := set_of_valid l.reverse r c

Result:
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }
this :
  { data := l.reverse ++ r }.set { byteIdx := utf8Len l.reverse } c =
    { data := l.reverse ++ List.modifyHead (fun x => c) r }
⊢ { s := { data := l.reverse ++ r }.set { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data =
    l.reverseAux (List.modifyHead (fun x => c) r)

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

Tactic:
simp only [setCurr, utf8Len_reverse]

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

Proof state:
case refl
l r : List Char
c : Char
h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }
this :
  { data := l.reverse ++ r }.set { byteIdx := utf8Len l } c = { data := l.reverse ++ List.modifyHead (fun x => c) r }
⊢ { s := { data := l.reverse ++ r }.set { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data =
    l.reverseAux (List.modifyHead (fun x => c) r)

Tactic:
simp [List.reverseAux_eq, this]

Result:
no goals

Proof state:
l r : List Char
c : Char
it : Iterator
h : ValidFor l r it
⊢ ValidFor l (List.modifyHead (fun x => c) r) (it.setCurr c)

Tactic:
cases h.out'

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