-- Mathlib/Data/String/Basic.lean
theorem lt_iff_toList_lt : ∀ {s₁ s₂ : String}, s₁ < s₂ ↔ s₁.toList < s₂.toList
  | ⟨s₁⟩, ⟨s₂⟩ => show ltb ⟨⟨s₁⟩, 0⟩ ⟨⟨s₂⟩, 0⟩ ↔ s₁ < s₂ by
    induction s₁ generalizing s₂ <;> cases s₂
    · unfold ltb; decide
    · rename_i c₂ cs₂; apply iff_of_true
      · unfold ltb
        simp [Iterator.hasNext, Char.utf8Size_pos]
      · apply List.nil_lt_cons
    · rename_i c₁ cs₁ ih; apply iff_of_false
      · unfold ltb
        simp [Iterator.hasNext]
      · apply not_lt_of_lt; apply List.nil_lt_cons
    · rename_i c₁ cs₁ ih c₂ cs₂; unfold ltb
      simp only [Iterator.hasNext, Pos.byteIdx_zero, endPos, utf8ByteSize, utf8ByteSize.go,
        add_pos_iff, Char.utf8Size_pos, or_true, decide_eq_true_eq, ↓reduceIte, Iterator.curr, get,
        utf8GetAux, Iterator.next, next, Bool.ite_eq_true_distrib]
      split_ifs with h
      · subst c₂
        suffices ltb ⟨⟨c₁ :: cs₁⟩, (0 : Pos) + c₁⟩ ⟨⟨c₁ :: cs₂⟩, (0 : Pos) + c₁⟩ =
          ltb ⟨⟨cs₁⟩, 0⟩ ⟨⟨cs₂⟩, 0⟩ by rw [this]; exact (ih cs₂).trans List.Lex.cons_iff.symm
        apply ltb_cons_addChar
      · refine ⟨List.Lex.rel, fun e ↦ ?_⟩
        cases e <;> rename_i h'
        · contradiction
        · assumption

Proof state:
case pos
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 }

Tactic:
apply ltb_cons_addChar

Result:
no goals

Proof state:
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 { s := { data := [] }, i := 0 }.hasNext = true then
        if { s := { data := c₁ :: cs₁ }, i := 0 }.hasNext = true then
          if { s := { data := c₁ :: cs₁ }, i := 0 }.curr = { s := { data := [] }, i := 0 }.curr then
            ltb { s := { data := c₁ :: cs₁ }, i := 0 }.next { s := { data := [] }, i := 0 }.next
          else decide ({ s := { data := c₁ :: cs₁ }, i := 0 }.curr < { s := { data := [] }, i := 0 }.curr)
        else true
      else false) =
      true

Tactic:
simp [Iterator.hasNext]

Result:
no goals

Proof state:
case neg
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₂

Tactic:
refine ⟨List.Lex.rel, fun e ↦ ?_⟩

Result:
case neg
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₂

Proof state:
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

Tactic:
unfold ltb

Result:
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 { s := { data := [] }, i := 0 }.hasNext = true then
        if { s := { data := c₁ :: cs₁ }, i := 0 }.hasNext = true then
          if { s := { data := c₁ :: cs₁ }, i := 0 }.curr = { s := { data := [] }, i := 0 }.curr then
            ltb { s := { data := c₁ :: cs₁ }, i := 0 }.next { s := { data := [] }, i := 0 }.next
          else decide ({ s := { data := c₁ :: cs₁ }, i := 0 }.curr < { s := { data := [] }, i := 0 }.curr)
        else true
      else false) =
      true

Proof state:
case nil.nil

⊢ (if { s := { data := [] }, i := 0 }.hasNext = true then
        if { s := { data := [] }, i := 0 }.hasNext = true then
          if { s := { data := [] }, i := 0 }.curr = { s := { data := [] }, i := 0 }.curr then
            ltb { s := { data := [] }, i := 0 }.next { s := { data := [] }, i := 0 }.next
          else decide ({ s := { data := [] }, i := 0 }.curr < { s := { data := [] }, i := 0 }.curr)
        else true
      else false) =
      true ↔
    [] < []

Tactic:
decide

Result:
no goals

Proof state:
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 := 0 + c₁ } { s := { data := c₁ :: cs₂ }, i := 0 + 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₂

Tactic:
exact (ih cs₂).trans List.Lex.cons_iff.symm

Result:
no goals

Proof state:
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₂

Tactic:
unfold ltb

Result:
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 { s := { data := c₂ :: cs₂ }, i := 0 }.hasNext = true then
        if { s := { data := c₁ :: cs₁ }, i := 0 }.hasNext = true then
          if { s := { data := c₁ :: cs₁ }, i := 0 }.curr = { s := { data := c₂ :: cs₂ }, i := 0 }.curr then
            ltb { s := { data := c₁ :: cs₁ }, i := 0 }.next { s := { data := c₂ :: cs₂ }, i := 0 }.next
          else decide ({ s := { data := c₁ :: cs₁ }, i := 0 }.curr < { s := { data := c₂ :: cs₂ }, i := 0 }.curr)
        else true
      else false) =
      true ↔
    c₁ :: cs₁ < c₂ :: cs₂