[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]


[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : SemilatticeSup α
s s₁ s₂ t t₁ t₂ u v : Finset α
a b c : α
⊢ c ∈ s ⊻ t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = c
[PROOFSTEP]
simp [(· ⊻ ·)]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : SemilatticeInf α
s s₁ s₂ t t₁ t₂ u v : Finset α
a b c : α
⊢ c ∈ s ⊼ t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = c
[PROOFSTEP]
simp [(· ⊼ ·)]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ c ∈ s ○ t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = c
[PROOFSTEP]
simp [disjSups, and_assoc]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ s ○ t ⊆ s ⊻ t
[PROOFSTEP]
simp_rw [subset_iff, mem_sups, mem_disjSups]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ ∀ ⦃x : α⦄, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = x) → ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊔ b = x
[PROOFSTEP]
exact fun c ⟨a, b, ha, hb, _, hc⟩ => ⟨a, b, ha, hb, hc⟩
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
p : α → Prop
⊢ (∀ (c : α), c ∈ s ○ t → p c) ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)
[PROOFSTEP]
simp_rw [mem_disjSups]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
p : α → Prop
⊢ (∀ (c : α), (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = c) → p c) ↔
    ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)
[PROOFSTEP]
refine' ⟨fun h a ha b hb hab => h _ ⟨_, ha, _, hb, hab, rfl⟩, _⟩
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
p : α → Prop
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)) →
    ∀ (c : α), (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = c) → p c
[PROOFSTEP]
rintro h _ ⟨a, ha, b, hb, hab, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝ b✝ c : α
p : α → Prop
h : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
⊢ p (a ⊔ b)
[PROOFSTEP]
exact h _ ha _ hb hab
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ Finset.Nonempty (s ○ t) → Finset.Nonempty s
[PROOFSTEP]
simp_rw [Finset.Nonempty, mem_disjSups]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ (∃ x a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = x) → ∃ x, x ∈ s
[PROOFSTEP]
exact fun ⟨_, a, ha, _⟩ => ⟨a, ha⟩
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ Finset.Nonempty (s ○ t) → Finset.Nonempty t
[PROOFSTEP]
simp_rw [Finset.Nonempty, mem_disjSups]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ (∃ x a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = x) → ∃ x, x ∈ t
[PROOFSTEP]
exact fun ⟨_, _, _, b, hb, _⟩ => ⟨b, hb⟩
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ ∅ ○ t = ∅
[PROOFSTEP]
simp [disjSups]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ s ○ ∅ = ∅
[PROOFSTEP]
simp [disjSups]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ {a} ○ {b} = if Disjoint a b then {a ⊔ b} else ∅
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
h : Disjoint a b
⊢ {a} ○ {b} = {a ⊔ b}
[PROOFSTEP]
simp [disjSups, filter_singleton, h]
[GOAL]
case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
h : ¬Disjoint a b
⊢ {a} ○ {b} = ∅
[PROOFSTEP]
simp [disjSups, filter_singleton, h]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ (s₁ ∪ s₂) ○ t = s₁ ○ t ∪ s₂ ○ t
[PROOFSTEP]
simp [disjSups, filter_union, image_union]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ s ○ (t₁ ∪ t₂) = s ○ t₁ ∪ s ○ t₂
[PROOFSTEP]
simp [disjSups, filter_union, image_union]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ (s₁ ∩ s₂) ○ t ⊆ s₁ ○ t ∩ s₂ ○ t
[PROOFSTEP]
simpa only [disjSups, inter_product, filter_inter_distrib] using image_inter_subset _ _ _
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ s ○ (t₁ ∩ t₂) ⊆ s ○ t₁ ∩ s ○ t₂
[PROOFSTEP]
simpa only [disjSups, product_inter, filter_inter_distrib] using image_inter_subset _ _ _
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
⊢ s ○ t = t ○ s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c a✝ : α
⊢ a✝ ∈ s ○ t ↔ a✝ ∈ t ○ s
[PROOFSTEP]
rw [mem_disjSups, mem_disjSups]
  -- Porting note: `exists₂_comm` no longer works with `∃ _ ∈ _, ∃ _ ∈ _, _`
[GOAL]
case a
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c a✝ : α
⊢ (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = a✝) ↔ ∃ a, a ∈ t ∧ ∃ b, b ∈ s ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c a✝ : α
⊢ (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = a✝) → ∃ a, a ∈ t ∧ ∃ b, b ∈ s ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
rintro ⟨a, ha, b, hb, hd, hs⟩
[GOAL]
case a.mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝¹ b✝ c a✝ a : α
ha : a ∈ s
b : α
hb : b ∈ t
hd : Disjoint a b
hs : a ⊔ b = a✝
⊢ ∃ a, a ∈ t ∧ ∃ b, b ∈ s ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
rw [disjoint_comm] at hd
[GOAL]
case a.mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝¹ b✝ c a✝ a : α
ha : a ∈ s
b : α
hb : b ∈ t
hd : Disjoint b a
hs : a ⊔ b = a✝
⊢ ∃ a, a ∈ t ∧ ∃ b, b ∈ s ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
rw [sup_comm] at hs
[GOAL]
case a.mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝¹ b✝ c a✝ a : α
ha : a ∈ s
b : α
hb : b ∈ t
hd : Disjoint b a
hs : b ⊔ a = a✝
⊢ ∃ a, a ∈ t ∧ ∃ b, b ∈ s ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
exact ⟨b, hb, a, ha, hd, hs⟩
[GOAL]
case a.mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c a✝ : α
⊢ (∃ a, a ∈ t ∧ ∃ b, b ∈ s ∧ Disjoint a b ∧ a ⊔ b = a✝) → ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
rintro ⟨a, ha, b, hb, hd, hs⟩
[GOAL]
case a.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝¹ b✝ c a✝ a : α
ha : a ∈ t
b : α
hb : b ∈ s
hd : Disjoint a b
hs : a ⊔ b = a✝
⊢ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
rw [disjoint_comm] at hd
[GOAL]
case a.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝¹ b✝ c a✝ a : α
ha : a ∈ t
b : α
hb : b ∈ s
hd : Disjoint b a
hs : a ⊔ b = a✝
⊢ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
rw [sup_comm] at hs
[GOAL]
case a.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝¹ b✝ c a✝ a : α
ha : a ∈ t
b : α
hb : b ∈ s
hd : Disjoint b a
hs : b ⊔ a = a✝
⊢ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = a✝
[PROOFSTEP]
exact ⟨b, hb, a, ha, hd, hs⟩
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ ∀ (s t u : Finset α), s ○ t ○ u = s ○ (t ○ u)
[PROOFSTEP]
refine' associative_of_commutative_of_le disjSups_comm _
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ ∀ (a b c : Finset α), a ○ b ○ c ≤ a ○ (b ○ c)
[PROOFSTEP]
simp only [le_eq_subset, disjSups_subset_iff, mem_disjSups]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ ∀ (a b c : Finset α) (a_1 : α),
    (∃ a_2, a_2 ∈ a ∧ ∃ b_1, b_1 ∈ b ∧ Disjoint a_2 b_1 ∧ a_2 ⊔ b_1 = a_1) →
      ∀ (b_1 : α),
        b_1 ∈ c →
          Disjoint a_1 b_1 →
            ∃ a_5,
              a_5 ∈ a ∧
                ∃ b_2, (∃ a, a ∈ b ∧ ∃ b, b ∈ c ∧ Disjoint a b ∧ a ⊔ b = b_2) ∧ Disjoint a_5 b_2 ∧ a_5 ⊔ b_2 = a_1 ⊔ b_1
[PROOFSTEP]
rintro s t u _ ⟨a, ha, b, hb, hab, rfl⟩ c hc habc
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s✝ t✝ u✝ v s t u : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
c : α
hc : c ∈ u
habc : Disjoint (a ⊔ b) c
⊢ ∃ a_1,
    a_1 ∈ s ∧ ∃ b_1, (∃ a, a ∈ t ∧ ∃ b, b ∈ u ∧ Disjoint a b ∧ a ⊔ b = b_1) ∧ Disjoint a_1 b_1 ∧ a_1 ⊔ b_1 = a ⊔ b ⊔ c
[PROOFSTEP]
rw [disjoint_sup_left] at habc
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s✝ t✝ u✝ v s t u : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
c : α
hc : c ∈ u
habc : Disjoint a c ∧ Disjoint b c
⊢ ∃ a_1,
    a_1 ∈ s ∧ ∃ b_1, (∃ a, a ∈ t ∧ ∃ b, b ∈ u ∧ Disjoint a b ∧ a ⊔ b = b_1) ∧ Disjoint a_1 b_1 ∧ a_1 ⊔ b_1 = a ⊔ b ⊔ c
[PROOFSTEP]
exact ⟨a, ha, _, ⟨b, hb, c, hc, habc.2, rfl⟩, hab.sup_right habc.1, sup_assoc.symm⟩
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ s ○ (t ○ u) = t ○ (s ○ u)
[PROOFSTEP]
simp_rw [← disjSups_assoc, disjSups_comm s]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ s ○ t ○ u = s ○ u ○ t
[PROOFSTEP]
simp_rw [disjSups_assoc, disjSups_comm]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ s ○ t ○ (u ○ v) = s ○ u ○ (t ○ v)
[PROOFSTEP]
simp_rw [← disjSups_assoc, disjSups_right_comm]


[GOAL]
α : Type u_1
β : Type u_2
a : α
o : Option α
⊢ a ∈ toFinset o ↔ a ∈ o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
a : α
⊢ a ∈ toFinset none ↔ a ∈ none
[PROOFSTEP]
simp [eq_comm]
[GOAL]
case some
α : Type u_1
β : Type u_2
a val✝ : α
⊢ a ∈ toFinset (some val✝) ↔ a ∈ some val✝
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
o : Option α
⊢ Finset.card (toFinset o) = Option.elim o 0 1
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
⊢ Finset.card (toFinset none) = Option.elim none 0 1
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
val✝ : α
⊢ Finset.card (toFinset (some val✝)) = Option.elim (some val✝) 0 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
⊢ ¬none ∈ map Embedding.some s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
⊢ cons none (map Embedding.some s) (_ : ¬none ∈ map Embedding.some s) ≤
      cons none (map Embedding.some t) (_ : ¬none ∈ map Embedding.some t) ↔
    s ≤ t
[PROOFSTEP]
rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
a : α
h : a ∈ none
⊢ a ∈ s
[PROOFSTEP]
cases h
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
a : α
⊢ some a = none ∨ some a ∈ (map Embedding.some s).val ↔ ∀ (a_1 : α), a_1 ∈ some a → a_1 ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
a : α
⊢ some a ∈ ↑insertNone s ↔ a ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
⊢ card (↑insertNone s) = card s + 1
[PROOFSTEP]
simp [insertNone]
[GOAL]
α : Type u_1
β : Type u_2
s : Finset (Option α)
x : α
⊢ x ∈ ↑eraseNone s ↔ some x ∈ s
[PROOFSTEP]
simp [eraseNone]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset (Option α)
⊢ ↑eraseNone s = Finset.biUnion s Option.toFinset
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset (Option α)
a✝ : α
⊢ a✝ ∈ ↑eraseNone s ↔ a✝ ∈ Finset.biUnion s Option.toFinset
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
⊢ ↑eraseNone (map Embedding.some s) = s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
s : Finset α
a✝ : α
⊢ a✝ ∈ ↑eraseNone (map Embedding.some s) ↔ a✝ ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset α
⊢ ↑eraseNone (image some s) = s
[PROOFSTEP]
simpa only [map_eq_image] using eraseNone_map_some s
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
⊢ ↑eraseNone (s ∪ t) = ↑eraseNone s ∪ ↑eraseNone t
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
a✝ : α
⊢ a✝ ∈ ↑eraseNone (s ∪ t) ↔ a✝ ∈ ↑eraseNone s ∪ ↑eraseNone t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
⊢ ↑eraseNone (s ∩ t) = ↑eraseNone s ∩ ↑eraseNone t
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
a✝ : α
⊢ a✝ ∈ ↑eraseNone (s ∩ t) ↔ a✝ ∈ ↑eraseNone s ∩ ↑eraseNone t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
⊢ ↑eraseNone ∅ = ∅
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
a✝ : α
⊢ a✝ ∈ ↑eraseNone ∅ ↔ a✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
⊢ ↑eraseNone {none} = ∅
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
a✝ : α
⊢ a✝ ∈ ↑eraseNone {none} ↔ a✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ image some (↑eraseNone s) = erase s none
[PROOFSTEP]
ext (_ | x)
[GOAL]
case a.none
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ none ∈ image some (↑eraseNone s) ↔ none ∈ erase s none
[PROOFSTEP]
simp
[GOAL]
case a.some
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
x : α
⊢ some x ∈ image some (↑eraseNone s) ↔ some x ∈ erase s none
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ map Embedding.some (↑eraseNone s) = erase s none
[PROOFSTEP]
rw [map_eq_image, Embedding.some_apply, image_some_eraseNone]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ ↑insertNone (↑eraseNone s) = insert none s
[PROOFSTEP]
ext (_ | x)
[GOAL]
case a.none
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ none ∈ ↑insertNone (↑eraseNone s) ↔ none ∈ insert none s
[PROOFSTEP]
simp
[GOAL]
case a.some
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
x : α
⊢ some x ∈ ↑insertNone (↑eraseNone s) ↔ some x ∈ insert none s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
⊢ ↑eraseNone (↑insertNone s) = s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
s : Finset α
a✝ : α
⊢ a✝ ∈ ↑eraseNone (↑insertNone s) ↔ a✝ ∈ s
[PROOFSTEP]
simp