-- 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
⊢ (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₂ }

Tactic:
conv => rhs; 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) =
    if { s := { data := { data := cs₂ }.data }, i := i₂ }.hasNext = true then
      if { s := { data := { data := cs₁ }.data }, i := i₁ }.hasNext = true then
        if
            { s := { data := { data := cs₁ }.data }, i := i₁ }.curr =
              { s := { data := { data := cs₂ }.data }, i := i₂ }.curr then
          ltb { s := { data := { data := cs₁ }.data }, i := i₁ }.next
            { s := { data := { data := cs₂ }.data }, i := i₂ }.next
        else
          decide
            ({ s := { data := { data := cs₁ }.data }, i := i₁ }.curr <
              { s := { data := { data := cs₂ }.data }, i := i₂ }.curr)
      else true
    else false

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

Tactic:
exact ih

Result:
no goals

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₁ + 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₂ }

Tactic:
repeat 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₂ }