-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem utf8GetAux_add_right_cancel (s : List Char) (i p n : Nat) :
    utf8GetAux s ⟨i + n⟩ ⟨p + n⟩ = utf8GetAux s ⟨i⟩ ⟨p⟩

Proof state:
case ind
s : List Char
i p n : Nat
⊢ ∀ (c : Char) (cs : List Char) (i : Pos),
    ¬i = { byteIdx := p } →
      utf8GetAux cs { byteIdx := i.byteIdx + c.utf8Size + n } { byteIdx := p + n } =
          utf8GetAux cs (i + c) { byteIdx := p } →
        (if { byteIdx := i.byteIdx + n } = { byteIdx := p + n } then c
          else utf8GetAux cs ({ byteIdx := i.byteIdx + n } + c) { byteIdx := p + n }) =
          if i = { byteIdx := p } then c else utf8GetAux cs (i + c) { byteIdx := p }

Tactic:
intro c cs ⟨i⟩ h ih

Result:
case ind
s : List Char
i✝ p n : Nat
c : Char
cs : List Char
i : Nat
h : ¬{ byteIdx := i } = { byteIdx := p }
ih :
  utf8GetAux cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := p + n } =
    utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }
⊢ (if { byteIdx := { byteIdx := i }.byteIdx + n } = { byteIdx := p + n } then c
    else utf8GetAux cs ({ byteIdx := { byteIdx := i }.byteIdx + n } + c) { byteIdx := p + n }) =
    if { byteIdx := i } = { byteIdx := p } then c else utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }

Proof state:
s : List Char
i p n : Nat
⊢ utf8GetAux s { byteIdx := i + n } { byteIdx := p + n } = utf8GetAux s { byteIdx := i } { byteIdx := p }

Tactic:
apply utf8InductionOn s ⟨i⟩ ⟨p⟩ (motive := fun s i =>
  utf8GetAux s ⟨i.byteIdx + n⟩ ⟨p + n⟩ = utf8GetAux s i ⟨p⟩) <;>
simp only [utf8GetAux, Char.reduceDefault, implies_true, ↓reduceIte, ne_eq, pos_add_char]

Result:
case ind
s : List Char
i p n : Nat
⊢ ∀ (c : Char) (cs : List Char) (i : Pos),
    ¬i = { byteIdx := p } →
      utf8GetAux cs { byteIdx := i.byteIdx + c.utf8Size + n } { byteIdx := p + n } =
          utf8GetAux cs (i + c) { byteIdx := p } →
        (if { byteIdx := i.byteIdx + n } = { byteIdx := p + n } then c
          else utf8GetAux cs ({ byteIdx := i.byteIdx + n } + c) { byteIdx := p + n }) =
          if i = { byteIdx := p } then c else utf8GetAux cs (i + c) { byteIdx := p }

Proof state:
case ind
s : List Char
i✝ p n : Nat
c : Char
cs : List Char
i : Nat
h : ¬{ byteIdx := i } = { byteIdx := p }
ih :
  utf8GetAux cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := p + n } =
    utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }
⊢ (if { byteIdx := { byteIdx := i }.byteIdx + n } = { byteIdx := p + n } then c
    else utf8GetAux cs ({ byteIdx := { byteIdx := i }.byteIdx + n } + c) { byteIdx := p + n }) =
    if { byteIdx := i } = { byteIdx := p } then c else utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }

Tactic:
simp only [Pos.ext_iff, Pos.addChar_eq] at h ⊢

Result:
case ind
s : List Char
i✝ p n : Nat
c : Char
cs : List Char
i : Nat
ih :
  utf8GetAux cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := p + n } =
    utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }
h : ¬i = p
⊢ (if i + n = p + n then c else utf8GetAux cs { byteIdx := i + n + c.utf8Size } { byteIdx := p + n }) =
    if i = p then c else utf8GetAux cs { byteIdx := i + c.utf8Size } { byteIdx := p }

Proof state:
case ind
s : List Char
i✝ p n : Nat
c : Char
cs : List Char
i : Nat
ih :
  utf8GetAux cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := p + n } =
    utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }
h : ¬i = p
⊢ utf8GetAux cs { byteIdx := i + n + c.utf8Size } { byteIdx := p + n } =
    utf8GetAux cs { byteIdx := i + c.utf8Size } { byteIdx := p }

Tactic:
rw [Nat.add_right_comm]

Result:
case ind
s : List Char
i✝ p n : Nat
c : Char
cs : List Char
i : Nat
ih :
  utf8GetAux cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := p + n } =
    utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }
h : ¬i = p
⊢ utf8GetAux cs { byteIdx := i + c.utf8Size + n } { byteIdx := p + n } =
    utf8GetAux cs { byteIdx := i + c.utf8Size } { byteIdx := p }

Proof state:
case ind
s : List Char
i✝ p n : Nat
c : Char
cs : List Char
i : Nat
ih :
  utf8GetAux cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := p + n } =
    utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }
h : ¬i = p
⊢ utf8GetAux cs { byteIdx := i + c.utf8Size + n } { byteIdx := p + n } =
    utf8GetAux cs { byteIdx := i + c.utf8Size } { byteIdx := p }

Tactic:
exact ih

Result:
no goals

Proof state:
case ind
s : List Char
i✝ p n : Nat
c : Char
cs : List Char
i : Nat
ih :
  utf8GetAux cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := p + n } =
    utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }
h : ¬i = p
⊢ (if i + n = p + n then c else utf8GetAux cs { byteIdx := i + n + c.utf8Size } { byteIdx := p + n }) =
    if i = p then c else utf8GetAux cs { byteIdx := i + c.utf8Size } { byteIdx := p }

Tactic:
simp only [Nat.add_right_cancel_iff, h, ↓reduceIte]

Result:
case ind
s : List Char
i✝ p n : Nat
c : Char
cs : List Char
i : Nat
ih :
  utf8GetAux cs { byteIdx := { byteIdx := i }.byteIdx + c.utf8Size + n } { byteIdx := p + n } =
    utf8GetAux cs ({ byteIdx := i } + c) { byteIdx := p }
h : ¬i = p
⊢ utf8GetAux cs { byteIdx := i + n + c.utf8Size } { byteIdx := p + n } =
    utf8GetAux cs { byteIdx := i + c.utf8Size } { byteIdx := p }