[GOAL]
⊢ DecidableRel fun x x_1 => x < x_1
[PROOFSTEP]
simp only [LT']
[GOAL]
⊢ DecidableRel fun s₁ s₂ => ltb (iter s₁) (iter s₂) = true
[PROOFSTEP]
infer_instance
  -- short-circuit type class inference
[GOAL]
c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos
⊢ ltb { s := { data := c :: cs₁ }, i := i₁ + c } { s := { data := c :: cs₂ }, i := i₂ + c } =
    ltb { s := { data := cs₁ }, i := i₁ } { s := { data := cs₂ }, i := i₂ }
[PROOFSTEP]
apply
  ltb.inductionOn ⟨⟨cs₁⟩, i₁⟩ ⟨⟨cs₂⟩, i₂⟩ (motive := fun ⟨⟨cs₁⟩, i₁⟩ ⟨⟨cs₂⟩, i₂⟩ ↦
    ltb ⟨⟨c :: cs₁⟩, i₁ + c⟩ ⟨⟨c :: cs₂⟩, i₂ + c⟩ = ltb ⟨⟨cs₁⟩, i₁⟩ ⟨⟨cs₂⟩, i₂⟩)
[GOAL]
case ind
c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos
⊢ ∀ (s₁ s₂ : String) (i₁ i₂ : Pos),
    Iterator.hasNext { s := s₂, i := i₂ } = true →
      Iterator.hasNext { s := s₁, i := i₁ } = true →
        get s₁ i₁ = get s₂ i₂ →
          (match Iterator.next { s := s₁, i := i₁ } with
            | { s := { data := cs₁ }, i := i₁ } =>
              match Iterator.next { s := s₂, i := i₂ } with
              | { s := { data := cs₂ }, i := i₂ } =>
                ltb { s := { data := c :: cs₁ }, i := i₁ + c } { s := { data := c :: cs₂ }, i := i₂ + c } =
                  ltb { s := { data := cs₁ }, i := i₁ } { s := { data := cs₂ }, i := i₂ }) →
            match { s := s₁, i := i₁ } with
            | { s := { data := cs₁ }, i := i₁ } =>
              match { s := s₂, i := i₂ } with
              | { s := { data := cs₂ }, i := i₂ } =>
                ltb { s := { data := c :: cs₁ }, i := i₁ + c } { s := { data := c :: cs₂ }, i := i₂ + c } =
                  ltb { s := { data := cs₁ }, i := i₁ } { s := { data := cs₂ }, i := i₂ }
[PROOFSTEP]
simp
[GOAL]
case eq
c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos
⊢ ∀ (s₁ s₂ : String) (i₁ i₂ : Pos),
    Iterator.hasNext { s := s₂, i := i₂ } = true →
      Iterator.hasNext { s := s₁, i := i₁ } = true →
        ¬get s₁ i₁ = get s₂ i₂ →
          match { s := s₁, i := i₁ } with
          | { s := { data := cs₁ }, i := i₁ } =>
            match { s := s₂, i := i₂ } with
            | { s := { data := cs₂ }, i := i₂ } =>
              ltb { s := { data := c :: cs₁ }, i := i₁ + c } { s := { data := c :: cs₂ }, i := i₂ + c } =
                ltb { s := { data := cs₁ }, i := i₁ } { s := { data := cs₂ }, i := i₂ }
[PROOFSTEP]
simp
[GOAL]
case base₁
c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos
⊢ ∀ (s₁ s₂ : String) (i₁ i₂ : Pos),
    Iterator.hasNext { s := s₂, i := i₂ } = true →
      ¬Iterator.hasNext { s := s₁, i := i₁ } = true →
        match { s := s₁, i := i₁ } with
        | { s := { data := cs₁ }, i := i₁ } =>
          match { s := s₂, i := i₂ } with
          | { s := { data := cs₂ }, i := i₂ } =>
            ltb { s := { data := c :: cs₁ }, i := i₁ + c } { s := { data := c :: cs₂ }, i := i₂ + c } =
              ltb { s := { data := cs₁ }, i := i₁ } { s := { data := cs₂ }, i := i₂ }
[PROOFSTEP]
simp
[GOAL]
case base₂
c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos
⊢ ∀ (s₁ s₂ : String) (i₁ i₂ : Pos),
    ¬Iterator.hasNext { s := s₂, i := i₂ } = true →
      match { s := s₁, i := i₁ } with
      | { s := { data := cs₁ }, i := i₁ } =>
        match { s := s₂, i := i₂ } with
        | { s := { data := cs₂ }, i := i₂ } =>
          ltb { s := { data := c :: cs₁ }, i := i₁ + c } { s := { data := c :: cs₂ }, i := i₂ + c } =
            ltb { s := { data := cs₁ }, i := i₁ } { s := { data := cs₂ }, i := i₂ }
[PROOFSTEP]
simp
[GOAL]
case ind
c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos
⊢ ∀ (s₁ s₂ : String) (i₁ i₂ : Pos),
    Iterator.hasNext { s := s₂, i := i₂ } = true →
      Iterator.hasNext { s := s₁, i := i₁ } = true →
        get s₁ i₁ = get s₂ i₂ →
          ltb
                { s := { data := c :: (Iterator.next { s := s₁, i := i₁ }).1.data },
                  i := (Iterator.next { s := s₁, i := i₁ }).i + c }
                { s := { data := c :: (Iterator.next { s := s₂, i := i₂ }).1.data },
                  i := (Iterator.next { s := s₂, i := i₂ }).i + c } =
              ltb
                { s := { data := (Iterator.next { s := s₁, i := i₁ }).1.data },
                  i := (Iterator.next { s := s₁, i := i₁ }).i }
                { s := { data := (Iterator.next { s := s₂, i := i₂ }).1.data },
                  i := (Iterator.next { s := s₂, i := i₂ }).i } →
            ltb { s := { data := c :: s₁.data }, i := i₁ + c } { s := { data := c :: s₂.data }, i := i₂ + c } =
              ltb { s := { data := s₁.data }, i := i₁ } { s := { data := s₂.data }, i := i₂ }
[PROOFSTEP]
intro ⟨cs₁⟩ ⟨cs₂⟩ i₁ i₂
[GOAL]
case eq
c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos
⊢ ∀ (s₁ s₂ : String) (i₁ i₂ : Pos),
    Iterator.hasNext { s := s₂, i := i₂ } = true →
      Iterator.hasNext { s := s₁, i := i₁ } = true →
        ¬get s₁ i₁ = get s₂ i₂ →
          ltb { s := { data := c :: s₁.data }, i := i₁ + c } { s := { data := c :: s₂.data }, i := i₂ + c } =
            ltb { s := { data := s₁.data }, i := i₁ } { s := { data := s₂.data }, i := i₂ }
[PROOFSTEP]
intro ⟨cs₁⟩ ⟨cs₂⟩ i₁ i₂
[GOAL]
case base₁
c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos
⊢ ∀ (s₁ s₂ : String) (i₁ i₂ : Pos),
    Iterator.hasNext { s := s₂, i := i₂ } = true →
      Iterator.hasNext { s := s₁, i := i₁ } = false →
        ltb { s := { data := c :: s₁.data }, i := i₁ + c } { s := { data := c :: s₂.data }, i := i₂ + c } =
          ltb { s := { data := s₁.data }, i := i₁ } { s := { data := s₂.data }, i := i₂ }
[PROOFSTEP]
intro ⟨cs₁⟩ ⟨cs₂⟩ i₁ i₂
[GOAL]
case base₂
c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos
⊢ ∀ (s₁ s₂ : String) (i₁ i₂ : Pos),
    Iterator.hasNext { s := s₂, i := i₂ } = false →
      ltb { s := { data := c :: s₁.data }, i := i₁ + c } { s := { data := c :: s₂.data }, i := i₂ + c } =
        ltb { s := { data := s₁.data }, i := i₁ } { s := { data := s₂.data }, i := i₂ }
[PROOFSTEP]
intro ⟨cs₁⟩ ⟨cs₂⟩ i₁ i₂
[GOAL]
case ind
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
⊢ Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true →
    Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true →
      get { data := cs₁ } i₁ = get { data := cs₂ } i₂ →
        ltb
              { s := { data := c :: (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
                i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i + c }
              { s := { data := c :: (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
                i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i + c } =
            ltb
              { s := { data := (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
                i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i }
              { s := { data := (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
                i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i } →
          ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
              { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
            ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
intros
[GOAL]
case eq
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
⊢ Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true →
    Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true →
      ¬get { data := cs₁ } i₁ = get { data := cs₂ } i₂ →
        ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
            { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
          ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
intros
[GOAL]
case base₁
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
⊢ Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true →
    Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = false →
      ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
          { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
        ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
intros
[GOAL]
case base₂
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
⊢ Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = false →
    ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
        { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
      ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
intros
[GOAL]
case ind
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝³ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝² : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝¹ : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
a✝ :
  ltb
      { s := { data := c :: (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i + c }
      { s := { data := c :: (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i + c } =
    ltb
      { s := { data := (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i }
      { s := { data := (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i }
⊢ ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
conv => lhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝³ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝² : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝¹ : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
a✝ :
  ltb
      { s := { data := c :: (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i + c }
      { s := { data := c :: (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i + c } =
    ltb
      { s := { data := (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i }
      { s := { data := (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i }
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
lhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝³ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝² : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝¹ : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
a✝ :
  ltb
      { s := { data := c :: (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i + c }
      { s := { data := c :: (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i + c } =
    ltb
      { s := { data := (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i }
      { s := { data := (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i }
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
lhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝³ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝² : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝¹ : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
a✝ :
  ltb
      { s := { data := c :: (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i + c }
      { s := { data := c :: (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i + c } =
    ltb
      { s := { data := (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i }
      { s := { data := (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i }
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
lhs
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝³ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝² : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝¹ : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
a✝ :
  ltb
      { s := { data := c :: (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i + c }
      { s := { data := c :: (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i + c } =
    ltb
      { s := { data := (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i }
      { s := { data := (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i }
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
    { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c }
[PROOFSTEP]
rw [ltb]
[GOAL]
case eq
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝² : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝¹ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝ : ¬get { data := cs₁ } i₁ = get { data := cs₂ } i₂
⊢ ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
conv => lhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝² : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝¹ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝ : ¬get { data := cs₁ } i₁ = get { data := cs₂ } i₂
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
lhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝² : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝¹ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝ : ¬get { data := cs₁ } i₁ = get { data := cs₂ } i₂
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
lhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝² : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝¹ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝ : ¬get { data := cs₁ } i₁ = get { data := cs₂ } i₂
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
lhs
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝² : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝¹ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝ : ¬get { data := cs₁ } i₁ = get { data := cs₂ } i₂
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
    { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c }
[PROOFSTEP]
rw [ltb]
[GOAL]
case base₁
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝¹ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = false
⊢ ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
conv => lhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝¹ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = false
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
lhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝¹ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = false
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
lhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝¹ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = false
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
lhs
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝¹ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = false
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
    { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c }
[PROOFSTEP]
rw [ltb]
[GOAL]
case base₂
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = false
⊢ ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
conv => lhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = false
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
lhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = false
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
lhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = false
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
      { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
lhs
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = false
| ltb { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c }
    { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c }
[PROOFSTEP]
rw [ltb]
[GOAL]
case ind
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝³ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝² : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝¹ : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
a✝ :
  ltb
      { s := { data := c :: (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i + c }
      { s := { data := c :: (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i + c } =
    ltb
      { s := { data := (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i }
      { s := { data := (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i }
⊢ (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
conv => rhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝³ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝² : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝¹ : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
a✝ :
  ltb
      { s := { data := c :: (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i + c }
      { s := { data := c :: (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i + c } =
    ltb
      { s := { data := (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i }
      { s := { data := (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i }
| (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝³ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝² : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝¹ : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
a✝ :
  ltb
      { s := { data := c :: (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i + c }
      { s := { data := c :: (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i + c } =
    ltb
      { s := { data := (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i }
      { s := { data := (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i }
| (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝³ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝² : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝¹ : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
a✝ :
  ltb
      { s := { data := c :: (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i + c }
      { s := { data := c :: (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i + c } =
    ltb
      { s := { data := (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i }
      { s := { data := (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i }
| (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rhs
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝³ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝² : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝¹ : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
a✝ :
  ltb
      { s := { data := c :: (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i + c }
      { s := { data := c :: (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i + c } =
    ltb
      { s := { data := (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i }
      { s := { data := (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i }
| ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rw [ltb]
[GOAL]
case eq
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝² : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝¹ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝ : ¬get { data := cs₁ } i₁ = get { data := cs₂ } i₂
⊢ (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
conv => rhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝² : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝¹ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝ : ¬get { data := cs₁ } i₁ = get { data := cs₂ } i₂
| (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝² : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝¹ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝ : ¬get { data := cs₁ } i₁ = get { data := cs₂ } i₂
| (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝² : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝¹ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝ : ¬get { data := cs₁ } i₁ = get { data := cs₂ } i₂
| (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rhs
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝² : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝¹ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝ : ¬get { data := cs₁ } i₁ = get { data := cs₂ } i₂
| ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rw [ltb]
[GOAL]
case base₁
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝¹ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = false
⊢ (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
conv => rhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝¹ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = false
| (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝¹ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = false
| (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝¹ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = false
| (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rhs
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝¹ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = false
| ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rw [ltb]
[GOAL]
case base₂
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = false
⊢ (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
conv => rhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = false
| (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = false
| (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rhs; rw [ltb]
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = false
| (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rhs
[GOAL]
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = false
| ltb { s := { data := { data := cs₁ }.data }, i := i₁ } { s := { data := { data := cs₂ }.data }, i := i₂ }
[PROOFSTEP]
rw [ltb]
[GOAL]
case ind
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝³ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝² : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝¹ : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
a✝ :
  ltb
      { s := { data := c :: (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i + c }
      { s := { data := c :: (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i + c } =
    ltb
      { s := { data := (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i }
      { s := { data := (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i }
⊢ (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    if Iterator.hasNext { s := { data := { data := cs₂ }.data }, i := i₂ } = true then
      if Iterator.hasNext { s := { data := { data := cs₁ }.data }, i := i₁ } = true then
        if
            Iterator.curr { s := { data := { data := cs₁ }.data }, i := i₁ } =
              Iterator.curr { s := { data := { data := cs₂ }.data }, i := i₂ } then
          ltb (Iterator.next { s := { data := { data := cs₁ }.data }, i := i₁ })
            (Iterator.next { s := { data := { data := cs₂ }.data }, i := i₂ })
        else
          decide
            (Iterator.curr { s := { data := { data := cs₁ }.data }, i := i₁ } <
              Iterator.curr { s := { data := { data := cs₂ }.data }, i := i₂ })
      else true
    else false
[PROOFSTEP]
simp [Iterator.hasNext_cons_addChar, *]
[GOAL]
case eq
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝² : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝¹ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝ : ¬get { data := cs₁ } i₁ = get { data := cs₂ } i₂
⊢ (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    if Iterator.hasNext { s := { data := { data := cs₂ }.data }, i := i₂ } = true then
      if Iterator.hasNext { s := { data := { data := cs₁ }.data }, i := i₁ } = true then
        if
            Iterator.curr { s := { data := { data := cs₁ }.data }, i := i₁ } =
              Iterator.curr { s := { data := { data := cs₂ }.data }, i := i₂ } then
          ltb (Iterator.next { s := { data := { data := cs₁ }.data }, i := i₁ })
            (Iterator.next { s := { data := { data := cs₂ }.data }, i := i₂ })
        else
          decide
            (Iterator.curr { s := { data := { data := cs₁ }.data }, i := i₁ } <
              Iterator.curr { s := { data := { data := cs₂ }.data }, i := i₂ })
      else true
    else false
[PROOFSTEP]
simp [Iterator.hasNext_cons_addChar, *]
[GOAL]
case base₁
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝¹ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = false
⊢ (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    if Iterator.hasNext { s := { data := { data := cs₂ }.data }, i := i₂ } = true then
      if Iterator.hasNext { s := { data := { data := cs₁ }.data }, i := i₁ } = true then
        if
            Iterator.curr { s := { data := { data := cs₁ }.data }, i := i₁ } =
              Iterator.curr { s := { data := { data := cs₂ }.data }, i := i₂ } then
          ltb (Iterator.next { s := { data := { data := cs₁ }.data }, i := i₁ })
            (Iterator.next { s := { data := { data := cs₂ }.data }, i := i₂ })
        else
          decide
            (Iterator.curr { s := { data := { data := cs₁ }.data }, i := i₁ } <
              Iterator.curr { s := { data := { data := cs₂ }.data }, i := i₂ })
      else true
    else false
[PROOFSTEP]
simp [Iterator.hasNext_cons_addChar, *]
[GOAL]
case base₂
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = false
⊢ (if Iterator.hasNext { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } = true then
      if Iterator.hasNext { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } = true then
        if
            Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } =
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c } then
          ltb (Iterator.next { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c })
            (Iterator.next { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
        else
          decide
            (Iterator.curr { s := { data := c :: { data := cs₁ }.data }, i := i₁ + c } <
              Iterator.curr { s := { data := c :: { data := cs₂ }.data }, i := i₂ + c })
      else true
    else false) =
    if Iterator.hasNext { s := { data := { data := cs₂ }.data }, i := i₂ } = true then
      if Iterator.hasNext { s := { data := { data := cs₁ }.data }, i := i₁ } = true then
        if
            Iterator.curr { s := { data := { data := cs₁ }.data }, i := i₁ } =
              Iterator.curr { s := { data := { data := cs₂ }.data }, i := i₂ } then
          ltb (Iterator.next { s := { data := { data := cs₁ }.data }, i := i₁ })
            (Iterator.next { s := { data := { data := cs₂ }.data }, i := i₂ })
        else
          decide
            (Iterator.curr { s := { data := { data := cs₁ }.data }, i := i₁ } <
              Iterator.curr { s := { data := { data := cs₂ }.data }, i := i₂ })
      else true
    else false
[PROOFSTEP]
simp [Iterator.hasNext_cons_addChar, *]
[GOAL]
case ind
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝³ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝² : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝¹ : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
a✝ :
  ltb
      { s := { data := c :: (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i + c }
      { s := { data := c :: (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i + c } =
    ltb
      { s := { data := (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i }
      { s := { data := (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i }
⊢ (if
        Iterator.curr { s := { data := c :: cs₁ }, i := i₁ + c } =
          Iterator.curr { s := { data := c :: cs₂ }, i := i₂ + c } then
      ltb (Iterator.next { s := { data := c :: cs₁ }, i := i₁ + c })
        (Iterator.next { s := { data := c :: cs₂ }, i := i₂ + c })
    else
      decide
        (Iterator.curr { s := { data := c :: cs₁ }, i := i₁ + c } <
          Iterator.curr { s := { data := c :: cs₂ }, i := i₂ + c })) =
    if Iterator.curr { s := { data := cs₁ }, i := i₁ } = Iterator.curr { s := { data := cs₂ }, i := i₂ } then
      ltb (Iterator.next { s := { data := cs₁ }, i := i₁ }) (Iterator.next { s := { data := cs₂ }, i := i₂ })
    else decide (Iterator.curr { s := { data := cs₁ }, i := i₁ } < Iterator.curr { s := { data := cs₂ }, i := i₂ })
[PROOFSTEP]
rename_i h₂ h₁ heq ih
[GOAL]
case ind
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
h₂ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
h₁ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
heq : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
ih :
  ltb
      { s := { data := c :: (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i + c }
      { s := { data := c :: (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i + c } =
    ltb
      { s := { data := (Iterator.next { s := { data := cs₁ }, i := i₁ }).1.data },
        i := (Iterator.next { s := { data := cs₁ }, i := i₁ }).i }
      { s := { data := (Iterator.next { s := { data := cs₂ }, i := i₂ }).1.data },
        i := (Iterator.next { s := { data := cs₂ }, i := i₂ }).i }
⊢ (if
        Iterator.curr { s := { data := c :: cs₁ }, i := i₁ + c } =
          Iterator.curr { s := { data := c :: cs₂ }, i := i₂ + c } then
      ltb (Iterator.next { s := { data := c :: cs₁ }, i := i₁ + c })
        (Iterator.next { s := { data := c :: cs₂ }, i := i₂ + c })
    else
      decide
        (Iterator.curr { s := { data := c :: cs₁ }, i := i₁ + c } <
          Iterator.curr { s := { data := c :: cs₂ }, i := i₂ + c })) =
    if Iterator.curr { s := { data := cs₁ }, i := i₁ } = Iterator.curr { s := { data := cs₂ }, i := i₂ } then
      ltb (Iterator.next { s := { data := cs₁ }, i := i₁ }) (Iterator.next { s := { data := cs₂ }, i := i₂ })
    else decide (Iterator.curr { s := { data := cs₁ }, i := i₁ } < Iterator.curr { s := { data := cs₂ }, i := i₂ })
[PROOFSTEP]
simp [Iterator.curr, get_cons_addChar, Iterator.next, next, *] at *
[GOAL]
case ind
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
h₂ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
h₁ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
heq : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
ih :
  ltb { s := { data := c :: cs₁ }, i := i₁ + get { data := cs₂ } i₂ + c }
      { s := { data := c :: cs₂ }, i := i₂ + get { data := cs₂ } i₂ + c } =
    ltb { s := { data := cs₁ }, i := i₁ + get { data := cs₂ } i₂ }
      { s := { data := cs₂ }, i := i₂ + get { data := cs₂ } i₂ }
⊢ ltb { s := { data := c :: cs₁ }, i := i₁ + c + get { data := cs₂ } i₂ }
      { s := { data := c :: cs₂ }, i := i₂ + c + get { data := cs₂ } i₂ } =
    ltb { s := { data := cs₁ }, i := i₁ + get { data := cs₂ } i₂ }
      { s := { data := cs₂ }, i := i₂ + get { data := cs₂ } i₂ }
[PROOFSTEP]
repeat rw [Pos.addChar_right_comm _ c]
[GOAL]
case ind
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
h₂ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
h₁ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
heq : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
ih :
  ltb { s := { data := c :: cs₁ }, i := i₁ + get { data := cs₂ } i₂ + c }
      { s := { data := c :: cs₂ }, i := i₂ + get { data := cs₂ } i₂ + c } =
    ltb { s := { data := cs₁ }, i := i₁ + get { data := cs₂ } i₂ }
      { s := { data := cs₂ }, i := i₂ + get { data := cs₂ } i₂ }
⊢ ltb { s := { data := c :: cs₁ }, i := i₁ + c + get { data := cs₂ } i₂ }
      { s := { data := c :: cs₂ }, i := i₂ + c + get { data := cs₂ } i₂ } =
    ltb { s := { data := cs₁ }, i := i₁ + get { data := cs₂ } i₂ }
      { s := { data := cs₂ }, i := i₂ + get { data := cs₂ } i₂ }
[PROOFSTEP]
rw [Pos.addChar_right_comm _ c]
[GOAL]
case ind
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
h₂ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
h₁ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
heq : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
ih :
  ltb { s := { data := c :: cs₁ }, i := i₁ + get { data := cs₂ } i₂ + c }
      { s := { data := c :: cs₂ }, i := i₂ + get { data := cs₂ } i₂ + c } =
    ltb { s := { data := cs₁ }, i := i₁ + get { data := cs₂ } i₂ }
      { s := { data := cs₂ }, i := i₂ + get { data := cs₂ } i₂ }
⊢ ltb { s := { data := c :: cs₁ }, i := i₁ + get { data := cs₂ } i₂ + c }
      { s := { data := c :: cs₂ }, i := i₂ + c + get { data := cs₂ } i₂ } =
    ltb { s := { data := cs₁ }, i := i₁ + get { data := cs₂ } i₂ }
      { s := { data := cs₂ }, i := i₂ + get { data := cs₂ } i₂ }
[PROOFSTEP]
rw [Pos.addChar_right_comm _ c]
[GOAL]
case ind
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
h₂ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
h₁ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
heq : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
ih :
  ltb { s := { data := c :: cs₁ }, i := i₁ + get { data := cs₂ } i₂ + c }
      { s := { data := c :: cs₂ }, i := i₂ + get { data := cs₂ } i₂ + c } =
    ltb { s := { data := cs₁ }, i := i₁ + get { data := cs₂ } i₂ }
      { s := { data := cs₂ }, i := i₂ + get { data := cs₂ } i₂ }
⊢ ltb { s := { data := c :: cs₁ }, i := i₁ + get { data := cs₂ } i₂ + c }
      { s := { data := c :: cs₂ }, i := i₂ + get { data := cs₂ } i₂ + c } =
    ltb { s := { data := cs₁ }, i := i₁ + get { data := cs₂ } i₂ }
      { s := { data := cs₂ }, i := i₂ + get { data := cs₂ } i₂ }
[PROOFSTEP]
rw [Pos.addChar_right_comm _ c]
[GOAL]
case ind
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
h₂ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
h₁ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
heq : get { data := cs₁ } i₁ = get { data := cs₂ } i₂
ih :
  ltb { s := { data := c :: cs₁ }, i := i₁ + get { data := cs₂ } i₂ + c }
      { s := { data := c :: cs₂ }, i := i₂ + get { data := cs₂ } i₂ + c } =
    ltb { s := { data := cs₁ }, i := i₁ + get { data := cs₂ } i₂ }
      { s := { data := cs₂ }, i := i₂ + get { data := cs₂ } i₂ }
⊢ ltb { s := { data := c :: cs₁ }, i := i₁ + get { data := cs₂ } i₂ + c }
      { s := { data := c :: cs₂ }, i := i₂ + get { data := cs₂ } i₂ + c } =
    ltb { s := { data := cs₁ }, i := i₁ + get { data := cs₂ } i₂ }
      { s := { data := cs₂ }, i := i₂ + get { data := cs₂ } i₂ }
[PROOFSTEP]
exact ih
[GOAL]
case eq
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
a✝² : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
a✝¹ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
a✝ : ¬get { data := cs₁ } i₁ = get { data := cs₂ } i₂
⊢ (if
        Iterator.curr { s := { data := c :: cs₁ }, i := i₁ + c } =
          Iterator.curr { s := { data := c :: cs₂ }, i := i₂ + c } then
      ltb (Iterator.next { s := { data := c :: cs₁ }, i := i₁ + c })
        (Iterator.next { s := { data := c :: cs₂ }, i := i₂ + c })
    else
      decide
        (Iterator.curr { s := { data := c :: cs₁ }, i := i₁ + c } <
          Iterator.curr { s := { data := c :: cs₂ }, i := i₂ + c })) =
    if Iterator.curr { s := { data := cs₁ }, i := i₁ } = Iterator.curr { s := { data := cs₂ }, i := i₂ } then
      ltb (Iterator.next { s := { data := cs₁ }, i := i₁ }) (Iterator.next { s := { data := cs₂ }, i := i₂ })
    else decide (Iterator.curr { s := { data := cs₁ }, i := i₁ } < Iterator.curr { s := { data := cs₂ }, i := i₂ })
[PROOFSTEP]
rename_i h₂ h₁ hne
[GOAL]
case eq
c : Char
cs₁✝ cs₂✝ : List Char
i₁✝ i₂✝ : Pos
cs₁ cs₂ : List Char
i₁ i₂ : Pos
h₂ : Iterator.hasNext { s := { data := cs₂ }, i := i₂ } = true
h₁ : Iterator.hasNext { s := { data := cs₁ }, i := i₁ } = true
hne : ¬get { data := cs₁ } i₁ = get { data := cs₂ } i₂
⊢ (if
        Iterator.curr { s := { data := c :: cs₁ }, i := i₁ + c } =
          Iterator.curr { s := { data := c :: cs₂ }, i := i₂ + c } then
      ltb (Iterator.next { s := { data := c :: cs₁ }, i := i₁ + c })
        (Iterator.next { s := { data := c :: cs₂ }, i := i₂ + c })
    else
      decide
        (Iterator.curr { s := { data := c :: cs₁ }, i := i₁ + c } <
          Iterator.curr { s := { data := c :: cs₂ }, i := i₂ + c })) =
    if Iterator.curr { s := { data := cs₁ }, i := i₁ } = Iterator.curr { s := { data := cs₂ }, i := i₂ } then
      ltb (Iterator.next { s := { data := cs₁ }, i := i₁ }) (Iterator.next { s := { data := cs₂ }, i := i₂ })
    else decide (Iterator.curr { s := { data := cs₁ }, i := i₁ } < Iterator.curr { s := { data := cs₂ }, i := i₂ })
[PROOFSTEP]
simp [Iterator.curr, get_cons_addChar, *]
[GOAL]
s₁ s₂ : List Char
⊢ ltb { s := { data := s₁ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ s₁ < s₂
[PROOFSTEP]
induction s₁ generalizing s₂
[GOAL]
case nil
s₂ : List Char
⊢ ltb { s := { data := [] }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ [] < s₂
[PROOFSTEP]
cases s₂
[GOAL]
case 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₂
s₂ : List Char
⊢ ltb { s := { data := head✝ :: tail✝ }, i := 0 } { s := { data := s₂ }, i := 0 } = true ↔ head✝ :: tail✝ < s₂
[PROOFSTEP]
cases s₂
[GOAL]
case nil.nil
⊢ ltb { s := { data := [] }, i := 0 } { s := { data := [] }, i := 0 } = true ↔ [] < []
[PROOFSTEP]
simp
[GOAL]
case nil.cons
head✝ : Char
tail✝ : List Char
⊢ ltb { s := { data := [] }, i := 0 } { s := { data := head✝ :: tail✝ }, i := 0 } = true ↔ [] < head✝ :: tail✝
[PROOFSTEP]
rename_i c₂ cs₂
[GOAL]
case nil.cons
c₂ : Char
cs₂ : List Char
⊢ ltb { s := { data := [] }, i := 0 } { s := { data := c₂ :: cs₂ }, i := 0 } = true ↔ [] < c₂ :: cs₂
[PROOFSTEP]
apply iff_of_true
[GOAL]
case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ ltb { s := { data := [] }, i := 0 } { s := { data := c₂ :: cs₂ }, i := 0 } = true
[PROOFSTEP]
rw [ltb]
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ Iterator.hasNext { s := { data := c₂ :: cs₂ }, i := 0 } = false → False
[PROOFSTEP]
apply ne_false_of_eq_true
[GOAL]
case nil.cons.ha.a
c₂ : Char
cs₂ : List Char
⊢ Iterator.hasNext { s := { data := c₂ :: cs₂ }, i := 0 } = true
[PROOFSTEP]
apply decide_eq_true
[GOAL]
case nil.cons.ha.a.a
c₂ : Char
cs₂ : List Char
⊢ 0.byteIdx < (endPos { data := c₂ :: cs₂ }).byteIdx
[PROOFSTEP]
simp [endPos, utf8ByteSize, utf8ByteSize.go, csize_pos]
[GOAL]
case nil.cons.hb
c₂ : Char
cs₂ : List Char
⊢ [] < c₂ :: cs₂
[PROOFSTEP]
apply List.nil_lt_cons
[GOAL]
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✝ < []
[PROOFSTEP]
rename_i c₁ cs₁ ih
[GOAL]
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₁ < []
[PROOFSTEP]
apply iff_of_false
[GOAL]
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
[PROOFSTEP]
rw [ltb]
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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₁ < []
[PROOFSTEP]
apply not_lt_of_lt
[GOAL]
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₁
[PROOFSTEP]
apply List.nil_lt_cons
[GOAL]
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✝
[PROOFSTEP]
rename_i c₁ cs₁ ih c₂ cs₂
[GOAL]
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₂
[PROOFSTEP]
rw [ltb]
[GOAL]
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₂
[PROOFSTEP]
simp [Iterator.hasNext, endPos, utf8ByteSize, utf8ByteSize.go, csize_pos, Iterator.curr, get, utf8GetAux, Iterator.next,
  next]
[GOAL]
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₂
[PROOFSTEP]
split_ifs with h
[GOAL]
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₂
[PROOFSTEP]
subst c₂
[GOAL]
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₂
[PROOFSTEP]
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
[GOAL]
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₂
[PROOFSTEP]
rw [Pos.zero_addChar_eq, this]
[GOAL]
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₂
[PROOFSTEP]
exact (ih cs₂).trans List.Lex.cons_iff.symm
[GOAL]
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 := { byteIdx := csize c₁ } }
      { s := { data := c₁ :: cs₂ }, i := { byteIdx := csize c₁ } } =
    ltb { s := { data := cs₁ }, i := 0 } { s := { data := cs₂ }, i := 0 }
[PROOFSTEP]
rw [← Pos.zero_addChar_eq]
[GOAL]
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 }
[PROOFSTEP]
apply ltb_cons_addChar
[GOAL]
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₂
[PROOFSTEP]
refine ⟨List.Lex.rel, fun e ↦ ?_⟩
[GOAL]
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₂
[PROOFSTEP]
cases e
[GOAL]
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 x x_1 => x < x_1) cs₁ cs₂
⊢ c₁ < c₁
[PROOFSTEP]
rename_i h'
[GOAL]
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₂
[PROOFSTEP]
rename_i h'
[GOAL]
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 x x_1 => x < x_1) cs₁ cs₂
⊢ c₁ < c₁
[PROOFSTEP]
contradiction
[GOAL]
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₂
[PROOFSTEP]
assumption
[GOAL]
⊢ DecidableRel fun x x_1 => x ≤ x_1
[PROOFSTEP]
simp only [LE]
[GOAL]
⊢ DecidableRel fun s₁ s₂ => ¬s₂ < s₁
[PROOFSTEP]
infer_instance
  -- short-circuit type class inference
[GOAL]
s : List Char
h : { data := s } ≠ ""
⊢ toList { data := s } = head { data := s } :: toList (drop { data := s } 1)
[PROOFSTEP]
cases s
[GOAL]
case nil
h : { data := [] } ≠ ""
⊢ toList { data := [] } = head { data := [] } :: toList (drop { data := [] } 1)
[PROOFSTEP]
simp only at h 
[GOAL]
case cons
head✝ : Char
tail✝ : List Char
h : { data := head✝ :: tail✝ } ≠ ""
⊢ toList { data := head✝ :: tail✝ } = head { data := head✝ :: tail✝ } :: toList (drop { data := head✝ :: tail✝ } 1)
[PROOFSTEP]
rename_i c cs
[GOAL]
case cons
c : Char
cs : List Char
h : { data := c :: cs } ≠ ""
⊢ toList { data := c :: cs } = head { data := c :: cs } :: toList (drop { data := c :: cs } 1)
[PROOFSTEP]
simp only [toList, List.cons.injEq]
[GOAL]
case cons
c : Char
cs : List Char
h : { data := c :: cs } ≠ ""
⊢ c = head { data := c :: cs } ∧ cs = (drop { data := c :: cs } 1).data
[PROOFSTEP]
constructor <;> [rfl; simp [drop_eq]]
[GOAL]
case cons
c : Char
cs : List Char
h : { data := c :: cs } ≠ ""
⊢ c = head { data := c :: cs } ∧ cs = (drop { data := c :: cs } 1).data
[PROOFSTEP]
constructor
[GOAL]
case cons.left
c : Char
cs : List Char
h : { data := c :: cs } ≠ ""
⊢ c = head { data := c :: cs }
[PROOFSTEP]
rfl
[GOAL]
case cons.right
c : Char
cs : List Char
h : { data := c :: cs } ≠ ""
⊢ cs = (drop { data := c :: cs } 1).data
[PROOFSTEP]
simp [drop_eq]
[GOAL]
a b c : String
⊢ a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
simp only [le_iff_toList_le]
[GOAL]
a b c : String
⊢ toList a ≤ toList b → toList b ≤ toList c → toList a ≤ toList c
[PROOFSTEP]
apply le_trans
[GOAL]
a b : String
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
simp only [lt_iff_toList_lt, le_iff_toList_le, lt_iff_le_not_le]
[GOAL]
a b : String
⊢ a ≤ b → b ≤ a → a = b
[PROOFSTEP]
simp only [le_iff_toList_le, ← toList_inj]
[GOAL]
a b : String
⊢ toList a ≤ toList b → toList b ≤ toList a → toList a = toList b
[PROOFSTEP]
apply le_antisymm
[GOAL]
a b : String
⊢ a ≤ b ∨ b ≤ a
[PROOFSTEP]
simp only [le_iff_toList_le]
[GOAL]
a b : String
⊢ toList a ≤ toList b ∨ toList b ≤ toList a
[PROOFSTEP]
apply le_total
[GOAL]
a b : String
⊢ compare a b = compareOfLessAndEq a b
[PROOFSTEP]
simp [compare, compareOfLessAndEq, toList, instLTString, List.instLTList, List.LT']
[GOAL]
a b : String
⊢ (if List.lt a.data b.data then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if List.Lex (fun x x_1 => x < x_1) a.data b.data then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
[PROOFSTEP]
split_ifs
[GOAL]
case pos
a b : String
h✝¹ : List.lt a.data b.data
h✝ : List.Lex (fun x x_1 => x < x_1) a.data b.data
⊢ Ordering.lt = Ordering.lt
[PROOFSTEP]
simp [List.lt_iff_lex_lt] at *
[GOAL]
case pos
a b : String
h✝² : List.lt a.data b.data
h✝¹ : ¬List.Lex (fun x x_1 => x < x_1) a.data b.data
h✝ : a = b
⊢ False
[PROOFSTEP]
simp [List.lt_iff_lex_lt] at *
[GOAL]
case neg
a b : String
h✝² : List.lt a.data b.data
h✝¹ : ¬List.Lex (fun x x_1 => x < x_1) a.data b.data
h✝ : ¬a = b
⊢ False
[PROOFSTEP]
simp [List.lt_iff_lex_lt] at *
[GOAL]
case pos
a b : String
h✝² : ¬List.lt a.data b.data
h✝¹ : a = b
h✝ : List.Lex (fun x x_1 => x < x_1) a.data b.data
⊢ False
[PROOFSTEP]
simp [List.lt_iff_lex_lt] at *
[GOAL]
case neg
a b : String
h✝² : ¬List.lt a.data b.data
h✝¹ : a = b
h✝ : ¬List.Lex (fun x x_1 => x < x_1) a.data b.data
⊢ Ordering.eq = Ordering.eq
[PROOFSTEP]
simp [List.lt_iff_lex_lt] at *
[GOAL]
case pos
a b : String
h✝² : ¬List.lt a.data b.data
h✝¹ : ¬a = b
h✝ : List.Lex (fun x x_1 => x < x_1) a.data b.data
⊢ False
[PROOFSTEP]
simp [List.lt_iff_lex_lt] at *
[GOAL]
case neg
a b : String
h✝² : ¬List.lt a.data b.data
h✝¹ : ¬a = b
h✝ : ¬List.Lex (fun x x_1 => x < x_1) a.data b.data
⊢ Ordering.gt = Ordering.gt
[PROOFSTEP]
simp [List.lt_iff_lex_lt] at *
[GOAL]
case pos
a b : String
h✝² : ¬List.Lex (fun x x_1 => x < x_1) a.data b.data
h✝¹ : a = b
h✝ : List.Lex (fun x x_1 => x < x_1) a.data b.data
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case neg
a b : String
h✝² : ¬List.Lex (fun x x_1 => x < x_1) a.data b.data
h✝¹ : ¬a = b
h✝ : List.Lex (fun x x_1 => x < x_1) a.data b.data
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
a b : String
h✝² : a = b
h✝¹ : List.Lex (fun x x_1 => x < x_1) a.data b.data
h✝ : ¬List.Lex (fun x x_1 => x < x_1) a.data b.data
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
a b : String
h✝² : ¬a = b
h✝¹ : List.Lex (fun x x_1 => x < x_1) a.data b.data
h✝ : ¬List.Lex (fun x x_1 => x < x_1) a.data b.data
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
l l' : List Char
h : asString l = asString l'
⊢ l = l'
[PROOFSTEP]
rw [← toList_inv_asString l, ← toList_inv_asString l', toList_inj, h]
[GOAL]
l : List Char
s : String
⊢ asString l = s ↔ l = toList s
[PROOFSTEP]
rw [← asString_inv_toList s, asString_inj, asString_inv_toList s]
