awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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'
⊢ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al =
    cons a (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al))
have some : (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) : Stream' (Option α)) =
  (↑(cons a (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al))) : Stream' (Option α))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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'
⊢ (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) : Stream' (Option α)) =
    (↑(cons a (tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al))) : Stream' (Option α))
have some : f = some a :: f.tail
Tactic: dsimp [tail, cons]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (hypothesis)
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 = some a :: f.tail
have f0₁ : get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 = some a
Tactic: rw [h1] at f0
Cleared hypotheses: f0, h1, h2
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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 = some a :: f.tail
have some : f = get? (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) f al) 0 :: f.tail
Tactic: rw [← f0]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
a : α
s : Seq α
⊢ (cons a s).head = some a
have rw : Prod.fst <$> (cons a s).destruct = some a
Tactic: rw [head_eq_destruct, destruct_cons, Option.map_eq_map, Option.map_some]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
a : α
s : Seq α
rw : Prod.fst <$> (cons a s).destruct = some a
⊢ (cons a s).head = some a
have rw₁ : Prod.fst <$> some (a, s) = some a
Tactic: rw [head_eq_destruct, destruct_cons, Option.map_eq_map, Option.map_some]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
a : α
s : Seq α
rw : Prod.fst <$> (cons a s).destruct = some a
rw₁ : Prod.fst <$> some (a, s) = some a
⊢ (cons a s).head = some a
have rw₂ : Option.map Prod.fst (some (a, s)) = some a
Tactic: rw [head_eq_destruct, destruct_cons, Option.map_eq_map, Option.map_some]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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
⊢ (cons a s).head = some a
have rw₃ : some (a, s).fst = some a
Tactic: rw [head_eq_destruct, destruct_cons, Option.map_eq_map, Option.map_some]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
x : α
h : s.head = some x
⊢ s = cons x s.tail
have h₁ : ∀ (n : ℕ), s.get? n = (cons x s.tail).get? n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
x : α
h : s.head = some x
n : ℕ
⊢ s.get? n = (cons x s.tail).get? n
have h₁ : s.get? 0 = (cons x s.tail).get? 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
x : α
h : s.head = some x
n : ℕ
h₁ : s.get? 0 = (cons x s.tail).get? 0
⊢ s.get? n = (cons x s.tail).get? n
have h₂ : ∀ (n : ℕ), s.get? (n + 1) = (cons x s.tail).get? (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
⊢ s.head = none ↔ s = nil
have mp : s.head = none → s = nil
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
s : Seq α
mp : s.head = none → s = nil
⊢ s.head = none ↔ s = nil
have mpr : s = nil → s.head = none
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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)
⊢ motive s
have none : (H : s.destruct = none) → motive s
Tactic: rcases H : destruct s with - | v
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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
⊢ motive s
have some : (v : Seq1 α) → (H : s.destruct = some v) → motive s
Tactic: rcases H : destruct s with - | v
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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 = some v
⊢ motive s
have some : (a : α) → (s' : Seq α) → (H : s.destruct = some (a, s')) → motive s
Tactic: obtain ⟨a, s'⟩ := v
Cleared hypotheses: v, H
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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 s
have some : motive (Seq.cons a s')
Tactic: rw [destruct_eq_cons H]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
⊢ Seq α
have refine : ∀ {n : ℕ} (h : corec' (Corec.f f) (some b) n = none), corec' (Corec.f f) (some b) (n + 1) = none
Tactic: refine ⟨Stream'.corec' (Corec.f f) (some b), fun {n} h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
h : corec' (Corec.f f) (some b) n = none
⊢ corec' (Corec.f f) (some b) (n + 1) = none
have rw : ((Corec.f f (some b)).fst :: corec' (Corec.f f) (Corec.f f (some b)).snd) (n + 1) = none
Tactic: rw [Stream'.corec'_eq]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
h : corec' (Corec.f f) (some b) n = none
⊢ corec' (Corec.f f) (Corec.f f (some b)).snd n = none
have revert : ∀ (h : corec' (Corec.f f) (some b) n = none), corec' (Corec.f f) (Corec.f f (some b)).snd n = none
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
⊢ ∀ (h : corec' (Corec.f f) (some b) n = none), corec' (Corec.f f) (Corec.f f (some b)).snd n = none
have generalize : ∀ (o : Option β) (h : corec' (Corec.f f) o n = none), corec' (Corec.f f) (Corec.f f o).snd n = none
Tactic: generalize some b = o
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
o : Option β
⊢ ∀ (h : corec' (Corec.f f) o 0 = none), corec' (Corec.f f) (Corec.f f o).snd 0 = none
have zero : (Corec.f f o).fst = none → (Corec.f f (Corec.f f o).snd).fst = none
Tactic: change (Corec.f f o).1 = none → (Corec.f f (Corec.f f o).2).1 = none
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
o : Option β
⊢ (Corec.f f o).fst = none → (Corec.f f (Corec.f f o).snd).fst = none
have zero : (Corec.f f none).fst = none → (Corec.f f (Corec.f f none).snd).fst = none
Tactic: rcases o with - | b
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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
⊢ (Corec.f f o).fst = none → (Corec.f f (Corec.f f o).snd).fst = none
have zero₁ : ∀ (b : β), (Corec.f f (some b)).fst = none → (Corec.f f (Corec.f f (some b)).snd).fst = none
Tactic: rcases o with - | b
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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
⊢ (Corec.f f (Corec.f f (some b)).snd).fst = none
have 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
Tactic: dsimp [Corec.f]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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
⊢ 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
have 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
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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),
    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
have 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
Tactic: rcases h₁ : f b with - | s
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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
⊢ ∀
    (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
have 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
Tactic: rcases h₁ : f b with - | s
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨a, b'⟩ := s
Cleared hypotheses: s, h₁, h
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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' (Corec.f f) o (n + 1) = none), corec' (Corec.f f) (Corec.f f o).snd (n + 1) = none
have 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
Tactic: rw [Stream'.corec'_eq (Corec.f f) (Corec.f f o).2, Stream'.corec'_eq (Corec.f f) o]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
o : Option β
⊢ ∀ (h : corec' (Corec.f f) o n = none), corec' (Corec.f f) (Corec.f f o).snd n = none
have zero : ∀ (o : Option β) (h : corec' (Corec.f f) o 0 = none), corec' (Corec.f f) (Corec.f f o).snd 0 = 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
Cleared hypotheses: n, o
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
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
⊢ ∀ (h : corec' (Corec.f f) o n = none), corec' (Corec.f f) (Corec.f f o).snd n = none
have 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
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
Cleared hypotheses: n, o
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
⊢ (corec f b).destruct = omap (corec f) (f b)
have 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)) sorry)))
    (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)) sorry))
Tactic: dsimp [corec, destruct, get]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
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)) ⋯))
have 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)) sorry)))
    (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)) sorry))
Tactic: dsimp [Corec.f]
-- Lean 4 proof step from Mathlib.Data.Seq.Defs (goal)
Goal:
α : Type u
β : Type v
f : β → Option (α × β)
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) (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)) ⋯))
have none : ∀ (h : f b = 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) (some b)) sorry)))
      (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'))))
    (match (motive := Option (α × β) → Option (α × Seq α)) none with
    | none => none
    | some (a, b) => some (a, Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) (corec' (Corec.f f) (some b)) sorry))
Tactic: rcases h : f b with - | s