-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem mapAux_of_valid (f : Char → Char) : ∀ l r, mapAux f ⟨utf8Len l⟩ ⟨l ++ r⟩ = ⟨l ++ r.map f⟩
  | l, [] => by unfold mapAux; simp
  | l, c::r => by
    unfold mapAux
    rw [dif_neg (by rw [atEnd_of_valid]; simp)]
    simp only [get_of_valid l (c :: r), Char.reduceDefault, List.headD_cons,
      set_of_valid l (c :: r), List.modifyHead_cons, next_of_valid l (f c) r, List.map_cons]
    simpa using mapAux_of_valid f (l++[f c]) r

Proof state:
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ ¬{ data := l ++ c :: r }.atEnd { byteIdx := utf8Len l } = true

Tactic:
rw [atEnd_of_valid]

Result:
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ ¬c :: r = []

Proof state:
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ (let c_1 := f ({ data := l ++ c :: r }.get { byteIdx := utf8Len l });
    let_fun this := ⋯;
    let s := { data := l ++ c :: r }.set { byteIdx := utf8Len l } c_1;
    mapAux f (s.next { byteIdx := utf8Len l }) s) =
    { data := l ++ List.map f (c :: r) }

Tactic:
simp only [get_of_valid l (c :: r), Char.reduceDefault, List.headD_cons,
  set_of_valid l (c :: r), List.modifyHead_cons, next_of_valid l (f c) r, List.map_cons]

Result:
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ mapAux f { byteIdx := utf8Len l + (f c).utf8Size } { data := l ++ f c :: r } = { data := l ++ f c :: List.map f r }

Proof state:
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ mapAux f { byteIdx := utf8Len l } { data := l ++ c :: r } = { data := l ++ List.map f (c :: r) }

Tactic:
unfold mapAux

Result:
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ (if h : { data := l ++ c :: r }.atEnd { byteIdx := utf8Len l } = true then { data := l ++ c :: r }
    else
      let c_1 := f ({ data := l ++ c :: r }.get { byteIdx := utf8Len l });
      let_fun this := ⋯;
      let s := { data := l ++ c :: r }.set { byteIdx := utf8Len l } c_1;
      mapAux f (s.next { byteIdx := utf8Len l }) s) =
    { data := l ++ List.map f (c :: r) }

Proof state:
f : Char → Char
l : List Char
⊢ (if h : { data := l ++ [] }.atEnd { byteIdx := utf8Len l } = true then { data := l ++ [] }
    else
      let c := f ({ data := l ++ [] }.get { byteIdx := utf8Len l });
      let_fun this := ⋯;
      let s := { data := l ++ [] }.set { byteIdx := utf8Len l } c;
      mapAux f (s.next { byteIdx := utf8Len l }) s) =
    { data := l ++ List.map f [] }

Tactic:
simp

Result:
no goals

Proof state:
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ ¬c :: r = []

Tactic:
simp

Result:
no goals

Proof state:
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ mapAux f { byteIdx := utf8Len l + (f c).utf8Size } { data := l ++ f c :: r } = { data := l ++ f c :: List.map f r }

Tactic:
simpa using mapAux_of_valid f (l++[f c]) r

Result:
no goals

Proof state:
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ (if h : { data := l ++ c :: r }.atEnd { byteIdx := utf8Len l } = true then { data := l ++ c :: r }
    else
      let c_1 := f ({ data := l ++ c :: r }.get { byteIdx := utf8Len l });
      let_fun this := ⋯;
      let s := { data := l ++ c :: r }.set { byteIdx := utf8Len l } c_1;
      mapAux f (s.next { byteIdx := utf8Len l }) s) =
    { data := l ++ List.map f (c :: r) }

Tactic:
rw [dif_neg (by rw [atEnd_of_valid]; simp)]

Result:
f : Char → Char
l : List Char
c : Char
r : List Char
⊢ (let c_1 := f ({ data := l ++ c :: r }.get { byteIdx := utf8Len l });
    let_fun this := ⋯;
    let s := { data := l ++ c :: r }.set { byteIdx := utf8Len l } c_1;
    mapAux f (s.next { byteIdx := utf8Len l }) s) =
    { data := l ++ List.map f (c :: r) }

Proof state:
f : Char → Char
l : List Char
⊢ mapAux f { byteIdx := utf8Len l } { data := l ++ [] } = { data := l ++ List.map f [] }

Tactic:
unfold mapAux

Result:
f : Char → Char
l : List Char
⊢ (if h : { data := l ++ [] }.atEnd { byteIdx := utf8Len l } = true then { data := l ++ [] }
    else
      let c := f ({ data := l ++ [] }.get { byteIdx := utf8Len l });
      let_fun this := ⋯;
      let s := { data := l ++ [] }.set { byteIdx := utf8Len l } c;
      mapAux f (s.next { byteIdx := utf8Len l }) s) =
    { data := l ++ List.map f [] }