-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem utf8PrevAux_of_valid {cs cs' : List Char} {c : Char} {i p : Nat}
    (hp : i + (utf8Len cs + c.utf8Size) = p) :
    utf8PrevAux (cs ++ c :: cs') ⟨i⟩ ⟨p⟩ = ⟨i + utf8Len cs⟩

Proof state:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ ¬({ byteIdx := i } + c').byteIdx = utf8Len cs + c.utf8Size + (i + c'.utf8Size)

Tactic:
apply ne_add_utf8Size_add_self

Result:
no goals

Proof state:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ { byteIdx := i }.byteIdx + c'.utf8Size + (utf8Len cs + c.utf8Size) = i + (utf8Len cs + c'.utf8Size + c.utf8Size)

Tactic:
simp [Nat.add_assoc, Nat.add_left_comm]

Result:
no goals

Proof state:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ ¬{ byteIdx := i } + c' = { byteIdx := i + (utf8Len cs + c'.utf8Size + c.utf8Size) }

Tactic:
simp only [Pos.ext_iff]

Result:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ ¬({ byteIdx := i } + c').byteIdx = i + (utf8Len cs + c'.utf8Size + c.utf8Size)

Proof state:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ utf8PrevAux (cs ++ c :: cs') ({ byteIdx := i } + c') { byteIdx := i + (utf8Len cs + c'.utf8Size + c.utf8Size) } =
    { byteIdx := i + (utf8Len cs + c'.utf8Size) }

case hnc
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ ¬{ byteIdx := i } + c' = { byteIdx := i + (utf8Len cs + c'.utf8Size + c.utf8Size) }

Tactic:
case hnc =>
  simp only [Pos.ext_iff]
  rw [Nat.add_right_comm, Nat.add_left_comm]
  apply ne_add_utf8Size_add_self

Result:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ utf8PrevAux (cs ++ c :: cs') ({ byteIdx := i } + c') { byteIdx := i + (utf8Len cs + c'.utf8Size + c.utf8Size) } =
    { byteIdx := i + (utf8Len cs + c'.utf8Size) }

Proof state:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ { byteIdx := { byteIdx := i }.byteIdx + c'.utf8Size + utf8Len cs } = { byteIdx := i + (utf8Len cs + c'.utf8Size) }

Tactic:
simp [Nat.add_assoc, Nat.add_comm]

Result:
no goals

Proof state:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ utf8PrevAux (c' :: cs ++ c :: cs') { byteIdx := i } { byteIdx := p } = { byteIdx := i + utf8Len (c' :: cs) }

Tactic:
simp only [utf8PrevAux, List.cons_append, utf8Len_cons, ← hp]

Result:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ (if { byteIdx := i } + c' = { byteIdx := i + (utf8Len cs + c'.utf8Size + c.utf8Size) } then { byteIdx := i }
    else
      utf8PrevAux (cs ++ c :: cs') ({ byteIdx := i } + c') { byteIdx := i + (utf8Len cs + c'.utf8Size + c.utf8Size) }) =
    { byteIdx := i + (utf8Len cs + c'.utf8Size) }

Proof state:
cs cs' : List Char
c : Char
i p : Nat
hp : i + (utf8Len cs + c.utf8Size) = p
⊢ utf8PrevAux (cs ++ c :: cs') { byteIdx := i } { byteIdx := p } = { byteIdx := i + utf8Len cs }

Tactic:
match cs with
| [] => simp [utf8PrevAux, ← hp, Pos.addChar_eq]
| c'::cs =>
  simp only [utf8PrevAux, List.cons_append, utf8Len_cons, ← hp]
  rw [if_neg]
  case hnc =>
    simp only [Pos.ext_iff]
    rw [Nat.add_right_comm, Nat.add_left_comm]
    apply ne_add_utf8Size_add_self
  refine (utf8PrevAux_of_valid (by simp [Nat.add_assoc, Nat.add_left_comm])).trans ?_
  simp [Nat.add_assoc, Nat.add_comm]

Result:
no goals

Proof state:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ (if { byteIdx := i } + c' = { byteIdx := i + (utf8Len cs + c'.utf8Size + c.utf8Size) } then { byteIdx := i }
    else
      utf8PrevAux (cs ++ c :: cs') ({ byteIdx := i } + c') { byteIdx := i + (utf8Len cs + c'.utf8Size + c.utf8Size) }) =
    { byteIdx := i + (utf8Len cs + c'.utf8Size) }

Tactic:
rw [if_neg]

Result:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ utf8PrevAux (cs ++ c :: cs') ({ byteIdx := i } + c') { byteIdx := i + (utf8Len cs + c'.utf8Size + c.utf8Size) } =
    { byteIdx := i + (utf8Len cs + c'.utf8Size) }

case hnc
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ ¬{ byteIdx := i } + c' = { byteIdx := i + (utf8Len cs + c'.utf8Size + c.utf8Size) }

Proof state:
cs cs' : List Char
c : Char
i p : Nat
hp : i + (utf8Len [] + c.utf8Size) = p
⊢ utf8PrevAux ([] ++ c :: cs') { byteIdx := i } { byteIdx := p } = { byteIdx := i + utf8Len [] }

Tactic:
simp [utf8PrevAux, ← hp, Pos.addChar_eq]

Result:
no goals

Proof state:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ ¬({ byteIdx := i } + c').byteIdx = i + (utf8Len cs + c'.utf8Size + c.utf8Size)

Tactic:
rw [Nat.add_right_comm, Nat.add_left_comm]

Result:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ ¬({ byteIdx := i } + c').byteIdx = utf8Len cs + c.utf8Size + (i + c'.utf8Size)

Proof state:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ utf8PrevAux (cs ++ c :: cs') ({ byteIdx := i } + c') { byteIdx := i + (utf8Len cs + c'.utf8Size + c.utf8Size) } =
    { byteIdx := i + (utf8Len cs + c'.utf8Size) }

Tactic:
refine (utf8PrevAux_of_valid (by simp [Nat.add_assoc, Nat.add_left_comm])).trans ?_

Result:
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + c.utf8Size) = p
⊢ { byteIdx := { byteIdx := i }.byteIdx + c'.utf8Size + utf8Len cs } = { byteIdx := i + (utf8Len cs + c'.utf8Size) }