case nil.nil

⊢ ltb { s := { data := [] }, i := 0 } { s := { data := [] }, i := 0 } = true ↔ [] < []

case nil.cons
head✝ : Char
tail✝ : List Char
⊢ ltb { s := { data := [] }, i := 0 } { s := { data := head✝ :: tail✝ }, i := 0 } = true ↔ [] < head✝ :: tail✝

case cons.nil
head✝ : Char
tail✝ : List Char
tail_ih✝ :
  ∀ (s₂ : List Char), ltb { s := { data := tail✝ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ tail✝ < s₂
⊢ ltb { s := { data := head✝ :: tail✝ }, i := 0 } { s := { data := [] }, i := 0 } = true ↔ head✝ :: tail✝ < []

case cons.cons
head✝¹ : Char
tail✝¹ : List Char
tail_ih✝ :
  ∀ (s₂ : List Char), ltb { s := { data := tail✝¹ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ tail✝¹ < s₂
head✝ : Char
tail✝ : List Char
⊢ ltb { s := { data := head✝¹ :: tail✝¹ }, i := 0 } { s := { data := head✝ :: tail✝ }, i := 0 } = true ↔
    head✝¹ :: tail✝¹ < head✝ :: tail✝
s₁ s₂ : List Char
⊢ ltb { s := { data := s₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ s₁ < s₂
induction s₁ generalizing s₂ <;> cases s₂
no goals
case nil.nil

⊢ ltb { s := { data := [] }, i := 0 } { s := { data := [] }, i := 0 } = true ↔ [] < []
simp
case nil.cons
c₂ : Char
cs₂ : List Char
⊢ ltb { s := { data := [] }, i := 0 } { s := { data := c₂ :: cs₂ }, i := 0 } = true ↔ [] < c₂ :: cs₂
case nil.cons
head✝ : Char
tail✝ : List Char
⊢ ltb { s := { data := [] }, i := 0 } { s := { data := head✝ :: tail✝ }, i := 0 } = true ↔ [] < head✝ :: tail✝
rename_i c₂ cs₂
case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ ltb { s := { data := [] }, i := 0 } { s := { data := c₂ :: cs₂ }, i := 0 } = true

case nil.cons.hb
c₂ : Char
cs₂ : List Char
⊢ [] < c₂ :: cs₂
case nil.cons
c₂ : Char
cs₂ : List Char
⊢ ltb { s := { data := [] }, i := 0 } { s := { data := c₂ :: cs₂ }, i := 0 } = true ↔ [] < c₂ :: cs₂
apply iff_of_true
case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ (if Iterator.hasNext { s := { data := c₂ :: cs₂ }, i := 0 } = true then
      if Iterator.hasNext { s := { data := [] }, i := 0 } = true then
        if Iterator.curr { s := { data := [] }, i := 0 } = Iterator.curr { s := { data := c₂ :: cs₂ }, i := 0 } then
          ltb (Iterator.next { s := { data := [] }, i := 0 }) (Iterator.next { s := { data := c₂ :: cs₂ }, i := 0 })
        else
          decide (Iterator.curr { s := { data := [] }, i := 0 } < Iterator.curr { s := { data := c₂ :: cs₂ }, i := 0 })
      else true
    else false) =
    true
case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ ltb { s := { data := [] }, i := 0 } { s := { data := c₂ :: cs₂ }, i := 0 } = true
rw [ltb]
case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ Iterator.hasNext { s := { data := c₂ :: cs₂ }, i := 0 } = false → False
case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ (if Iterator.hasNext { s := { data := c₂ :: cs₂ }, i := 0 } = true then
      if Iterator.hasNext { s := { data := [] }, i := 0 } = true then
        if Iterator.curr { s := { data := [] }, i := 0 } = Iterator.curr { s := { data := c₂ :: cs₂ }, i := 0 } then
          ltb (Iterator.next { s := { data := [] }, i := 0 }) (Iterator.next { s := { data := c₂ :: cs₂ }, i := 0 })
        else
          decide (Iterator.curr { s := { data := [] }, i := 0 } < Iterator.curr { s := { data := c₂ :: cs₂ }, i := 0 })
      else true
    else false) =
    true
simp
case nil.cons.ha.a
c₂ : Char
cs₂ : List Char
⊢ Iterator.hasNext { s := { data := c₂ :: cs₂ }, i := 0 } = true
case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ Iterator.hasNext { s := { data := c₂ :: cs₂ }, i := 0 } = false → False
apply ne_false_of_eq_true
case nil.cons.ha.a.a
c₂ : Char
cs₂ : List Char
⊢ 0.byteIdx < (endPos { data := c₂ :: cs₂ }).byteIdx
case nil.cons.ha.a
c₂ : Char
cs₂ : List Char
⊢ Iterator.hasNext { s := { data := c₂ :: cs₂ }, i := 0 } = true
apply decide_eq_true
no goals
case nil.cons.ha.a.a
c₂ : Char
cs₂ : List Char
⊢ 0.byteIdx < (endPos { data := c₂ :: cs₂ }).byteIdx
simp [endPos, utf8ByteSize, utf8ByteSize.go, csize_pos]
no goals
case nil.cons.hb
c₂ : Char
cs₂ : List Char
⊢ [] < c₂ :: cs₂
apply List.nil_lt_cons
case cons.nil
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
⊢ ltb { s := { data := c₁ :: cs₁ }, i := 0 } { s := { data := [] }, i := 0 } = true ↔ c₁ :: cs₁ < []
case cons.nil
head✝ : Char
tail✝ : List Char
tail_ih✝ :
  ∀ (s₂ : List Char), ltb { s := { data := tail✝ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ tail✝ < s₂
⊢ ltb { s := { data := head✝ :: tail✝ }, i := 0 } { s := { data := [] }, i := 0 } = true ↔ head✝ :: tail✝ < []
rename_i c₁ cs₁ ih
case cons.nil.ha
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬ltb { s := { data := c₁ :: cs₁ }, i := 0 } { s := { data := [] }, i := 0 } = true

case cons.nil.hb
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬c₁ :: cs₁ < []
case cons.nil
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
⊢ ltb { s := { data := c₁ :: cs₁ }, i := 0 } { s := { data := [] }, i := 0 } = true ↔ c₁ :: cs₁ < []
apply iff_of_false
case cons.nil.ha
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬(if Iterator.hasNext { s := { data := [] }, i := 0 } = true then
        if Iterator.hasNext { s := { data := c₁ :: cs₁ }, i := 0 } = true then
          if Iterator.curr { s := { data := c₁ :: cs₁ }, i := 0 } = Iterator.curr { s := { data := [] }, i := 0 } then
            ltb (Iterator.next { s := { data := c₁ :: cs₁ }, i := 0 }) (Iterator.next { s := { data := [] }, i := 0 })
          else
            decide
              (Iterator.curr { s := { data := c₁ :: cs₁ }, i := 0 } < Iterator.curr { s := { data := [] }, i := 0 })
        else true
      else false) =
      true
case cons.nil.ha
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬ltb { s := { data := c₁ :: cs₁ }, i := 0 } { s := { data := [] }, i := 0 } = true
rw [ltb]
no goals
case cons.nil.ha
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬(if Iterator.hasNext { s := { data := [] }, i := 0 } = true then
        if Iterator.hasNext { s := { data := c₁ :: cs₁ }, i := 0 } = true then
          if Iterator.curr { s := { data := c₁ :: cs₁ }, i := 0 } = Iterator.curr { s := { data := [] }, i := 0 } then
            ltb (Iterator.next { s := { data := c₁ :: cs₁ }, i := 0 }) (Iterator.next { s := { data := [] }, i := 0 })
          else
            decide
              (Iterator.curr { s := { data := c₁ :: cs₁ }, i := 0 } < Iterator.curr { s := { data := [] }, i := 0 })
        else true
      else false) =
      true
simp
case cons.nil.hb.a
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
⊢ [] < c₁ :: cs₁
case cons.nil.hb
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬c₁ :: cs₁ < []
apply not_lt_of_lt
no goals
case cons.nil.hb.a
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
⊢ [] < c₁ :: cs₁
apply List.nil_lt_cons
case cons.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
⊢ ltb { s := { data := c₁ :: cs₁ }, i := 0 } { s := { data := c₂ :: cs₂ }, i := 0 } = true ↔ c₁ :: cs₁ < c₂ :: cs₂
case cons.cons
head✝¹ : Char
tail✝¹ : List Char
tail_ih✝ :
  ∀ (s₂ : List Char), ltb { s := { data := tail✝¹ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ tail✝¹ < s₂
head✝ : Char
tail✝ : List Char
⊢ ltb { s := { data := head✝¹ :: tail✝¹ }, i := 0 } { s := { data := head✝ :: tail✝ }, i := 0 } = true ↔
    head✝¹ :: tail✝¹ < head✝ :: tail✝
rename_i c₁ cs₁ ih c₂ cs₂
case cons.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
⊢ (if Iterator.hasNext { s := { data := c₂ :: cs₂ }, i := 0 } = true then
        if Iterator.hasNext { s := { data := c₁ :: cs₁ }, i := 0 } = true then
          if
              Iterator.curr { s := { data := c₁ :: cs₁ }, i := 0 } =
                Iterator.curr { s := { data := c₂ :: cs₂ }, i := 0 } then
            ltb (Iterator.next { s := { data := c₁ :: cs₁ }, i := 0 })
              (Iterator.next { s := { data := c₂ :: cs₂ }, i := 0 })
          else
            decide
              (Iterator.curr { s := { data := c₁ :: cs₁ }, i := 0 } <
                Iterator.curr { s := { data := c₂ :: cs₂ }, i := 0 })
        else true
      else false) =
      true ↔
    c₁ :: cs₁ < c₂ :: cs₂
case cons.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
⊢ ltb { s := { data := c₁ :: cs₁ }, i := 0 } { s := { data := c₂ :: cs₂ }, i := 0 } = true ↔ c₁ :: cs₁ < c₂ :: cs₂
rw [ltb]
case cons.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
⊢ (if c₁ = c₂ then ltb { s := { data := c₁ :: cs₁ }, i := 0 + c₁ } { s := { data := c₂ :: cs₂ }, i := 0 + c₂ } = true
    else c₁ < c₂) ↔
    c₁ :: cs₁ < c₂ :: cs₂
case cons.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
⊢ (if Iterator.hasNext { s := { data := c₂ :: cs₂ }, i := 0 } = true then
        if Iterator.hasNext { s := { data := c₁ :: cs₁ }, i := 0 } = true then
          if
              Iterator.curr { s := { data := c₁ :: cs₁ }, i := 0 } =
                Iterator.curr { s := { data := c₂ :: cs₂ }, i := 0 } then
            ltb (Iterator.next { s := { data := c₁ :: cs₁ }, i := 0 })
              (Iterator.next { s := { data := c₂ :: cs₂ }, i := 0 })
          else
            decide
              (Iterator.curr { s := { data := c₁ :: cs₁ }, i := 0 } <
                Iterator.curr { s := { data := c₂ :: cs₂ }, i := 0 })
        else true
      else false) =
      true ↔
    c₁ :: cs₁ < c₂ :: cs₂
simp [Iterator.hasNext, endPos, utf8ByteSize, utf8ByteSize.go, csize_pos, Iterator.curr, get,
      utf8GetAux, Iterator.next, next]
case cons.cons.inl
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : c₁ = c₂
⊢ ltb { s := { data := c₁ :: cs₁ }, i := 0 + c₁ } { s := { data := c₂ :: cs₂ }, i := 0 + c₂ } = true ↔
    c₁ :: cs₁ < c₂ :: cs₂

case cons.cons.inr
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
⊢ c₁ < c₂ ↔ c₁ :: cs₁ < c₂ :: cs₂
case cons.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
⊢ (if c₁ = c₂ then ltb { s := { data := c₁ :: cs₁ }, i := 0 + c₁ } { s := { data := c₂ :: cs₂ }, i := 0 + c₂ } = true
    else c₁ < c₂) ↔
    c₁ :: cs₁ < c₂ :: cs₂
split_ifs with h
case cons.cons.inl
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
⊢ ltb { s := { data := c₁ :: cs₁ }, i := 0 + c₁ } { s := { data := c₁ :: cs₂ }, i := 0 + c₁ } = true ↔
    c₁ :: cs₁ < c₁ :: cs₂
case cons.cons.inl
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : c₁ = c₂
⊢ ltb { s := { data := c₁ :: cs₁ }, i := 0 + c₁ } { s := { data := c₂ :: cs₂ }, i := 0 + c₂ } = true ↔
    c₁ :: cs₁ < c₂ :: cs₂
subst c₂
case cons.cons.inl
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
⊢ ltb { s := { data := c₁ :: cs₁ }, i := { byteIdx := csize c₁ } }
      { s := { data := c₁ :: cs₂ }, i := { byteIdx := csize c₁ } } =
    ltb { s := { data := cs₁ }, i := 0 } { s := { data := cs₂ }, i := 0 }
case cons.cons.inl
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
⊢ ltb { s := { data := c₁ :: cs₁ }, i := 0 + c₁ } { s := { data := c₁ :: cs₂ }, i := 0 + c₁ } = true ↔
    c₁ :: cs₁ < c₁ :: cs₂
suffices ltb ⟨⟨c₁ :: cs₁⟩, ⟨csize c₁⟩⟩ ⟨⟨c₁ :: cs₂⟩, ⟨csize c₁⟩⟩ = ltb ⟨⟨cs₁⟩, 0⟩ ⟨⟨cs₂⟩, 0⟩
  by rw [Pos.zero_addChar_eq, this]; exact (ih cs₂).trans List.Lex.cons_iff.symm
case cons.cons.inl
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
⊢ ltb { s := { data := c₁ :: cs₁ }, i := 0 + c₁ } { s := { data := c₁ :: cs₂ }, i := 0 + c₁ } =
    ltb { s := { data := cs₁ }, i := 0 } { s := { data := cs₂ }, i := 0 }
case cons.cons.inl
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
⊢ ltb { s := { data := c₁ :: cs₁ }, i := { byteIdx := csize c₁ } }
      { s := { data := c₁ :: cs₂ }, i := { byteIdx := csize c₁ } } =
    ltb { s := { data := cs₁ }, i := 0 } { s := { data := cs₂ }, i := 0 }
rw [← Pos.zero_addChar_eq]
no goals
case cons.cons.inl
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
⊢ ltb { s := { data := c₁ :: cs₁ }, i := 0 + c₁ } { s := { data := c₁ :: cs₂ }, i := 0 + c₁ } =
    ltb { s := { data := cs₁ }, i := 0 } { s := { data := cs₂ }, i := 0 }
apply ltb_cons_addChar
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
this :
  ltb { s := { data := c₁ :: cs₁ }, i := { byteIdx := csize c₁ } }
      { s := { data := c₁ :: cs₂ }, i := { byteIdx := csize c₁ } } =
    ltb { s := { data := cs₁ }, i := 0 } { s := { data := cs₂ }, i := 0 }
⊢ ltb { s := { data := cs₁ }, i := 0 } { s := { data := cs₂ }, i := 0 } = true ↔ c₁ :: cs₁ < c₁ :: cs₂
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
this :
  ltb { s := { data := c₁ :: cs₁ }, i := { byteIdx := csize c₁ } }
      { s := { data := c₁ :: cs₂ }, i := { byteIdx := csize c₁ } } =
    ltb { s := { data := cs₁ }, i := 0 } { s := { data := cs₂ }, i := 0 }
⊢ ltb { s := { data := c₁ :: cs₁ }, i := 0 + c₁ } { s := { data := c₁ :: cs₂ }, i := 0 + c₁ } = true ↔
    c₁ :: cs₁ < c₁ :: cs₂
rw [Pos.zero_addChar_eq, this]
no goals
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
this :
  ltb { s := { data := c₁ :: cs₁ }, i := { byteIdx := csize c₁ } }
      { s := { data := c₁ :: cs₂ }, i := { byteIdx := csize c₁ } } =
    ltb { s := { data := cs₁ }, i := 0 } { s := { data := cs₂ }, i := 0 }
⊢ ltb { s := { data := cs₁ }, i := 0 } { s := { data := cs₂ }, i := 0 } = true ↔ c₁ :: cs₁ < c₁ :: cs₂
exact (ih cs₂).trans List.Lex.cons_iff.symm
case cons.cons.inr
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
e : c₁ :: cs₁ < c₂ :: cs₂
⊢ c₁ < c₂
case cons.cons.inr
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
⊢ c₁ < c₂ ↔ c₁ :: cs₁ < c₂ :: cs₂
refine ⟨List.Lex.rel, fun e ↦ ?_⟩
case cons.cons.inr.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
h : ¬c₁ = c₁
h' : List.Lex (fun x x_1 => x < x_1) cs₁ cs₂
⊢ c₁ < c₁

case cons.cons.inr.rel
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
h' : c₁ < c₂
⊢ c₁ < c₂
case cons.cons.inr
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
e : c₁ :: cs₁ < c₂ :: cs₂
⊢ c₁ < c₂
cases e <;> rename_i h'
no goals
case cons.cons.inr.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
h : ¬c₁ = c₁
h' : List.Lex (fun x x_1 => x < x_1) cs₁ cs₂
⊢ c₁ < c₁
contradiction
no goals
case cons.cons.inr.rel
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := { data := cs₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
h' : c₁ < c₂
⊢ c₁ < c₂
assumption