awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.tails.get n = drop n s.tail
s : Stream' α
succ : s.tails.tail.get n = drop (n + 1) s.tail
succ₁ : s.tails.tail.get n = drop n s.tail.tail
succ₂ : (s.tail :: s.tail.tails).tail.get n = drop n s.tail.tail
⊢ s.tails.get (n + 1) = drop (n + 1) s.tail
have succ₃ : s.tail.tails.get n = drop n s.tail.tail
Tactic: rw [get_succ, drop_succ, tails_eq, tail_cons, ih]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.tails.get n = drop n s.tail
s : Stream' α
succ : s.tails.tail.get n = drop (n + 1) s.tail
succ₁ : s.tails.tail.get n = drop n s.tail.tail
succ₂ : (s.tail :: s.tail.tails).tail.get n = drop n s.tail.tail
succ₃ : s.tail.tails.get n = drop n s.tail.tail
⊢ s.tails.get (n + 1) = drop (n + 1) s.tail
have succ₄ : drop n s.tail.tail = drop n s.tail.tail
Tactic: rw [get_succ, drop_succ, tails_eq, tail_cons, ih]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ s.tails.get n = drop n s.tail
have zero : ∀ (s : Stream' α), s.tails.get 0 = drop 0 s.tail
Tactic: induction n generalizing s with
  | zero => rfl
  | succ n ih => rw [get_succ, drop_succ, tails_eq, tail_cons, ih]
Cleared hypotheses: n, s
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s : Stream' α
zero : ∀ (s : Stream' α), s.tails.get 0 = drop 0 s.tail
⊢ s.tails.get n = drop n s.tail
have succ : ∀ (n : ℕ) (ih : ∀ (s : Stream' α), s.tails.get n = drop n s.tail) (s : Stream' α),
  s.tails.get (n + 1) = drop (n + 1) s.tail
Tactic: induction n generalizing s with
  | zero => rfl
  | succ n ih => rw [get_succ, drop_succ, tails_eq, tail_cons, ih]
Cleared hypotheses: n, s
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
l : List α
s : Stream' α
⊢ corec
      (fun (x : List α × Stream' α) ↦
        match (motive := List α × Stream' α → List α) x with
        | (a, snd) => a)
      (fun (p : List α × Stream' α) ↦
        match (motive := List α × Stream' α → List α × Stream' α) p with
        | (l', s') => (l' ++ [s'.head], s'.tail))
      (l, s) =
    l ::
      corec
        (fun (x : List α × Stream' α) ↦
          match (motive := List α × Stream' α → List α) x with
          | (a, snd) => a)
        (fun (p : List α × Stream' α) ↦
          match (motive := List α × Stream' α → List α × Stream' α) p with
          | (l', s') => (l' ++ [s'.head], s'.tail))
        (l ++ [s.head], s.tail)
have rw : (match (motive := List α × Stream' α → List α) (l, s) with
    | (a, snd) => a) ::
    corec (α := List α × Stream' α)
      (fun (x : List α × Stream' α) ↦
        (match (motive := List α × Stream' α → List α) x with
          | (a, snd) => a :
          List α))
      (fun (p : List α × Stream' α) ↦
        (match (motive := List α × Stream' α → List α × Stream' α) p with
          | (l', s') => (l' ++ [s'.head], s'.tail) :
          List α × Stream' α))
      (match (motive := List α × Stream' α → List α × Stream' α) (l, s) with
        | (l', s') => (l' ++ [s'.head], s'.tail) :
        List α × Stream' α) =
  l ::
    corec
      (fun (x : List α × Stream' α) ↦
        match (motive := List α × Stream' α → List α) x with
        | (a, snd) => a)
      (fun (p : List α × Stream' α) ↦
        match (motive := List α × Stream' α → List α × Stream' α) p with
        | (l', s') => (l' ++ [s'.head], s'.tail))
      (l ++ [s.head], s.tail)
Tactic: rw [corec_eq]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
⊢ (initsCore [s.head] s.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail
have rw : ([s.head] :: initsCore ([s.head] ++ [s.tail.head]) s.tail.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail
Tactic: rw [inits_core_eq]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
⊢ a :: (initsCore l s).get (n + 1) = (initsCore (a :: l) s).get (n + 1)
have succ : (initsCore (a :: (l ++ [s.head])) s.tail).get n = ((a :: l) :: initsCore (a :: l ++ [s.head]) s.tail).get (n + 1)
Tactic: rw [get_succ, inits_core_eq, tail_cons, ih, inits_core_eq (a :: l) s]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
n : ℕ
l : List α
s : Stream' α
⊢ a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
have zero : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get 0 = (initsCore (a :: l) s).get 0
Tactic: induction n generalizing l s with
  | zero => rfl
  | succ n ih =>
    rw [get_succ, inits_core_eq, tail_cons, ih, inits_core_eq (a :: l) s]
    rfl
Cleared hypotheses: n, l, s
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
n : ℕ
l : List α
s : Stream' α
zero : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get 0 = (initsCore (a :: l) s).get 0
⊢ a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
have succ : ∀ (n : ℕ) (ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n) (l : List α)
  (s : Stream' α), a :: (initsCore l s).get (n + 1) = (initsCore (a :: l) s).get (n + 1)
Tactic: induction n generalizing l s with
  | zero => rfl
  | succ n ih =>
    rw [get_succ, inits_core_eq, tail_cons, ih, inits_core_eq (a :: l) s]
    rfl
Cleared hypotheses: n, l, s
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.inits.get n = take n.succ s
s : Stream' α
⊢ s.inits.get (n + 1) = take (n + 1).succ s
have succ : s.inits.tail.get n = take (n + 1).succ s
Tactic: rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.inits.get n = take n.succ s
s : Stream' α
succ : s.inits.tail.get n = take (n + 1).succ s
⊢ s.inits.get (n + 1) = take (n + 1).succ s
have succ₁ : s.inits.tail.get n = s.head :: take (n + 1) s.tail
Tactic: rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.inits.get n = take n.succ s
s : Stream' α
succ : s.inits.tail.get n = take (n + 1).succ s
succ₁ : s.inits.tail.get n = s.head :: take (n + 1) s.tail
⊢ s.inits.get (n + 1) = take (n + 1).succ s
have succ₂ : s.inits.tail.get n = s.head :: s.tail.inits.get n
Tactic: rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.inits.get n = take n.succ s
s : Stream' α
succ : s.inits.tail.get n = take (n + 1).succ s
succ₁ : s.inits.tail.get n = s.head :: take (n + 1) s.tail
succ₂ : s.inits.tail.get n = s.head :: s.tail.inits.get n
⊢ s.inits.get (n + 1) = take (n + 1).succ s
have succ₃ : (initsCore [s.head, s.tail.head] s.tail.tail).get n = s.head :: s.tail.inits.get n
Tactic: rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.inits.get n = take n.succ s
s : Stream' α
succ : s.inits.tail.get n = take (n + 1).succ s
succ₁ : s.inits.tail.get n = s.head :: take (n + 1) s.tail
succ₂ : s.inits.tail.get n = s.head :: s.tail.inits.get n
succ₃ : (initsCore [s.head, s.tail.head] s.tail.tail).get n = s.head :: s.tail.inits.get n
⊢ s.inits.get (n + 1) = take (n + 1).succ s
have succ₄ : (initsCore [s.head, s.tail.head] s.tail.tail).get n = s.head :: (initsCore [s.tail.head] s.tail.tail).get n
Tactic: rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.inits.get n = take n.succ s
s : Stream' α
succ : s.inits.tail.get n = take (n + 1).succ s
succ₁ : s.inits.tail.get n = s.head :: take (n + 1) s.tail
succ₂ : s.inits.tail.get n = s.head :: s.tail.inits.get n
succ₃ : (initsCore [s.head, s.tail.head] s.tail.tail).get n = s.head :: s.tail.inits.get n
succ₄ : (initsCore [s.head, s.tail.head] s.tail.tail).get n = s.head :: (initsCore [s.tail.head] s.tail.tail).get n
⊢ s.inits.get (n + 1) = take (n + 1).succ s
have succ₅ : (initsCore [s.head, s.tail.head] s.tail.tail).get n = (initsCore [s.head, s.tail.head] s.tail.tail).get n
Tactic: rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s : Stream' α
⊢ s.inits.get n = take n.succ s
have zero : ∀ (s : Stream' α), s.inits.get 0 = take (succ 0) s
Tactic: induction n generalizing s with
  | zero => rfl
  | succ n ih => rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core]
Cleared hypotheses: n, s
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n : ℕ
s : Stream' α
zero : ∀ (s : Stream' α), s.inits.get 0 = take (succ 0) s
⊢ s.inits.get n = take n.succ s
have succ : ∀ (n : ℕ) (ih : ∀ (s : Stream' α), s.inits.get n = take n.succ s) (s : Stream' α),
  s.inits.get (n + 1) = take (n + 1).succ s
Tactic: induction n generalizing s with
  | zero => rfl
  | succ n ih => rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core]
Cleared hypotheses: n, s
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
⊢ s.inits = [s.head] :: map (List.cons s.head) s.tail.inits
have a : ∀ (n : ℕ), s.inits.get n = ([s.head] :: map (List.cons s.head) s.tail.inits).get n
Tactic: apply Stream'.ext
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
n : ℕ
⊢ s.inits.get n = ([s.head] :: map (List.cons s.head) s.tail.inits).get n
have a : s.inits.get 0 = ([s.head] :: map (List.cons s.head) s.tail.inits).get 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
n : ℕ
a : s.inits.get 0 = ([s.head] :: map (List.cons s.head) s.tail.inits).get 0
⊢ s.inits.get n = ([s.head] :: map (List.cons s.head) s.tail.inits).get n
have a₁ : ∀ (n : ℕ), s.inits.get (n + 1) = ([s.head] :: map (List.cons s.head) s.tail.inits).get (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
n : ℕ
⊢ s.inits.get (n + 1) = ([s.head] :: map (List.cons s.head) s.tail.inits).get (n + 1)
have a : take (n + 1).succ s = s.head :: take n.succ s.tail
Tactic: rw [get_inits, get_succ, tail_cons, get_map, get_inits]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
⊢ zip appendStream' s.inits s.tails = const s
have a : ∀ (n n_1 : ℕ), ((zip appendStream' s.inits s.tails).get n).get n_1 = ((const s).get n).get n_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
⊢ nats = 0 :: map succ nats
have a : ∀ (n : ℕ), nats.get n = (0 :: map succ nats).get n
Tactic: apply Stream'.ext
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
n : ℕ
⊢ nats.get n = (0 :: map succ nats).get n
have a : nats.get 0 = (0 :: map succ nats).get 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
n : ℕ
a : nats.get 0 = (0 :: map succ nats).get 0
⊢ nats.get n = (0 :: map succ nats).get n
have a₁ : ∀ (n : ℕ), nats.get (n + 1) = (0 :: map succ nats).get (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next
have case1 : ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
    { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next =
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
    { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c }
Tactic: rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_pos, ← ih]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next
case1 :
  ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next =
    ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c }
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next
have case1₁ : { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
  { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr
Tactic: rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_pos, ← ih]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next =
    ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c }
have case1 : ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c + Pos.Raw.get s₁.s s₁.i : Legacy.Iterator }
    { s := ofList (c :: s₂.s.toList), i := s₂.i + c + Pos.Raw.get s₂.s s₂.i : Legacy.Iterator } =
  ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + Pos.Raw.get s₁.s s₁.i + c }
    { s := ofList (c :: s₂.s.toList), i := s₂.i + Pos.Raw.get s₂.s s₂.i + c }
Tactic: simp only [Legacy.Iterator.next, Pos.Raw.next, get_cons_addChar, ofList_toList]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c + Pos.Raw.get s₁.s s₁.i : Legacy.Iterator }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c + Pos.Raw.get s₂.s s₂.i : Legacy.Iterator } =
    ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + Pos.Raw.get s₁.s s₁.i + c }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + Pos.Raw.get s₂.s s₂.i + c }
have case1 : s₁.i + c + Pos.Raw.get s₁.s s₁.i = s₁.i + Pos.Raw.get s₁.s s₁.i + c
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c : Legacy.Iterator } =
    ltb s₁.next s₂.next
case1 : s₁.i + c + Pos.Raw.get s₁.s s₁.i = s₁.i + Pos.Raw.get s₁.s s₁.i + c
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c + Pos.Raw.get s₁.s s₁.i : Legacy.Iterator }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c + Pos.Raw.get s₂.s s₂.i : Legacy.Iterator } =
    ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + Pos.Raw.get s₁.s s₁.i + c }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + Pos.Raw.get s₂.s s₂.i + c }
have case1₁ : s₂.i + c + Pos.Raw.get s₂.s s₂.i = s₂.i + Pos.Raw.get s₂.s s₂.i + c
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator } =
    decide (s₁.curr < s₂.curr)
have case2 : decide
    ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr <
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr) =
  decide (s₁.curr < s₂.curr)
Tactic: rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_neg]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
case2 :
  decide
      ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr <
        { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr) =
    decide (s₁.curr < s₂.curr)
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator } =
    decide (s₁.curr < s₂.curr)
have case2₁ : ¬{ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
    { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr
Tactic: rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_neg]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator } =
    true
have case3 : (if { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.hasNext = true then
    if { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.hasNext = true then
      if
          { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr then
        ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
          { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next
      else
        decide
          ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr <
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr)
    else true
  else false) =
  true
Tactic: rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_neg (by simpa using h₂)]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
case3 :
  (if { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr)
      else true
    else false) =
    true
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator } =
    true
have case3₁ : (if { s := ofList s₂.s.toList, i := s₂.i : Legacy.Iterator }.hasNext = true then
    if { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.hasNext = true then
      if
          { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr then
        ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
          { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next
      else
        decide
          ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr <
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr)
    else true
  else false) =
  true
Tactic: rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_neg (by simpa using h₂)]
-- Lean 4 proof step from Mathlib.Data.String.Basic (goal)
Goal:
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : ¬s₁.hasNext = true
case3 :
  (if { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr)
      else true
    else false) =
    true
case3₁ :
  (if { s := ofList s₂.s.toList, i := s₂.i : Legacy.Iterator }.hasNext = true then
      if { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.hasNext = true then
        if
            { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr then
          ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next
        else
          decide
            ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr <
              { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr)
      else true
    else false) =
    true
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator } =
    true
have case3₂ : (if { s := ofList s₂.s.toList, i := s₂.i : Legacy.Iterator }.hasNext = true then
    if { s := ofList s₁.s.toList, i := s₁.i : Legacy.Iterator }.hasNext = true then
      if
          { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr =
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr then
        ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.next
          { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.next
      else
        decide
          ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c : Legacy.Iterator }.curr <
            { s := ofList (c :: s₂.s.toList), i := s₂.i + c : Legacy.Iterator }.curr)
    else true
  else false) =
  true
Tactic: rw [ltb, Legacy.Iterator.hasNext_cons_addChar, Legacy.Iterator.hasNext_cons_addChar,
      if_pos (by simpa using h₁), if_neg (by simpa using h₂)]