awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
v : Seq1 α
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
⊢ List.length.{u} (α := α)
      (match (motive := Option (Seq1 α) → List α) some v with
      | none => []
      | some (x, r) => x :: take m r) ≤
    m + 1

Tactic:
obtain ⟨x, r⟩ := v
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
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:
simpa using ih
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
succ :
  ∀ (x : Option (Seq1 α)),
    List.length.{u} (α := α)
        (match (motive := Option (Seq1 α) → List α) x with
        | none => []
        | some (x, r) => x :: take m r) ≤
      m + 1
⊢ List.length.{u} (α := α)
      (match (motive := Option (Seq1 α) → List α) s.destruct 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

Premises used: Option.some, Option.none, Stream'.Seq.destruct
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
zero : ∀ {s : Seq α}, (take 0 s).length ≤ 0
succ : ∀ (m : ℕ) (ih : ∀ {s : Seq α}, (take m s).length ≤ m) {s : Seq α}, (take (m + 1) s).length ≤ m + 1
⊢ (take n s).length ≤ n

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

Premises used: Option.some, Stream'.Seq.take, Option.none, Stream'.Seq.destruct
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
hle : ∀ (h : s.Terminates), 0 ≤ s.length h
⊢ (take 0 s).length = 0

Tactic:
simp [take]

Premises used: Stream'.Seq.take
-- Module: Mathlib.Data.Seq.Basic
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
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
⊢ (take (n + 1) s).length = n + 1

Tactic:
rw [take, destruct]

Premises used: Stream'.Seq.take, Stream'.Seq.destruct
-- Module: Mathlib.Data.Seq.Basic
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
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
⊢ 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))
-- Module: Mathlib.Data.Seq.Basic
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
succ : (take n s.tail).length = n
⊢ 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:
simp only [Option.mem_def.1 ha, Option.map_eq_map, Option.map_some, List.length_cons,
        Nat.add_right_cancel_iff]

Premises used: Nat.add_right_cancel_iff, List.length_cons, Option.map_some, Iff.mp, Option.map_eq_map, Option.mem_def
-- Module: Mathlib.Data.Seq.Basic
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
succ : ∀ (h : s.tail.Terminates), n ≤ s.tail.length h
⊢ (take n s.tail).length = n

Tactic:
rw [ih]
-- Module: Mathlib.Data.Seq.Basic
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
succ : ∀ m < n, ¬(↑s : Stream' (Option α)).get (m + 1) = none
⊢ n ≤ s.tail.length h

Tactic:
simp only [length, tail, Nat.le_find_iff, TerminatedAt, get?_mk, Stream'.tail]

Premises used: Stream'.Seq.TerminatedAt, Stream'.Seq.length, Nat.le_find_iff, Stream'.Seq.tail, Stream'.Seq.get?_mk, Stream'.tail
-- Module: Mathlib.Data.Seq.Basic
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
⊢ ∃ (a : α), a ∈ s.get? n

Tactic:
have := lt_length_iff'.1 (fun ht => (Nat.lt_of_succ_le (hle ht)))
-- Module: Mathlib.Data.Seq.Basic
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
⊢ ∃ (a : α), Membership.mem (γ := Option α) none a

Tactic:
rw [le_stable s (Nat.succ_le_of_lt hmn) hs] at this

Premises used: Stream'.Seq.le_stable, Nat.succ_le_of_lt
-- Module: Mathlib.Data.Seq.Basic
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 : α), Membership.mem (γ := Option α) none a
⊢ False

Tactic:
simp at this
-- Module: Mathlib.Data.Seq.Basic
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
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
⊢ (take n s).length = n

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

Premises used: Nat.add_right_cancel_iff, Stream'.Seq.TerminatedAt, List.length_cons, Stream'.Seq.take, Stream'.Seq.length, Nat.le_find_iff, Stream'.Seq.tail, Option.map_some, Stream'.Seq.get?_mk, Stream'.Seq.destruct, Option.map_eq_map, Stream'.tail
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
h : s.Terminates
rw : ∀ (h_1 : s.Terminates), s.length h ≤ s.length h_1
⊢ (s.toList h).length = s.length h

Tactic:
rw [toList, length_take_of_le_length]

Premises used: Stream'.Seq.toList, Stream'.Seq.length_take_of_le_length
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
h h_1 : s.Terminates
⊢ s.length h ≤ s.length h_1

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
h h_1 : s.Terminates
⊢ s.length h ≤ s.length h_1

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
a : ∀ (k : α), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.toList h) n = some k ↔ s.get? n = some k
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.toList h) n = s.get? n

Tactic:
ext k
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
k : α
a : s.get? n = some k → ∀ m ≤ n, ¬s.get? m = none
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.toList h) n = some k ↔ s.get? n = some k

Tactic:
simp only [toList, getElem?_take, Nat.lt_find_iff, length,
    Option.ite_none_right_eq_some, and_iff_right_iff_imp, TerminatedAt]

Premises used: Stream'.Seq.TerminatedAt, Stream'.Seq.toList, Stream'.Seq.length, and_iff_right_iff_imp, Option.ite_none_right_eq_some, Nat.lt_find_iff, Stream'.Seq.getElem?_take
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
h_1 : s.Terminates
n : ℕ
k : α
h : s.get? n = some k
m : ℕ
hmn : m ≤ n
a : ∀ (a : α) (ha : s.get? m = some a), ¬s.get? m = none
⊢ ¬s.get? m = none

Tactic:
let ⟨a, ha⟩ := ge_stable s hmn h
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
h_1 : s.Terminates
n : ℕ
k : α
h : s.get? n = some k
m : ℕ
hmn : m ≤ n
a : α
ha : s.get? m = some a
⊢ ¬s.get? m = none

Tactic:
simp [ha]
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
h : s.Terminates
h₁ : ∀ (n : ℕ) (a : α), (↑(s.toList h) : Seq α).get? n = some a ↔ s.get? n = some a
⊢ (↑(s.toList h) : Seq α) = s

Tactic:
ext n
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
a : α
⊢ (↑(s.toList h) : Seq α).get? n = some a ↔ s.get? n = some a

Tactic:
simp [ofList]

Premises used: Stream'.Seq.ofList
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
l : List α
⊢ (↑((↑l : Seq α).toList ⋯) : Seq α) = (↑l : Seq α)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
h :
  ∀ (i : ℕ) (a : α),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (toList nil ⋯) i = some a ↔
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] i = some a
⊢ Eq.{u + 1} (α := List α) (toList nil ⋯) []

Tactic:
ext
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
i : ℕ
a : α
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (toList nil ⋯) i = some a ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] i = some a

Tactic:
simp [nil, toList, const]

Premises used: Stream'.Seq.toList, Stream'.Seq.nil, Stream'.const
-- Module: Mathlib.Data.Seq.Basic
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)
rw₂ rw₃ : s.get? (s.length h - 1) = s.get? (s.length h - 1)
⊢ (s.toList h).getLast? = s.get? (s.length h - 1)

Tactic:
rw [List.getLast?_eq_getElem?, getElem?_toList, length_toList]

Premises used: Stream'.Seq.length_toList, Stream'.Seq.getElem?_toList, List.getLast?_eq_getElem?
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a : α
s t : Seq α
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)))
⊢ 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))

Tactic:
rw [corec_eq]

Premises used: Stream'.Seq.corec_eq
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a : α
s t : Seq α
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 α))
⊢ 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:
dsimp [append]

Premises used: Stream'.Seq.append
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a : α
s t : Seq α
rw 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 α))
⊢ 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:
rw [destruct_cons]

Premises used: Stream'.Seq.destruct_cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
H :
  ∀ (s : Seq α),
    BisimO (fun (s1 s2 : Seq α) ↦ ∃ (s : Seq α), s1 = append nil s ∧ s2 = s) (append nil s).destruct s.destruct
⊢ append nil s = s

Tactic:
apply coinduction2

Premises used: Stream'.Seq.coinduction2
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s_1 s : Seq α
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
⊢ BisimO (fun (s1 s2 : Seq α) ↦ ∃ (s : Seq α), s1 = append nil s ∧ s2 = s) (append nil s).destruct s.destruct

Tactic:
dsimp [append]

Premises used: Stream'.Seq.append
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s_1 s : Seq α
H :
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop)
    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 α)) destruct (nil, s).1 with
      | none =>
        match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) (nil, s).2.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', (nil, s).2)),
    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
⊢ 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:
rw [corec_eq]

Premises used: Stream'.Seq.corec_eq