-- Mathlib/Data/String/Basic.lean
theorem ltb_cons_addChar (c : Char) (cs₁ cs₂ : List Char) (i₁ i₂ : Pos) :
    ltb ⟨⟨c :: cs₁⟩, i₁ + c⟩ ⟨⟨c :: cs₂⟩, i₂ + c⟩ = ltb ⟨⟨cs₁⟩, i₁⟩ ⟨⟨cs₂⟩, i₂⟩

Proof state:
case ind
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝³ : { s := { data := cs₂ }, i := i₂ }.hasNext = true
a✝² : { s := { data := cs₁ }, i := i₁ }.hasNext = true
a✝¹ : { data := cs₁ }.get i₁ = { data := cs₂ }.get i₂
a✝ :
  ltb
      { s := { data := c :: { s := { data := cs₁ }, i := i₁ }.next.1.data },
        i := { s := { data := cs₁ }, i := i₁ }.next.i + c }
      { s := { data := c :: { s := { data := cs₂ }, i := i₂ }.next.1.data },
        i := { s := { data := cs₂ }, i := i₂ }.next.i + c } =
    ltb
      { s := { data := { s := { data := cs₁ }, i := i₁ }.next.1.data }, i := { s := { data := cs₁ }, i := i₁ }.next.i }
      { s := { data := { s := { data := cs₂ }, i := i₂ }.next.1.data }, i := { s := { data := cs₂ }, i := i₂ }.next.i }
⊢ (if { s := { data := c :: cs₁ }, i := i₁ + c }.curr = { s := { data := c :: cs₂ }, i := i₂ + c }.curr then
      ltb { s := { data := c :: cs₁ }, i := i₁ + c }.next { s := { data := c :: cs₂ }, i := i₂ + c }.next
    else decide ({ s := { data := c :: cs₁ }, i := i₁ + c }.curr < { s := { data := c :: cs₂ }, i := i₂ + c }.curr)) =
    if { s := { data := cs₁ }, i := i₁ }.curr = { s := { data := cs₂ }, i := i₂ }.curr then
      ltb { s := { data := cs₁ }, i := i₁ }.next { s := { data := cs₂ }, i := i₂ }.next
    else decide ({ s := { data := cs₁ }, i := i₁ }.curr < { s := { data := cs₂ }, i := i₂ }.curr)

Tactic:
rename_i h₂ h₁ heq ih

Result:
case ind
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
h₂ : { s := { data := cs₂ }, i := i₂ }.hasNext = true
h₁ : { s := { data := cs₁ }, i := i₁ }.hasNext = true
heq : { data := cs₁ }.get i₁ = { data := cs₂ }.get i₂
ih :
  ltb
      { s := { data := c :: { s := { data := cs₁ }, i := i₁ }.next.1.data },
        i := { s := { data := cs₁ }, i := i₁ }.next.i + c }
      { s := { data := c :: { s := { data := cs₂ }, i := i₂ }.next.1.data },
        i := { s := { data := cs₂ }, i := i₂ }.next.i + c } =
    ltb
      { s := { data := { s := { data := cs₁ }, i := i₁ }.next.1.data }, i := { s := { data := cs₁ }, i := i₁ }.next.i }
      { s := { data := { s := { data := cs₂ }, i := i₂ }.next.1.data }, i := { s := { data := cs₂ }, i := i₂ }.next.i }
⊢ (if { s := { data := c :: cs₁ }, i := i₁ + c }.curr = { s := { data := c :: cs₂ }, i := i₂ + c }.curr then
      ltb { s := { data := c :: cs₁ }, i := i₁ + c }.next { s := { data := c :: cs₂ }, i := i₂ + c }.next
    else decide ({ s := { data := c :: cs₁ }, i := i₁ + c }.curr < { s := { data := c :: cs₂ }, i := i₂ + c }.curr)) =
    if { s := { data := cs₁ }, i := i₁ }.curr = { s := { data := cs₂ }, i := i₂ }.curr then
      ltb { s := { data := cs₁ }, i := i₁ }.next { s := { data := cs₂ }, i := i₂ }.next
    else decide ({ s := { data := cs₁ }, i := i₁ }.curr < { s := { data := cs₂ }, i := i₂ }.curr)

Proof state:
case eq
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
h₂ : { s := { data := cs₂ }, i := i₂ }.hasNext = true
h₁ : { s := { data := cs₁ }, i := i₁ }.hasNext = true
hne : ¬{ data := cs₁ }.get i₁ = { data := cs₂ }.get i₂
⊢ (if { s := { data := c :: cs₁ }, i := i₁ + c }.curr = { s := { data := c :: cs₂ }, i := i₂ + c }.curr then
      ltb { s := { data := c :: cs₁ }, i := i₁ + c }.next { s := { data := c :: cs₂ }, i := i₂ + c }.next
    else decide ({ s := { data := c :: cs₁ }, i := i₁ + c }.curr < { s := { data := c :: cs₂ }, i := i₂ + c }.curr)) =
    if { s := { data := cs₁ }, i := i₁ }.curr = { s := { data := cs₂ }, i := i₂ }.curr then
      ltb { s := { data := cs₁ }, i := i₁ }.next { s := { data := cs₂ }, i := i₂ }.next
    else decide ({ s := { data := cs₁ }, i := i₁ }.curr < { s := { data := cs₂ }, i := i₂ }.curr)

Tactic:
simp [Iterator.curr, get_cons_addChar, hne]

Result:
no goals

Proof state:
c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos
⊢ ltb { s := { data := c :: cs₁ }, i := i₁ + c } { s := { data := c :: cs₂ }, i := i₂ + c } =
    ltb { s := { data := cs₁ }, i := i₁ } { s := { data := cs₂ }, i := i₂ }

Tactic:
apply ltb.inductionOn ⟨⟨cs₁⟩, i₁⟩ ⟨⟨cs₂⟩, i₂⟩ (motive := fun ⟨⟨cs₁⟩, i₁⟩ ⟨⟨cs₂⟩, i₂⟩ ↦
  ltb ⟨⟨c :: cs₁⟩, i₁ + c⟩ ⟨⟨c :: cs₂⟩, i₂ + c⟩ =
  ltb ⟨⟨cs₁⟩, i₁⟩ ⟨⟨cs₂⟩, i₂⟩) <;> simp only <;>
intro ⟨cs₁⟩ ⟨cs₂⟩ i₁ i₂ <;>
intros <;>
(conv => lhs; unfold ltb) <;> (conv => rhs; unfold ltb) <;>
simp only [Iterator.hasNext_cons_addChar, ite_false, ite_true, *, reduceCtorEq]

Result:
case ind
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝³ : { s := { data := cs₂ }, i := i₂ }.hasNext = true
a✝² : { s := { data := cs₁ }, i := i₁ }.hasNext = true
a✝¹ : { data := cs₁ }.get i₁ = { data := cs₂ }.get i₂
a✝ :
  ltb
      { s := { data := c :: { s := { data := cs₁ }, i := i₁ }.next.1.data },
        i := { s := { data := cs₁ }, i := i₁ }.next.i + c }
      { s := { data := c :: { s := { data := cs₂ }, i := i₂ }.next.1.data },
        i := { s := { data := cs₂ }, i := i₂ }.next.i + c } =
    ltb
      { s := { data := { s := { data := cs₁ }, i := i₁ }.next.1.data }, i := { s := { data := cs₁ }, i := i₁ }.next.i }
      { s := { data := { s := { data := cs₂ }, i := i₂ }.next.1.data }, i := { s := { data := cs₂ }, i := i₂ }.next.i }
⊢ (if { s := { data := c :: cs₁ }, i := i₁ + c }.curr = { s := { data := c :: cs₂ }, i := i₂ + c }.curr then
      ltb { s := { data := c :: cs₁ }, i := i₁ + c }.next { s := { data := c :: cs₂ }, i := i₂ + c }.next
    else decide ({ s := { data := c :: cs₁ }, i := i₁ + c }.curr < { s := { data := c :: cs₂ }, i := i₂ + c }.curr)) =
    if { s := { data := cs₁ }, i := i₁ }.curr = { s := { data := cs₂ }, i := i₂ }.curr then
      ltb { s := { data := cs₁ }, i := i₁ }.next { s := { data := cs₂ }, i := i₂ }.next
    else decide ({ s := { data := cs₁ }, i := i₁ }.curr < { s := { data := cs₂ }, i := i₂ }.curr)

case eq
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝² : { s := { data := cs₂ }, i := i₂ }.hasNext = true
a✝¹ : { s := { data := cs₁ }, i := i₁ }.hasNext = true
a✝ : ¬{ data := cs₁ }.get i₁ = { data := cs₂ }.get i₂
⊢ (if { s := { data := c :: cs₁ }, i := i₁ + c }.curr = { s := { data := c :: cs₂ }, i := i₂ + c }.curr then
      ltb { s := { data := c :: cs₁ }, i := i₁ + c }.next { s := { data := c :: cs₂ }, i := i₂ + c }.next
    else decide ({ s := { data := c :: cs₁ }, i := i₁ + c }.curr < { s := { data := c :: cs₂ }, i := i₂ + c }.curr)) =
    if { s := { data := cs₁ }, i := i₁ }.curr = { s := { data := cs₂ }, i := i₂ }.curr then
      ltb { s := { data := cs₁ }, i := i₁ }.next { s := { data := cs₂ }, i := i₂ }.next
    else decide ({ s := { data := cs₁ }, i := i₁ }.curr < { s := { data := cs₂ }, i := i₂ }.curr)