-- 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 base₂
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝ : ¬{ s := { data := cs₂ }, i := i₂ }.hasNext = true
⊢ ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }

Tactic:
conv => lhs; unfold ltb

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

Proof state:
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)

Tactic:
rename_i h₂ h₁ hne

Result:
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)

Proof state:
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)

Tactic:
simp only [Iterator.next, next, heq, Iterator.curr, get_cons_addChar, ite_true] at 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 :: cs₁ }, i := i₁ + { data := cs₂ }.get i₂ + c }
      { s := { data := c :: cs₂ }, i := i₂ + { data := cs₂ }.get i₂ + c } =
    ltb { s := { data := cs₁ }, i := i₁ + { data := cs₂ }.get i₂ }
      { s := { data := cs₂ }, i := i₂ + { data := cs₂ }.get i₂ }
⊢ ltb { s := { data := c :: cs₁ }, i := i₁ + c + { data := cs₂ }.get i₂ }
      { s := { data := c :: cs₂ }, i := i₂ + c + { data := cs₂ }.get i₂ } =
    ltb { s := { data := cs₁ }, i := i₁ + { data := cs₂ }.get i₂ }
      { s := { data := cs₂ }, i := i₂ + { data := cs₂ }.get i₂ }

Proof state:
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 :: cs₁ }, i := i₁ + { data := cs₂ }.get i₂ + c }
      { s := { data := c :: cs₂ }, i := i₂ + { data := cs₂ }.get i₂ + c } =
    ltb { s := { data := cs₁ }, i := i₁ + { data := cs₂ }.get i₂ }
      { s := { data := cs₂ }, i := i₂ + { data := cs₂ }.get i₂ }
⊢ ltb { s := { data := c :: cs₁ }, i := i₁ + { data := cs₂ }.get i₂ + c }
      { s := { data := c :: cs₂ }, i := i₂ + c + { data := cs₂ }.get i₂ } =
    ltb { s := { data := cs₁ }, i := i₁ + { data := cs₂ }.get i₂ }
      { s := { data := cs₂ }, i := i₂ + { data := cs₂ }.get i₂ }

Tactic:
rw [Pos.addChar_right_comm _ c]

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 :: cs₁ }, i := i₁ + { data := cs₂ }.get i₂ + c }
      { s := { data := c :: cs₂ }, i := i₂ + { data := cs₂ }.get i₂ + c } =
    ltb { s := { data := cs₁ }, i := i₁ + { data := cs₂ }.get i₂ }
      { s := { data := cs₂ }, i := i₂ + { data := cs₂ }.get i₂ }
⊢ ltb { s := { data := c :: cs₁ }, i := i₁ + { data := cs₂ }.get i₂ + c }
      { s := { data := c :: cs₂ }, i := i₂ + { data := cs₂ }.get i₂ + c } =
    ltb { s := { data := cs₁ }, i := i₁ + { data := cs₂ }.get i₂ }
      { s := { data := cs₂ }, i := i₂ + { data := cs₂ }.get i₂ }