awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
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
⊢ { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
    { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr

Tactic:
simpa only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList] using h

Premises used: String.Legacy.Iterator.curr, String.ofList_toList, String.get_cons_addChar
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ { s := ofList s₂.s.toList, i := s₂.i : Legacy.Iterator }.hasNext = true

Tactic:
simpa using h₁
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ { s := ofList s₁.s.toList, i := s₁.i : Legacy.Iterator }.hasNext = true

Tactic:
simpa using h₂
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
case2 :
  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) =
    decide (s₁.curr < s₂.curr)
case2₁ :
  ¬{ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.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:
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]

Premises used: String.ltb, if_pos, String.Legacy.Iterator.hasNext_cons_addChar, if_neg
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ 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) =
    decide (s₁.curr < s₂.curr)

Tactic:
simp only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList, decide_eq_decide]

Premises used: String.Legacy.Iterator.curr, decide_eq_decide, String.ofList_toList, String.get_cons_addChar
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ ¬{ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr

Tactic:
simpa only [Legacy.Iterator.curr, get_cons_addChar, ofList_toList] using h

Premises used: String.Legacy.Iterator.curr, String.ofList_toList, String.get_cons_addChar
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ { s := ofList s₂.s.toList, i := s₂.i : Legacy.Iterator }.hasNext = true

Tactic:
simpa using h₁
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ ¬{ s := ofList s₁.s.toList, i := s₁.i : Legacy.Iterator }.hasNext = true

Tactic:
simpa using h₂
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : ¬s₂.hasNext = true
⊢ ¬{ s := ofList s₂.s.toList, i := s₂.i : Legacy.Iterator }.hasNext = true

Tactic:
simpa using h₁
-- Module: Mathlib.Data.String.Basic
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
case4₂ case4₃ : 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

Tactic:
rw [ltb, Legacy.Iterator.hasNext_cons_addChar, if_neg (by simpa using h₁)]

Premises used: String.ltb, String.Legacy.Iterator.hasNext_cons_addChar, if_neg
-- Module: Mathlib.Data.String.Basic
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
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
⊢ 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₂

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₁)]

Premises used: String.ltb, String.Pos.Raw.add_char_right_comm, String.Legacy.Iterator.curr, decide_eq_decide, String.ofList_toList, if_pos, String.Legacy.Iterator.next, String.Pos.Raw.next, String.Legacy.Iterator.hasNext_cons_addChar, if_neg, String.get_cons_addChar
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos.Raw
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 }
⊢ 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₂ }

Tactic:
rw [eq_comm, ← ltb_cons_addChar' c]

Premises used: String.ltb_cons_addChar', eq_comm
-- Module: Mathlib.Data.String.Basic
Goal:
c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos.Raw
⊢ 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:
simp
-- Module: Mathlib.Data.String.Basic
Goal:
s₁ s₂ : String
obtain :
  ∀ (s₁ : List Char),
    ltb { s := ofList s₁, i := 0 : Legacy.Iterator } { s := s₂, i := 0 : Legacy.Iterator } = true ↔
      (ofList s₁).toList < s₂.toList
⊢ ltb { s := s₁, i := 0 : Legacy.Iterator } { s := s₂, i := 0 : Legacy.Iterator } = true ↔ s₁.toList < s₂.toList

Tactic:
obtain ⟨s₁, rfl⟩ := s₁.exists_eq_ofList

Premises used: String.exists_eq_ofList, rfl
-- Module: Mathlib.Data.String.Basic
Goal:
s₂ : String
s₁ : List Char
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
⊢ 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

Premises used: String.exists_eq_ofList, rfl
-- Module: Mathlib.Data.String.Basic
Goal:
s₁ s₂ : List Char
simp : ltb { s := ofList s₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ s₁ < s₂
⊢ ltb { s := ofList s₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔
    (ofList s₁).toList < (ofList s₂).toList

Tactic:
simp only [String.toList_ofList]

Premises used: String.toList_ofList
-- Module: Mathlib.Data.String.Basic
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₂
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₂
⊢ ltb { s := ofList s₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ s₁ < s₂

Tactic:
induction s₁ generalizing s₂
-- Module: Mathlib.Data.String.Basic
Goal:
s₂ : List Char
nil :
  ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList [], i := 0 : Legacy.Iterator } = true ↔
    LT.lt (α := List Char) [] []
nil₁ :
  ∀ (head : Char) (tail : List Char),
    ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList (head :: tail), i := 0 : Legacy.Iterator } = true ↔
      [] < head :: tail
⊢ ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ [] < s₂

Tactic:
cases s₂
-- Module: Mathlib.Data.String.Basic
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 < []
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
⊢ ltb { s := ofList (head :: tail), i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔
    head :: tail < s₂

Tactic:
cases s₂
-- Module: Mathlib.Data.String.Basic
Goal:
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) [] []
⊢ ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList [], i := 0 : Legacy.Iterator } = true ↔
    LT.lt (α := List Char) [] []

Tactic:
unfold ltb

Premises used: String.ltb
-- Module: Mathlib.Data.String.Basic
Goal:
⊢ (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:
decide
-- Module: Mathlib.Data.String.Basic
Goal:
c₂ : Char
cs₂ : List Char
nil : ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator } = true
nil₁ : [] < c₂ :: cs₂
⊢ ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator } = true ↔
    [] < c₂ :: cs₂

Tactic:
apply iff_of_true

Premises used: iff_of_true
-- Module: Mathlib.Data.String.Basic
Goal:
c₂ : Char
cs₂ : List Char
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
⊢ ltb { s := ofList [], i := 0 : Legacy.Iterator } { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator } = true

Tactic:
unfold ltb

Premises used: String.ltb
-- Module: Mathlib.Data.String.Basic
Goal:
c₂ : Char
cs₂ : List Char
⊢ (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:
simp [Legacy.Iterator.hasNext, Char.utf8Size_pos]

Premises used: String.Legacy.Iterator.hasNext, Char.utf8Size_pos
-- Module: Mathlib.Data.String.Basic
Goal:
c₂ : Char
cs₂ : List Char
⊢ [] < c₂ :: cs₂

Tactic:
apply List.nil_lt_cons

Premises used: List.nil_lt_cons
-- Module: Mathlib.Data.String.Basic
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
cons₁ : ¬c₁ :: cs₁ < []
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator } { s := ofList [], i := 0 : Legacy.Iterator } = true ↔
    c₁ :: cs₁ < []

Tactic:
apply iff_of_false

Premises used: iff_of_false
-- Module: Mathlib.Data.String.Basic
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 :
  ¬(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
⊢ ¬ltb { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator } { s := ofList [], i := 0 : Legacy.Iterator } = true

Tactic:
unfold ltb

Premises used: String.ltb
-- Module: Mathlib.Data.String.Basic
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₂
⊢ ¬(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:
simp [Legacy.Iterator.hasNext]

Premises used: String.Legacy.Iterator.hasNext
-- Module: Mathlib.Data.String.Basic
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 : [] < c₁ :: cs₁
⊢ ¬c₁ :: cs₁ < []

Tactic:
apply not_lt_of_gt

Premises used: not_lt_of_gt
-- Module: Mathlib.Data.String.Basic
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₂
⊢ [] < c₁ :: cs₁

Tactic:
apply List.nil_lt_cons

Premises used: List.nil_lt_cons
-- Module: Mathlib.Data.String.Basic
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₂
c₂ : Char
cs₂ : List Char
cons :
  (if { s := ofList (c₂ :: cs₂), 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 (c₂ :: cs₂), i := 0 : Legacy.Iterator }.curr then
            ltb { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.next
              { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.next
          else
            decide
              ({ s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.curr <
                { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.curr)
        else true
      else false) =
      true ↔
    c₁ :: cs₁ < c₂ :: cs₂
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator } { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator } =
      true ↔
    c₁ :: cs₁ < c₂ :: cs₂

Tactic:
unfold ltb

Premises used: String.ltb
-- Module: Mathlib.Data.String.Basic
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₂
c₂ : Char
cs₂ : List Char
cons :
  (if c₁ = c₂ then
      ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
          { s := ofList (c₂ :: cs₂), i := 0 + c₂ : Legacy.Iterator } =
        true
    else c₁ < c₂) ↔
    c₁ :: cs₁ < c₂ :: cs₂
⊢ (if { s := ofList (c₂ :: cs₂), 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 (c₂ :: cs₂), i := 0 : Legacy.Iterator }.curr then
            ltb { s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.next
              { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.next
          else
            decide
              ({ s := ofList (c₁ :: cs₁), i := 0 : Legacy.Iterator }.curr <
                { s := ofList (c₂ :: cs₂), i := 0 : Legacy.Iterator }.curr)
        else true
      else false) =
      true ↔
    c₁ :: cs₁ < c₂ :: cs₂

Tactic:
simp only [Legacy.Iterator.hasNext, Pos.Raw.byteIdx_zero, rawEndPos_ofList, utf8Len_cons,
        add_pos_iff, Char.utf8Size_pos, or_true, decide_true, ↓reduceIte, Legacy.Iterator.curr,
        Pos.Raw.get, String.toList_ofList, Pos.Raw.utf8GetAux, Legacy.Iterator.next, Pos.Raw.next,
        Bool.ite_eq_true_distrib, decide_eq_true_eq]

Premises used: String.toList_ofList, String.Pos.Raw.utf8GetAux, String.Legacy.Iterator.hasNext, String.Legacy.Iterator.curr, String.Pos.Raw.byteIdx_zero, String.utf8Len_cons, Bool.ite_eq_true_distrib, String.rawEndPos_ofList, decide_true, String.Legacy.Iterator.next, String.Pos.Raw.get, Char.utf8Size_pos, add_pos_iff, reduceIte, decide_eq_true_eq, String.Pos.Raw.next, or_true
-- Module: Mathlib.Data.String.Basic
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₂
c₂ : Char
cs₂ : List Char
pos :
  ∀ (h : c₁ = c₂),
    ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
          { s := ofList (c₂ :: cs₂), i := 0 + c₂ : Legacy.Iterator } =
        true ↔
      c₁ :: cs₁ < c₂ :: cs₂
neg : ∀ (h : ¬c₁ = c₂), c₁ < c₂ ↔ c₁ :: cs₁ < c₂ :: cs₂
⊢ (if c₁ = c₂ then
      ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
          { s := ofList (c₂ :: cs₂), i := 0 + c₂ : Legacy.Iterator } =
        true
    else c₁ < c₂) ↔
    c₁ :: cs₁ < c₂ :: cs₂

Tactic:
split_ifs with h