-- 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:
s₁ s₂ : List Char
⊢ ltb { s := { data := s₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ s₁ < s₂

Tactic:
induction s₁ generalizing s₂ <;> cases s₂

Result:
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✝

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
⊢ (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₂

Tactic:
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]

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 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₂

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₁ } = true ↔
    c₁ :: cs₁ < c₁ :: cs₂

Tactic:
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

Result:
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 }

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

Tactic:
assumption

Result:
no goals

Proof state:
case nil.cons
c₂ : Char
cs₂ : List Char
⊢ ltb { s := { data := [] }, i := 0 } { s := { data := c₂ :: cs₂ }, i := 0 } = true ↔ [] < c₂ :: cs₂

Tactic:
apply iff_of_true

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

Proof state:
case nil.cons.hb
c₂ : Char
cs₂ : List Char
⊢ [] < c₂ :: cs₂

Tactic:
apply List.nil_lt_cons

Result:
no goals

Proof state:
case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ (if { s := { data := c₂ :: cs₂ }, i := 0 }.hasNext = true then
      if { s := { data := [] }, i := 0 }.hasNext = true then
        if { s := { data := [] }, i := 0 }.curr = { s := { data := c₂ :: cs₂ }, i := 0 }.curr then
          ltb { s := { data := [] }, i := 0 }.next { s := { data := c₂ :: cs₂ }, i := 0 }.next
        else decide ({ s := { data := [] }, i := 0 }.curr < { s := { data := c₂ :: cs₂ }, i := 0 }.curr)
      else true
    else false) =
    true

Tactic:
simp [Iterator.hasNext, Char.utf8Size_pos]

Result:
no goals

Proof state:
case neg.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 x1 x2 => x1 < x2) cs₁ cs₂
⊢ c₁ < c₁

Tactic:
contradiction

Result:
no goals

Proof state:
case nil.nil

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

Tactic:
unfold ltb

Result:
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 ↔
    [] < []

Proof state:
case cons.nil.hb.h
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₁

Tactic:
apply List.nil_lt_cons

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
⊢ (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₂

Tactic:
split_ifs with h

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