awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : ¬s₂.hasNext = 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 } =
    false
have case4 : (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) =
  false
Tactic: rw [ltb, Legacy.Iterator.hasNext_cons_addChar, if_neg (by simpa using h₁)]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : ¬s₂.hasNext = true
case4 :
  (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) =
    false
⊢ 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 } =
    false
have case4₁ : (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) =
  false
Tactic: rw [ltb, Legacy.Iterator.hasNext_cons_addChar, if_neg (by simpa using h₁)]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : ¬s₂.hasNext = true
case4 :
  (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) =
    false
case4₁ :
  (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) =
    false
⊢ 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 } =
    false
have case4₂ : false = false
Tactic: rw [ltb, Legacy.Iterator.hasNext_cons_addChar, if_neg (by simpa using h₁)]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
⊢ 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 } =
    ltb s₁ s₂
have case1 : ∀ (s₁ s₂ : Legacy.Iterator) (h₁ : s₂.hasNext = true) (h₂ : s₁.hasNext = true) (h : s₁.curr = s₂.curr)
  (ih :
    ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
        { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
      ltb s₁.next s₂.next),
  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 } =
    ltb s₁.next s₂.next
Tactic: fun_induction ltb s₁ s₂ with
  | case1 s₁ s₂ h₁ h₂ h ih =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_pos, ← ih]
    · simp only [Legacy.Iterator.next, Pos.Raw.next, get_cons_addChar, ofList_toList]
      congr 2 <;> apply Pos.Raw.add_char_right_comm
    · simpa only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList] using h
  | case2 s₁ s₂ h₁ h₂ h =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_neg]
    · simp only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList, decide_eq_decide]
    · simpa only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList] using h
  | case3 s₁ s₂ h₁ h₂ =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_neg (by simpa using h₂)]
  | case4 s₁ s₂ h₁ =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, if_neg (by simpa using h₁)]
Cleared hypotheses: s₁, s₂
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
case1 :
  ∀ (s₁ s₂ : Legacy.Iterator) (h₁ : s₂.hasNext = true) (h₂ : s₁.hasNext = true) (h : s₁.curr = s₂.curr)
    (ih :
      ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
          { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
        ltb s₁.next s₂.next),
    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 } =
      ltb s₁.next s₂.next
⊢ 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 } =
    ltb s₁ s₂
have case2 : ∀ (s₁ s₂ : Legacy.Iterator) (h₁ : s₂.hasNext = true) (h₂ : s₁.hasNext = true) (h : ¬s₁.curr = s₂.curr),
  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 } =
    decide (s₁.curr < s₂.curr)
Tactic: fun_induction ltb s₁ s₂ with
  | case1 s₁ s₂ h₁ h₂ h ih =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_pos, ← ih]
    · simp only [Legacy.Iterator.next, Pos.Raw.next, get_cons_addChar, ofList_toList]
      congr 2 <;> apply Pos.Raw.add_char_right_comm
    · simpa only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList] using h
  | case2 s₁ s₂ h₁ h₂ h =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_neg]
    · simp only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList, decide_eq_decide]
    · simpa only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList] using h
  | case3 s₁ s₂ h₁ h₂ =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_neg (by simpa using h₂)]
  | case4 s₁ s₂ h₁ =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, if_neg (by simpa using h₁)]
Cleared hypotheses: s₁, s₂
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
case1 :
  ∀ (s₁ s₂ : Legacy.Iterator) (h₁ : s₂.hasNext = true) (h₂ : s₁.hasNext = true) (h : s₁.curr = s₂.curr)
    (ih :
      ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
          { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
        ltb s₁.next s₂.next),
    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 } =
      ltb s₁.next s₂.next
case2 :
  ∀ (s₁ s₂ : Legacy.Iterator) (h₁ : s₂.hasNext = true) (h₂ : s₁.hasNext = true) (h : ¬s₁.curr = s₂.curr),
    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 } =
      decide (s₁.curr < s₂.curr)
⊢ 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 } =
    ltb s₁ s₂
have case3 : ∀ (s₁ s₂ : Legacy.Iterator) (h₁ : s₂.hasNext = true) (h₂ : ¬s₁.hasNext = 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
Tactic: fun_induction ltb s₁ s₂ with
  | case1 s₁ s₂ h₁ h₂ h ih =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_pos, ← ih]
    · simp only [Legacy.Iterator.next, Pos.Raw.next, get_cons_addChar, ofList_toList]
      congr 2 <;> apply Pos.Raw.add_char_right_comm
    · simpa only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList] using h
  | case2 s₁ s₂ h₁ h₂ h =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_neg]
    · simp only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList, decide_eq_decide]
    · simpa only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList] using h
  | case3 s₁ s₂ h₁ h₂ =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_neg (by simpa using h₂)]
  | case4 s₁ s₂ h₁ =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, if_neg (by simpa using h₁)]
Cleared hypotheses: s₁, s₂
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
case1 :
  ∀ (s₁ s₂ : Legacy.Iterator) (h₁ : s₂.hasNext = true) (h₂ : s₁.hasNext = true) (h : s₁.curr = s₂.curr)
    (ih :
      ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
          { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
        ltb s₁.next s₂.next),
    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 } =
      ltb s₁.next s₂.next
case2 :
  ∀ (s₁ s₂ : Legacy.Iterator) (h₁ : s₂.hasNext = true) (h₂ : s₁.hasNext = true) (h : ¬s₁.curr = s₂.curr),
    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 } =
      decide (s₁.curr < s₂.curr)
case3 :
  ∀ (s₁ s₂ : Legacy.Iterator) (h₁ : s₂.hasNext = true) (h₂ : ¬s₁.hasNext = 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
⊢ 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 } =
    ltb s₁ s₂
have case4 : ∀ (s₁ s₂ : Legacy.Iterator) (h₁ : ¬s₂.hasNext = 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 } =
    false
Tactic: fun_induction ltb s₁ s₂ with
  | case1 s₁ s₂ h₁ h₂ h ih =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_pos, ← ih]
    · simp only [Legacy.Iterator.next, Pos.Raw.next, get_cons_addChar, ofList_toList]
      congr 2 <;> apply Pos.Raw.add_char_right_comm
    · simpa only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList] using h
  | case2 s₁ s₂ h₁ h₂ h =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_neg]
    · simp only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList, decide_eq_decide]
    · simpa only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList] using h
  | case3 s₁ s₂ h₁ h₂ =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_neg (by simpa using h₂)]
  | case4 s₁ s₂ h₁ =>
    rw [ltb, Legacy.Iterator.hasNext_cons_addChar, if_neg (by simpa using h₁)]
Cleared hypotheses: s₁, s₂
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos.Raw
⊢ ltb { s := ofList (c :: cs₁), i := i₁ + c : Legacy.Iterator }
      { s := ofList (c :: cs₂), i := i₂ + c : Legacy.Iterator } =
    ltb { s := ofList cs₁, i := i₁ } { s := ofList cs₂, i := i₂ }
have rw : ltb
    { s := ofList (c :: { s := ofList cs₁, i := i₁ : Legacy.Iterator }.s.toList),
      i := { s := ofList cs₁, i := i₁ : Legacy.Iterator }.i + c : Legacy.Iterator }
    { s := ofList (c :: { s := ofList cs₂, i := i₂ : Legacy.Iterator }.s.toList),
      i := { s := ofList cs₂, i := i₂ : Legacy.Iterator }.i + c : Legacy.Iterator } =
  ltb { s := ofList (c :: cs₁), i := i₁ + c } { s := ofList (c :: cs₂), i := i₂ + c }
Tactic: rw [eq_comm, ← ltb_cons_addChar' c]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
s₁ s₂ : String
⊢ ltb { s := s₁, i := 0 : Legacy.Iterator } { s := s₂, i := 0 : Legacy.Iterator } = true ↔ s₁.toList < s₂.toList
have obtain : ∀ (s₁ : List Char),
  ltb { s := ofList s₁, i := 0 : Legacy.Iterator } { s := s₂, i := 0 : Legacy.Iterator } = true ↔
    (ofList s₁).toList < s₂.toList
Tactic: obtain ⟨s₁, rfl⟩ := s₁.exists_eq_ofList
Cleared hypotheses: s₁
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
s₂ : String
s₁ : List Char
⊢ ltb { s := ofList s₁, i := 0 : Legacy.Iterator } { s := s₂, i := 0 : Legacy.Iterator } = true ↔
    (ofList s₁).toList < s₂.toList
have obtain : ∀ (s₂ : List Char),
  ltb { s := ofList s₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔
    (ofList s₁).toList < (ofList s₂).toList
Tactic: obtain ⟨s₂, rfl⟩ := s₂.exists_eq_ofList
Cleared hypotheses: s₂
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
s₁ s₂ : List Char
⊢ ltb { s := ofList s₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔
    (ofList s₁).toList < (ofList s₂).toList
have simp : ltb { s := ofList s₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ s₁ < s₂
Tactic: simp only [String.toList_ofList]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
s₁ s₂ : List Char
⊢ ltb { s := ofList s₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ s₁ < s₂
have nil : ∀ (s₂ : List Char),
  ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ [] < s₂
Tactic: induction s₁ generalizing s₂
Cleared hypotheses: s₁, s₂
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
s₁ s₂ : List Char
nil :
  ∀ (s₂ : List Char),
    ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ [] < s₂
⊢ ltb { s := ofList s₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ s₁ < s₂
have cons : ∀ (head : Char) (tail : List Char),
  (∀ (s₂ : List Char),
      ltb { s := ofList tail, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔
        tail < s₂) →
    ∀ (s₂ : List Char),
      ltb { s := ofList (head :: tail), i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔
        head :: tail < s₂
Tactic: induction s₁ generalizing s₂
Cleared hypotheses: s₁, s₂
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
s₂ : List Char
⊢ ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ [] < s₂
have nil : ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList [], i := 0 : Legacy.Iterator } = true ↔
  LT.lt (α := List Char) [] []
Tactic: cases s₂
Cleared hypotheses: s₂
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
s₂ : List Char
nil :
  ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList [], i := 0 : Legacy.Iterator } = true ↔
    LT.lt (α := List Char) [] []
⊢ ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ [] < s₂
have nil₁ : ∀ (head : Char) (tail : List Char),
  ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList (head :: tail), i := 0 : Legacy.Iterator } = true ↔
    [] < head :: tail
Tactic: cases s₂
Cleared hypotheses: s₂
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
head : Char
tail : List Char
tail_ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList tail, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ tail < s₂
s₂ : List Char
⊢ ltb { s := ofList (head :: tail), i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔
    head :: tail < s₂
have cons : ltb { s := ofList (head :: tail), i := 0 : Legacy.Iterator } { s := ofList [], i := 0 : Legacy.Iterator } = true ↔
  head :: tail < []
Tactic: cases s₂
Cleared hypotheses: s₂
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
head : Char
tail : List Char
tail_ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList tail, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ tail < s₂
s₂ : List Char
cons :
  ltb { s := ofList (head :: tail), i := 0 : Legacy.Iterator } { s := ofList [], i := 0 : Legacy.Iterator } = true ↔
    head :: tail < []
⊢ ltb { s := ofList (head :: tail), i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔
    head :: tail < s₂
have cons₁ : ∀ (head_1 : Char) (tail_1 : List Char),
  ltb { s := ofList (head :: tail), i := 0 : Legacy.Iterator }
        { s := ofList (head_1 :: tail_1), i := 0 : Legacy.Iterator } =
      true ↔
    head :: tail < head_1 :: tail_1
Tactic: cases s₂
Cleared hypotheses: s₂
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
⊢ ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList [], i := 0 : Legacy.Iterator } = true ↔
    LT.lt (α := List Char) [] []
have nil : (if { s := ofList [], i := 0 : Legacy.Iterator }.hasNext = true then
      if { s := ofList [], i := 0 : Legacy.Iterator }.hasNext = true then
        if { s := ofList [], i := 0 : Legacy.Iterator }.curr = { s := ofList [], i := 0 : Legacy.Iterator }.curr then
          ltb { s := ofList [], i := 0 : Legacy.Iterator }.next { s := ofList [], i := 0 : Legacy.Iterator }.next
        else
          decide ({ s := ofList [], i := 0 : Legacy.Iterator }.curr < { s := ofList [], i := 0 : Legacy.Iterator }.curr)
      else true
    else false) =
    true ↔
  LT.lt (α := List Char) [] []
Tactic: unfold ltb
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₂ : Char
cs₂ : List Char
⊢ ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator } = true ↔
    [] < c₂ :: cs₂
have nil : ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator } = true
Tactic: apply iff_of_true
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₂ : Char
cs₂ : List Char
nil : ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator } = true
⊢ ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator } = true ↔
    [] < c₂ :: cs₂
have nil₁ : [] < c₂ :: cs₂
Tactic: apply iff_of_true
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₂ : Char
cs₂ : List Char
⊢ ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator } = true
have nil : (if { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.hasNext = true then
    if { s := ofList [], i := 0 : Legacy.Iterator }.hasNext = true then
      if
          { s := ofList [], i := 0 : Legacy.Iterator }.curr =
            { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.curr then
        ltb { s := ofList [], i := 0 : Legacy.Iterator }.next { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.next
      else
        decide
          ({ s := ofList [], i := 0 : Legacy.Iterator }.curr <
            { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.curr)
    else true
  else false) =
  true
Tactic: unfold ltb
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator } { s := ofList [], i := 0 : Legacy.Iterator } = true ↔
    c₁ :: cs₁ < []
have cons : ¬ltb { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator } { s := ofList [], i := 0 : Legacy.Iterator } = true
Tactic: apply iff_of_false
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
cons : ¬ltb { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator } { s := ofList [], i := 0 : Legacy.Iterator } = true
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator } { s := ofList [], i := 0 : Legacy.Iterator } = true ↔
    c₁ :: cs₁ < []
have cons₁ : ¬c₁ :: cs₁ < []
Tactic: apply iff_of_false
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
⊢ ¬ltb { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator } { s := ofList [], i := 0 : Legacy.Iterator } = true
have cons : ¬(if { s := ofList [], i := 0 : Legacy.Iterator }.hasNext = true then
      if { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.hasNext = true then
        if
            { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.curr =
              { s := ofList [], i := 0 : Legacy.Iterator }.curr then
          ltb { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.next
            { s := ofList [], i := 0 : Legacy.Iterator }.next
        else
          decide
            ({ s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.curr <
              { s := ofList [], i := 0 : Legacy.Iterator }.curr)
      else true
    else false) =
    true
Tactic: unfold ltb