awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 = some a
h1 : a' = a
h2 : tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) = s'
⊢ f = get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 :: f.tail

Tactic:
(Stream'.eta f).symm

Premises used: Stream'.get, Stream'.eta, Eq.symm, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 = some a
h1 : a' = a
h2 : tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) = s'
⊢ f = get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 :: f.tail

Tactic:
exact (Stream'.eta f).symm

Premises used: Stream'.eta, Eq.symm
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Option α) (head nil) none

Tactic:
rfl

Premises used: Stream'.Seq.head, Stream'.const, rfl, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a : α
s : Seq α
rw : Prod.fst <$> (cons a s).destruct = some a
rw₁ : Prod.fst <$> some (a, s) = some a
rw₂ : Option.map Prod.fst (some (a, s)) = some a
rw₃ rw₄ : some (a, s).fst = some a
⊢ (cons a s).head = some a

Tactic:
rw [head_eq_destruct, destruct_cons, Option.map_eq_map, Option.map_some]

Premises used: Option.map_some, Stream'.Seq.destruct_cons, Stream'.Seq.head_eq_destruct, Option.map_eq_map
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Seq α) (tail nil) nil

Tactic:
rfl

Premises used: Stream'.Seq.nil, Stream'.Seq.tail, Stream'.get, Stream'.const, Stream'.tail, rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a : α
s : Seq α
⊢ (cons a s).tail = s

Tactic:
rfl

Premises used: Stream'.Seq, Stream'.Seq.tail, Stream'.get, Stream'.cons, Stream'.tail, rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
x : α
h : s.head = some x
h₁ : ∀ (n : ℕ), s.get? n = (cons x s.tail).get? n
⊢ s = cons x s.tail

Tactic:
ext1 n
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
x : α
h : s.head = some x
n : ℕ
h₁ : s.get? 0 = (cons x s.tail).get? 0
h₂ : ∀ (n : ℕ), s.get? (n + 1) = (cons x s.tail).get? (n + 1)
⊢ s.get? n = (cons x s.tail).get? n

Tactic:
cases n
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
x : α
h : s.head = some x
n : ℕ
⊢ s.get? (n + 1) = (cons x s.tail).get? (n + 1)

Tactic:
simp only [get?_cons_zero, get?_cons_succ, get?_tail]

Premises used: Stream'.Seq.get?_tail, Stream'.Seq.get?_cons_zero, Stream'.Seq.get?_cons_succ
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
x : α
h : s.head = some x
⊢ s.get? 0 = some x

Tactic:
h

Premises used: Stream'.Seq.head
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
x : α
h : s.head = some x
⊢ s.get? 0 = some x

Tactic:
exact h
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
h : s.head = none
⊢ s = nil

Tactic:
get?_zero_eq_none.mp h

Premises used: Stream'.Seq.get?_zero_eq_none, Iff.mp
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
mp : s.head = none → s = nil
mpr : s = nil → s.head = none
⊢ s.head = none ↔ s = nil

Tactic:
constructor
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
⊢ s.head = none → s = nil

Tactic:
apply head_eq_none

Premises used: Stream'.Seq.head_eq_none
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
h : s = nil
⊢ s.head = none

Tactic:
simp [h]
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
none : (H : s.destruct = Option.none) → motive s
some : (v : Seq1 α) → (H : s.destruct = Option.some v) → motive s
⊢ motive s

Tactic:
rcases H : destruct s with - | v

Premises used: Stream'.Seq.destruct
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
H : s.destruct = Option.none
none : motive Seq.nil
⊢ motive s

Tactic:
rw [destruct_eq_none H]

Premises used: Stream'.Seq.destruct_eq_none
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
H : s.destruct = none
⊢ motive Seq.nil

Tactic:
apply nil
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
v : Seq1 α
H : s.destruct = Option.some v
some : (a : α) → (s' : Seq α) → (H : s.destruct = Option.some (a, s')) → motive s
⊢ motive s

Tactic:
obtain ⟨a, s'⟩ := v
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
a : α
s' : Seq α
H : s.destruct = Option.some (a, s')
some : motive (Seq.cons a s')
⊢ motive s

Tactic:
rw [destruct_eq_cons H]

Premises used: Stream'.Seq.destruct_eq_cons
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
a : α
s' : Seq α
H : s.destruct = some (a, s')
⊢ motive (Seq.cons a s')

Tactic:
apply cons
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
refine : ∀ {n : ℕ} (h : corec' (Corec.f f) (some b) n = none), corec' (Corec.f f) (some b) (n + 1) = none
⊢ Seq α

Tactic:
refine ⟨Stream'.corec' (Corec.f f) (some b), fun {n} h => ?_⟩
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
h : corec' (Corec.f f) (some b) n = none
rw : ((Corec.f f (some b)).fst :: corec' (Corec.f f) (Corec.f f (some b)).snd) (n + 1) = none
⊢ corec' (Corec.f f) (some b) (n + 1) = none

Tactic:
rw [Stream'.corec'_eq]

Premises used: Stream'.corec'_eq
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
h : corec' (Corec.f f) (some b) n = none
revert : ∀ (h : corec' (Corec.f f) (some b) n = none), corec' (Corec.f f) (Corec.f f (some b)).snd n = none
⊢ corec' (Corec.f f) (Corec.f f (some b)).snd n = none

Tactic:
revert h
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
generalize : ∀ (o : Option β) (h : corec' (Corec.f f) o n = none), corec' (Corec.f f) (Corec.f f o).snd n = none
⊢ ∀ (h : corec' (Corec.f f) (some b) n = none), corec' (Corec.f f) (Corec.f f (some b)).snd n = none

Tactic:
generalize some b = o

Premises used: Option.some
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
o : Option β
zero : (Corec.f f o).fst = none → (Corec.f f (Corec.f f o).snd).fst = none
⊢ ∀ (h : corec' (Corec.f f) o 0 = none), corec' (Corec.f f) (Corec.f f o).snd 0 = none

Tactic:
change (Corec.f f o).1 = none → (Corec.f f (Corec.f f o).2).1 = none
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
o : Option β
zero : (Corec.f f none).fst = none → (Corec.f f (Corec.f f none).snd).fst = none
zero₁ : ∀ (b : β), (Corec.f f (some b)).fst = none → (Corec.f f (Corec.f f (some b)).snd).fst = none
⊢ (Corec.f f o).fst = none → (Corec.f f (Corec.f f o).snd).fst = none

Tactic:
rcases o with - | b
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h : (Corec.f f none).fst = none
⊢ (Corec.f f (Corec.f f none).snd).fst = none

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b_1 b : β
h :
  Eq.{u + 1} (α := Option α)
    (Prod.fst.{u, v} (β := Option β)
      (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
      | none => (none, none)
      | some (a, b') => (some a, some b')))
    none
zero :
  Eq.{u + 1} (α := Option α)
    (Prod.fst.{u, v} (β := Option β)
      (match (motive := Option β → Prod.{u, v} (Option α) (Option β))
        Prod.snd.{u, v} (α := Option α)
          (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')) with
      | none => (none, none)
      | some b =>
        match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')))
    none
⊢ (Corec.f f (Corec.f f (some b)).snd).fst = none

Tactic:
dsimp [Corec.f]

Premises used: Stream'.Seq.Corec.f
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b_1 b : β
h :
  Eq.{u + 1} (α := Option α)
    (Prod.fst.{u, v} (β := Option β)
      (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
      | none => (none, none)
      | some (a, b') => (some a, some b')))
    none
zero :
  ∀
    (h :
      Eq.{u + 1} (α := Option α)
        (Prod.fst.{u, v} (β := Option β)
          (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')))
        none),
    Eq.{u + 1} (α := Option α)
      (Prod.fst.{u, v} (β := Option β)
        (match (motive := Option β → Prod.{u, v} (Option α) (Option β))
          Prod.snd.{u, v} (α := Option α)
            (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
            | none => (none, none)
            | some (a, b') => (some a, some b')) with
        | none => (none, none)
        | some b =>
          match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')))
      none
⊢ Eq.{u + 1} (α := Option α)
    (Prod.fst.{u, v} (β := Option β)
      (match (motive := Option β → Prod.{u, v} (Option α) (Option β))
        Prod.snd.{u, v} (α := Option α)
          (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')) with
      | none => (none, none)
      | some b =>
        match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')))
    none

Tactic:
revert h
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b_1 b : β
zero :
  ∀ (h₁ : f b = none)
    (h :
      Eq.{u + 1} (α := Option α)
        (Prod.fst.{u, v} (β := Option β)
          (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) none with
          | none => (none, none)
          | some (a, b') => (some a, some b')))
        none),
    Eq.{u + 1} (α := Option α)
      (Prod.fst.{u, v} (β := Option β)
        (match (motive := Option β → Prod.{u, v} (Option α) (Option β))
          Prod.snd.{u, v} (α := Option α)
            (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) none with
            | none => (none, none)
            | some (a, b') => (some a, some b')) with
        | none => (none, none)
        | some b =>
          match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')))
      none
zero₁ :
  ∀ (s : α × β) (h₁ : f b = some s)
    (h :
      Eq.{u + 1} (α := Option α)
        (Prod.fst.{u, v} (β := Option β)
          (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) some s with
          | none => (none, none)
          | some (a, b') => (some a, some b')))
        none),
    Eq.{u + 1} (α := Option α)
      (Prod.fst.{u, v} (β := Option β)
        (match (motive := Option β → Prod.{u, v} (Option α) (Option β))
          Prod.snd.{u, v} (α := Option α)
            (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) some s with
            | none => (none, none)
            | some (a, b') => (some a, some b')) with
        | none => (none, none)
        | some b =>
          match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')))
      none
⊢ ∀
    (h :
      Eq.{u + 1} (α := Option α)
        (Prod.fst.{u, v} (β := Option β)
          (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')))
        none),
    Eq.{u + 1} (α := Option α)
      (Prod.fst.{u, v} (β := Option β)
        (match (motive := Option β → Prod.{u, v} (Option α) (Option β))
          Prod.snd.{u, v} (α := Option α)
            (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
            | none => (none, none)
            | some (a, b') => (some a, some b')) with
        | none => (none, none)
        | some b =>
          match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')))
      none

Tactic:
rcases h₁ : f b with - | s
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b_1 b : β
h₁ : f b = none
h :
  Eq.{u + 1} (α := Option α)
    (Prod.fst.{u, v} (β := Option β)
      (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) none with
      | none => (none, none)
      | some (a, b') => (some a, some b')))
    none
⊢ Eq.{u + 1} (α := Option α)
    (Prod.fst.{u, v} (β := Option β)
      (match (motive := Option β → Prod.{u, v} (Option α) (Option β))
        Prod.snd.{u, v} (α := Option α)
          (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) none with
          | none => (none, none)
          | some (a, b') => (some a, some b')) with
      | none => (none, none)
      | some b =>
        match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')))
    none

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b_1 b : β
s : α × β
h₁ : f b = some s
h :
  Eq.{u + 1} (α := Option α)
    (Prod.fst.{u, v} (β := Option β)
      (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) some s with
      | none => (none, none)
      | some (a, b') => (some a, some b')))
    none
zero :
  ∀ (a : α) (b' : β) (h₁ : f b = some (a, b'))
    (h :
      Eq.{u + 1} (α := Option α)
        (Prod.fst.{u, v} (β := Option β)
          (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) some (a, b') with
          | none => (none, none)
          | some (a, b') => (some a, some b')))
        none),
    Eq.{u + 1} (α := Option α)
      (Prod.fst.{u, v} (β := Option β)
        (match (motive := Option β → Prod.{u, v} (Option α) (Option β))
          Prod.snd.{u, v} (α := Option α)
            (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) some (a, b') with
            | none => (none, none)
            | some (a, b') => (some a, some b')) with
        | none => (none, none)
        | some b =>
          match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')))
      none
⊢ Eq.{u + 1} (α := Option α)
    (Prod.fst.{u, v} (β := Option β)
      (match (motive := Option β → Prod.{u, v} (Option α) (Option β))
        Prod.snd.{u, v} (α := Option α)
          (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) some s with
          | none => (none, none)
          | some (a, b') => (some a, some b')) with
      | none => (none, none)
      | some b =>
        match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')))
    none

Tactic:
obtain ⟨a, b'⟩ := s
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b_1 b : β
a : α
b' : β
h₁ : f b = some (a, b')
h :
  Eq.{u + 1} (α := Option α)
    (Prod.fst.{u, v} (β := Option β)
      (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) some (a, b') with
      | none => (none, none)
      | some (a, b') => (some a, some b')))
    none
⊢ Eq.{u + 1} (α := Option α)
    (Prod.fst.{u, v} (β := Option β)
      (match (motive := Option β → Prod.{u, v} (Option α) (Option β))
        Prod.snd.{u, v} (α := Option α)
          (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) some (a, b') with
          | none => (none, none)
          | some (a, b') => (some a, some b')) with
      | none => (none, none)
      | some b =>
        match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')))
    none

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
IH : ∀ (o : Option β) (h : corec' (Corec.f f) o n = none), corec' (Corec.f f) (Corec.f f o).snd n = none
o : Option β
succ :
  ∀ (h : ((Corec.f f o).fst :: corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = none),
    ((Corec.f f (Corec.f f o).snd).fst :: corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd) (n + 1) = none
⊢ ∀ (h : corec' (Corec.f f) o (n + 1) = none), corec' (Corec.f f) (Corec.f f o).snd (n + 1) = none

Tactic:
rw [Stream'.corec'_eq (Corec.f f) (Corec.f f o).2, Stream'.corec'_eq (Corec.f f) o]

Premises used: Stream'.corec'_eq, Stream'.Seq.Corec.f, Prod.snd
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
IH : ∀ (o : Option β) (h : corec' (Corec.f f) o n = none), corec' (Corec.f f) (Corec.f f o).snd n = none
o : Option β
⊢ ∀ (h : ((Corec.f f o).fst :: corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = none),
    ((Corec.f f (Corec.f f o).snd).fst :: corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd) (n + 1) = none

Tactic:
IH (Corec.f f o).2

Premises used: Stream'.corec', Stream'.Seq.Corec.f, Stream'.map, Stream'.corec, Stream'.cons, Prod.snd
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
IH : ∀ (o : Option β) (h : corec' (Corec.f f) o n = none), corec' (Corec.f f) (Corec.f f o).snd n = none
o : Option β
⊢ ∀ (h : ((Corec.f f o).fst :: corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = none),
    ((Corec.f f (Corec.f f o).snd).fst :: corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd) (n + 1) = none

Tactic:
exact IH (Corec.f f o).2

Premises used: Stream'.Seq.Corec.f, Prod.snd
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
o : Option β
zero : ∀ (o : Option β) (h : corec' (Corec.f f) o 0 = none), corec' (Corec.f f) (Corec.f f o).snd 0 = none
succ :
  ∀ (n : ℕ) (IH : ∀ (o : Option β) (h : corec' (Corec.f f) o n = none), corec' (Corec.f f) (Corec.f f o).snd n = none)
    (o : Option β) (h : corec' (Corec.f f) o (n + 1) = none), corec' (Corec.f f) (Corec.f f o).snd (n + 1) = none
⊢ ∀ (h : corec' (Corec.f f) o n = none), corec' (Corec.f f) (Corec.f f o).snd n = none

Tactic:
induction n generalizing o with
  | zero =>
    change (Corec.f f o).1 = none → (Corec.f f (Corec.f f o).2).1 = none
    rcases o with - | b <;> intro h
    · rfl
    dsimp [Corec.f] at h
    dsimp [Corec.f]
    revert h; rcases h₁ : f b with - | s <;> intro h
    · rfl
    · obtain ⟨a, b'⟩ := s
      contradiction
  | succ n IH =>
    rw [Stream'.corec'_eq (Corec.f f) (Corec.f f o).2, Stream'.corec'_eq (Corec.f f) o]
    exact IH (Corec.f f o).2

Premises used: Stream'.corec'_eq, Stream'.Seq.Corec.f, Prod.snd
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
dsimp :
  Eq (α := Option (Seq1 α))
    (Option.map
      (fun (a' : α) ↦
        (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯)))
      (corec' (Corec.f f) (some b) 0))
    (match (motive := Option (α × β) → Option (α × Seq α)) f b with
    | none => none
    | some (a, b) => some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯))
⊢ (corec f b).destruct = omap (corec f) (f b)

Tactic:
dsimp [corec, destruct, get]

Premises used: Stream'.get, Stream'.Seq.corec, Stream'.Seq.destruct
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
dsimp :
  Eq.{u + 1} (α := Option (Seq1 α))
    (Option.map
      (fun (a' : α) ↦
        (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯)))
      (Prod.fst.{u, v} (β := Option β)
        (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
        | none => (none, none)
        | some (a, b') => (some a, some b'))))
    (match (motive := Option (α × β) → Option (α × Seq α)) f b with
    | none => none
    | some (a, b) => some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯))
⊢ Eq (α := Option (Seq1 α))
    (Option.map
      (fun (a' : α) ↦
        (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯)))
      (Corec.f f (some b)).fst)
    (match (motive := Option (α × β) → Option (α × Seq α)) f b with
    | none => none
    | some (a, b) => some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) ⋯))

Tactic:
dsimp [Corec.f]

Premises used: Stream'.Seq.Corec.f
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
none :
  ∀ (h : f b = Option.none),
    Eq.{u + 1} (α := Option (Seq1 α))
      (Option.map
        (fun (a' : α) ↦
          (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b)) ⋯)))
        (Prod.fst.{u, v} (β := Option β)
          (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) Option.none with
          | Option.none => (Option.none, Option.none)
          | Option.some (a, b') => (Option.some a, Option.some b'))))
      (match (motive := Option (α × β) → Option (α × Seq α)) Option.none with
      | Option.none => Option.none
      | Option.some (a, b) =>
        Option.some
          (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b)) ⋯))
some :
  ∀ (s : α × β) (h : f b = Option.some s),
    Eq.{u + 1} (α := Option (Seq1 α))
      (Option.map
        (fun (a' : α) ↦
          (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b)) ⋯)))
        (Prod.fst.{u, v} (β := Option β)
          (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) Option.some s with
          | Option.none => (Option.none, Option.none)
          | Option.some (a, b') => (Option.some a, Option.some b'))))
      (match (motive := Option (α × β) → Option (α × Seq α)) Option.some s with
      | Option.none => Option.none
      | Option.some (a, b) =>
        Option.some
          (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b)) ⋯))
⊢ Eq.{u + 1} (α := Option (Seq1 α))
    (Option.map
      (fun (a' : α) ↦
        (a', tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b)) ⋯)))
      (Prod.fst.{u, v} (β := Option β)
        (match (motive := Option (α × β) → Prod.{u, v} (Option α) (Option β)) f b with
        | Option.none => (Option.none, Option.none)
        | Option.some (a, b') => (Option.some a, Option.some b'))))
    (match (motive := Option (α × β) → Option (α × Seq α)) f b with
    | Option.none => Option.none
    | Option.some (a, b) =>
      Option.some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (Option.some b)) ⋯))

Tactic:
rcases h : f b with - | s