-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
case3 :
  (if { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr)
      else true
    else false) =
    true
case3₁ :
  (if { s := ofList s₂.s.toList, i := s₂.i : Legacy.Iterator }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr)
      else true
    else false) =
    true
case3₂ :
  (if { s := ofList s₂.s.toList, i := s₂.i : Legacy.Iterator }.hasNext = true then
      if { s := ofList s₁.s.toList, i := s₁.i : Legacy.Iterator }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr)
      else true
    else false) =
    true
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator } =
    true
have case3₃ : (if { s := ofList s₁.s.toList, i := s₁.i : Legacy.Iterator }.hasNext = true then
    if
        { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
          { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr then
      ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
        { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next
    else
      decide
        ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr <
          { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr)
  else true) =
  true
Tactic: rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_neg (by simpa using h₂)]