awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
m n : ℕ
h_mn : m < n
x : α
h_get : s.get? m = some x
⊢ x ∈ take n s
have zero : ∀ {s : Seq α} {n : ℕ} (h_mn : 0 < n) (h_get : s.get? 0 = some x), x ∈ take n s
Tactic: induction m generalizing n s with
  | zero =>
    obtain ⟨l, hl⟩ := Nat.exists_add_one_eq.mpr h_mn
    rw [← hl, take, head_eq_some h_get]
    simp
  | succ k ih =>
    obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_lt h_mn
    have : ∃ y, s.get? 0 = some y := by
      apply ge_stable _ _ h_get
      simp
    obtain ⟨y, hy⟩ := this
    rw [take, head_eq_some hy]
    simp only [destruct_cons, List.mem_cons]
    right
    apply ih (by lia)
    rwa [get?_tail]
Cleared hypotheses: s, m, n, h_mn, h_get
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
m n : ℕ
h_mn : m < n
x : α
h_get : s.get? m = some x
zero : ∀ {s : Seq α} {n : ℕ} (h_mn : 0 < n) (h_get : s.get? 0 = some x), x ∈ take n s
⊢ x ∈ take n s
have succ : ∀ (k : ℕ) (ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s) {s : Seq α} {n : ℕ}
  (h_mn : k + 1 < n) (h_get : s.get? (k + 1) = some x), x ∈ take n s
Tactic: induction m generalizing n s with
  | zero =>
    obtain ⟨l, hl⟩ := Nat.exists_add_one_eq.mpr h_mn
    rw [← hl, take, head_eq_some h_get]
    simp
  | succ k ih =>
    obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_lt h_mn
    have : ∃ y, s.get? 0 = some y := by
      apply ge_stable _ _ h_get
      simp
    obtain ⟨y, hy⟩ := this
    rw [take, head_eq_some hy]
    simp only [destruct_cons, List.mem_cons]
    right
    apply ih (by lia)
    rwa [get?_tail]
Cleared hypotheses: s, m, n, h_mn, h_get
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
⊢ (take (m + 1) s).length ≤ m + 1
have succ : List.length.{u} (α := α)
    (match (motive := Option (Seq1 α) → List α) s.destruct with
    | none => []
    | some (x, r) => x :: take m r) ≤
  m + 1
Tactic: rw [take]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
v : Seq1 α
⊢ List.length.{u} (α := α)
      (match (motive := Option (Seq1 α) → List α) some v with
      | none => []
      | some (x, r) => x :: take m r) ≤
    m + 1
have succ : ∀ (x : α) (r : Seq α),
  List.length.{u} (α := α)
      (match (motive := Option (Seq1 α) → List α) some (x, r) with
      | none => []
      | some (x, r) => x :: take m r) ≤
    m + 1
Tactic: obtain ⟨x, r⟩ := v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
⊢ List.length.{u} (α := α)
      (match (motive := Option (Seq1 α) → List α) s.destruct with
      | none => []
      | some (x, r) => x :: take m r) ≤
    m + 1
have succ : ∀ (x : Option (Seq1 α)),
  List.length.{u} (α := α)
      (match (motive := Option (Seq1 α) → List α) x with
      | none => []
      | some (x, r) => x :: take m r) ≤
    m + 1
Tactic: cases s.destruct with
    | none => simp
    | some v =>
      obtain ⟨x, r⟩ := v
      simpa using ih
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ (take n s).length ≤ n
have zero : ∀ {s : Seq α}, (take 0 s).length ≤ 0
Tactic: induction n generalizing s with
  | zero => simp
  | succ m ih =>
    rw [take]
    cases s.destruct with
    | none => simp
    | some v =>
      obtain ⟨x, r⟩ := v
      simpa using ih
Cleared hypotheses: s, n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
zero : ∀ {s : Seq α}, (take 0 s).length ≤ 0
⊢ (take n s).length ≤ n
have succ : ∀ (m : ℕ) (ih : ∀ {s : Seq α}, (take m s).length ≤ m) {s : Seq α}, (take (m + 1) s).length ≤ m + 1
Tactic: induction n generalizing s with
  | zero => simp
  | succ m ih =>
    rw [take]
    cases s.destruct with
    | none => simp
    | some v =>
      obtain ⟨x, r⟩ := v
      simpa using ih
Cleared hypotheses: s, n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ {s : Seq α} (hle : ∀ (h : s.Terminates), n ≤ s.length h), (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
⊢ (take (n + 1) s).length = n + 1
have succ : List.length.{u} (α := α)
    (match (motive := Option (Seq1 α) → List α) (fun (a' : α) ↦ (a', s.tail)) <$> s.get? 0 with
    | none => []
    | some (x, r) => x :: take n r) =
  n + 1
Tactic: rw [take, destruct]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ {s : Seq α} (hle : ∀ (h : s.Terminates), n ≤ s.length h), (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
⊢ List.length.{u} (α := α)
      (match (motive := Option (Seq1 α) → List α) (fun (a' : α) ↦ (a', s.tail)) <$> s.get? 0 with
      | none => []
      | some (x, r) => x :: take n r) =
    n + 1
have succ : ∀ (a : α) (ha : a ∈ s.get? 0),
  List.length.{u} (α := α)
      (match (motive := Option (Seq1 α) → List α) (fun (a' : α) ↦ (a', s.tail)) <$> s.get? 0 with
      | none => []
      | some (x, r) => x :: take n r) =
    n + 1
Tactic: let ⟨a, ha⟩ := lt_length_iff'.1 (fun ht => lt_of_lt_of_le (Nat.succ_pos _) (hle ht))
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ {s : Seq α} (hle : ∀ (h : s.Terminates), n ≤ s.length h), (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
⊢ List.length.{u} (α := α)
      (match (motive := Option (Seq1 α) → List α) (fun (a' : α) ↦ (a', s.tail)) <$> s.get? 0 with
      | none => []
      | some (x, r) => x :: take n r) =
    n + 1
have succ : (take n s.tail).length = n
Tactic: simp only [Option.mem_def.1 ha, Option.map_eq_map, Option.map_some, List.length_cons,
        Nat.add_right_cancel_iff]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ {s : Seq α} (hle : ∀ (h : s.Terminates), n ≤ s.length h), (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
⊢ (take n s.tail).length = n
have succ : ∀ (h : s.tail.Terminates), n ≤ s.tail.length h
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
ih : ∀ {s : Seq α} (hle : ∀ (h : s.Terminates), n ≤ s.length h), (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
h : s.tail.Terminates
⊢ n ≤ s.tail.length h
have succ : ∀ m < n, ¬(↑s : Stream' (Option α)).get (m + 1) = none
Tactic: simp only [length, tail, Nat.le_find_iff, TerminatedAt, get?_mk, Stream'.tail]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
Goal:
α : Type u
n : ℕ
ih : ∀ {s : Seq α} (hle : ∀ (h : s.Terminates), n ≤ s.length h), (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
h : s.tail.Terminates
m : ℕ
hmn : m < n
hs : (↑s : Stream' (Option α)).get (m + 1) = none
⊢ False
have this : ∃ (a : α), a ∈ s.get? n
Tactic: have := lt_length_iff'.1 (fun ht => (Nat.lt_of_succ_le (hle ht)))
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
Goal:
α : Type u
n : ℕ
ih : ∀ {s : Seq α} (hle : ∀ (h : s.Terminates), n ≤ s.length h), (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
h : s.tail.Terminates
m : ℕ
hmn : m < n
hs : (↑s : Stream' (Option α)).get (m + 1) = none
this : ∃ (a : α), a ∈ s.get? n
⊢ False
have this₁ : ∃ (a : α), Membership.mem (γ := Option α) none a
Tactic: rw [le_stable s (Nat.succ_le_of_lt hmn) hs] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
hle : ∀ (h : s.Terminates), n ≤ s.length h
⊢ (take n s).length = n
have zero : ∀ {s : Seq α} (hle : ∀ (h : s.Terminates), 0 ≤ s.length h), (take 0 s).length = 0
Tactic: induction n generalizing s with
  | zero => simp [take]
  | succ n ih =>
      rw [take, destruct]
      let ⟨a, ha⟩ := lt_length_iff'.1 (fun ht => lt_of_lt_of_le (Nat.succ_pos _) (hle ht))
      simp only [Option.mem_def.1 ha, Option.map_eq_map, Option.map_some, List.length_cons,
        Nat.add_right_cancel_iff]
      rw [ih]
      intro h
      simp only [length, tail, Nat.le_find_iff, TerminatedAt, get?_mk, Stream'.tail]
      intro m hmn hs
      have := lt_length_iff'.1 (fun ht => (Nat.lt_of_succ_le (hle ht)))
      rw [le_stable s (Nat.succ_le_of_lt hmn) hs] at this
      simp at this
Cleared hypotheses: s, n, hle
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
hle : ∀ (h : s.Terminates), n ≤ s.length h
zero : ∀ {s : Seq α} (hle : ∀ (h : s.Terminates), 0 ≤ s.length h), (take 0 s).length = 0
⊢ (take n s).length = n
have succ : ∀ (n : ℕ) (ih : ∀ {s : Seq α} (hle : ∀ (h : s.Terminates), n ≤ s.length h), (take n s).length = n) {s : Seq α}
  (hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h), (take (n + 1) s).length = n + 1
Tactic: induction n generalizing s with
  | zero => simp [take]
  | succ n ih =>
      rw [take, destruct]
      let ⟨a, ha⟩ := lt_length_iff'.1 (fun ht => lt_of_lt_of_le (Nat.succ_pos _) (hle ht))
      simp only [Option.mem_def.1 ha, Option.map_eq_map, Option.map_some, List.length_cons,
        Nat.add_right_cancel_iff]
      rw [ih]
      intro h
      simp only [length, tail, Nat.le_find_iff, TerminatedAt, get?_mk, Stream'.tail]
      intro m hmn hs
      have := lt_length_iff'.1 (fun ht => (Nat.lt_of_succ_le (hle ht)))
      rw [le_stable s (Nat.succ_le_of_lt hmn) hs] at this
      simp at this
Cleared hypotheses: s, n, hle
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
h : s.Terminates
⊢ (s.toList h).length = s.length h
have rw : ∀ (h_1 : s.Terminates), s.length h ≤ s.length h_1
Tactic: rw [toList, length_take_of_le_length]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.toList h) n = s.get? n
have a : ∀ (k : α), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.toList h) n = some k ↔ s.get? n = some k
Tactic: ext k
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
k : α
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.toList h) n = some k ↔ s.get? n = some k
have a : s.get? n = some k → ∀ m ≤ n, ¬s.get? m = none
Tactic: simp only [toList, getElem?_take, Nat.lt_find_iff, length,
    Option.ite_none_right_eq_some, and_iff_right_iff_imp, TerminatedAt]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
h_1 : s.Terminates
n : ℕ
k : α
h : s.get? n = some k
m : ℕ
hmn : m ≤ n
⊢ ¬s.get? m = none
have a : ∀ (a : α) (ha : s.get? m = some a), ¬s.get? m = none
Tactic: let ⟨a, ha⟩ := ge_stable s hmn h
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
h : s.Terminates
⊢ (↑(s.toList h) : Seq α) = s
have h₁ : ∀ (n : ℕ) (a : α), (↑(s.toList h) : Seq α).get? n = some a ↔ s.get? n = some a
Tactic: ext n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
⊢ Eq.{u + 1} (α := List α) (toList nil ⋯) []
have h : ∀ (i : ℕ) (a : α),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (toList nil sorry) i = some a ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] i = some a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
h : s.Terminates
⊢ (s.toList h).getLast? = s.get? (s.length h - 1)
have rw : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.toList h) ((s.toList h).length - 1) =
  s.get? (s.length h - 1)
Tactic: rw [List.getLast?_eq_getElem?, getElem?_toList, length_toList]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
h : s.Terminates
rw :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.toList h) ((s.toList h).length - 1) =
    s.get? (s.length h - 1)
⊢ (s.toList h).getLast? = s.get? (s.length h - 1)
have rw₁ : s.get? ((s.toList h).length - 1) = s.get? (s.length h - 1)
Tactic: rw [List.getLast?_eq_getElem?, getElem?_toList, length_toList]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
h : s.Terminates
rw :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.toList h) ((s.toList h).length - 1) =
    s.get? (s.length h - 1)
rw₁ : s.get? ((s.toList h).length - 1) = s.get? (s.length h - 1)
⊢ (s.toList h).getLast? = s.get? (s.length h - 1)
have rw₂ : s.get? (s.length h - 1) = s.get? (s.length h - 1)
Tactic: rw [List.getLast?_eq_getElem?, getElem?_toList, length_toList]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
a : α
s t : Seq α
⊢ destruct
      (corec
        (fun (x : Seq α × Seq α) ↦
          match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
          | none =>
            match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.2))
        (cons a s, t)) =
    some
      (a,
        corec
          (fun (x : Seq α × Seq α) ↦
            match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
            | none =>
              match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.2))
          (s, t))
have rw : Eq (α := Option (Seq1 α))
  (omap (β := Seq α × Seq α)
    (corec fun (x : Seq α × Seq α) ↦
      match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
      | none =>
        match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', x.2))
    (match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) (cons a s, t).1.destruct with
    | none =>
      match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) (cons a s, t).2.destruct with
      | none => none
      | some (a, b) => some (a, nil, b)
    | some (a_1, s₁') => some (a_1, s₁', (cons a s, t).2)))
  (some
    (a,
      corec
        (fun (x : Seq α × Seq α) ↦
          match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
          | none =>
            match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.2))
        (s, t)))
Tactic: rw [corec_eq]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
a : α
s t : Seq α
⊢ Eq (α := Option (Seq1 α))
    (omap (β := Seq α × Seq α)
      (corec fun (x : Seq α × Seq α) ↦
        match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
        | none =>
          match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
          | none => none
          | some (a, b) => some (a, nil, b)
        | some (a, s₁') => some (a, s₁', x.2))
      (match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) (cons a s, t).1.destruct with
      | none =>
        match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) (cons a s, t).2.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a_1, s₁') => some (a_1, s₁', (cons a s, t).2)))
    (some
      (a,
        corec
          (fun (x : Seq α × Seq α) ↦
            match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
            | none =>
              match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.2))
          (s, t)))
have dsimp : Eq.{u + 1} (α := Option (Seq1 α))
  (match (motive := Option (α × Seq α × Seq α) → Option (α × Seq α))
      match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) (cons a s).destruct with
      | none =>
        match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) t.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', t) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun (x : Seq α × Seq α) ↦
              match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
              | none =>
                match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b) :
    Option (α × Seq α))
  (some
      (a,
        corec
          (fun (x : Seq α × Seq α) ↦
            match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
            | none =>
              match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.2))
          (s, t)) :
    Option (α × Seq α))
Tactic: dsimp [append]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
a : α
s t : Seq α
⊢ Eq.{u + 1} (α := Option (Seq1 α))
    (match (motive := Option (α × Seq α × Seq α) → Option (α × Seq α))
        match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) (cons a s).destruct with
        | none =>
          match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) t.destruct with
          | none => none
          | some (a, b) => some (a, nil, b)
        | some (a, s₁') => some (a, s₁', t) with
      | none => none
      | some (a, b) =>
        some
          (a,
            corec
              (fun (x : Seq α × Seq α) ↦
                match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
                | none =>
                  match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              b) :
      Option (α × Seq α))
    (some
        (a,
          corec
            (fun (x : Seq α × Seq α) ↦
              match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
              | none =>
                match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            (s, t)) :
      Option (α × Seq α))
have rw : Eq.{u + 1} (α := Option (Seq1 α))
  (match (motive := Option (α × Seq α × Seq α) → Option (α × Seq α))
      match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) some (a, s) with
      | none =>
        match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) t.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', t) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun (x : Seq α × Seq α) ↦
              match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
              | none =>
                match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b) :
    Option (α × Seq α))
  (some
      (a,
        corec
          (fun (x : Seq α × Seq α) ↦
            match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
            | none =>
              match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.2))
          (s, t)) :
    Option (α × Seq α))
Tactic: rw [destruct_cons]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
⊢ append nil s = s
have H : ∀ (s : Seq α),
  BisimO (fun (s1 s2 : Seq α) ↦ ∃ (s : Seq α), s1 = append nil s ∧ s2 = s) (append nil s).destruct s.destruct
Tactic: apply coinduction2
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s_1 s : Seq α
⊢ BisimO (fun (s1 s2 : Seq α) ↦ ∃ (s : Seq α), s1 = append nil s ∧ s2 = s) (append nil s).destruct s.destruct
have H : match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop)
  destruct
    (corec
      (fun (x : Seq α × Seq α) ↦
        match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
        | none =>
          match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
          | none => none
          | some (a, b) => some (a, nil, b)
        | some (a, s₁') => some (a, s₁', x.2))
      (nil, s)),
  s.destruct with
| none, none => True
| some (a, s), some (a', s') =>
  a = a' ∧
    ∃ (s_2 : Seq α),
      s =
          corec
            (fun (x : Seq α × Seq α) ↦
              match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
              | none =>
                match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            (nil, s_2) ∧
        s' = s_2
| x, x_1 => False
Tactic: dsimp [append]