-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem utf8GetAux_of_valid (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len cs = p) :
    utf8GetAux (cs ++ cs') ⟨i⟩ ⟨p⟩ = cs'.headD default

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

Tactic:
rw [if_neg]

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

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

Proof state:
cs cs' : List Char
i p : Nat
hp : i + utf8Len [] = p
⊢ utf8GetAux ([] ++ []) { byteIdx := i } { byteIdx := p } = [].headD default

Tactic:
rfl

Result:
no goals

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

Tactic:
simp only [← hp, utf8Len_cons, Pos.ext_iff]

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

Proof state:
cs cs' : List Char
i p : Nat
hp : i + utf8Len cs = p
⊢ utf8GetAux (cs ++ cs') { byteIdx := i } { byteIdx := p } = cs'.headD default

Tactic:
match cs, cs' with
| [], [] => rfl
| [], c::cs' => simp [← hp, utf8GetAux]
| c::cs, cs' =>
  simp only [List.cons_append, utf8GetAux, Char.reduceDefault]
  rw [if_neg]
  case hnc => simp only [← hp, utf8Len_cons, Pos.ext_iff]; exact ne_self_add_add_utf8Size
  refine utf8GetAux_of_valid cs cs' ?_
  simpa [Nat.add_assoc, Nat.add_comm] using hp

Result:
no goals

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

Tactic:
simp [← hp, utf8GetAux]

Result:
no goals

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

Tactic:
simpa [Nat.add_assoc, Nat.add_comm] using hp

Result:
no goals

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

Tactic:
simp only [List.cons_append, utf8GetAux, Char.reduceDefault]

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

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

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

Tactic:
case hnc => simp only [← hp, utf8Len_cons, Pos.ext_iff]; exact ne_self_add_add_utf8Size

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

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

Tactic:
exact ne_self_add_add_utf8Size

Result:
no goals

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

Tactic:
refine utf8GetAux_of_valid cs cs' ?_

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