-- 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
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
⊢ 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₄ : 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₂)]