awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s : Computation α
a val : α
f0 :
  s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = Option.some a → f (n + 1) = Option.some a) 0 =
    Option.some val
h :
  Eq (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α) Option.some val with
      | none => Sum.inr s.tail
      | Option.some a => Sum.inl a :
      α ⊕ Computation α)
    (Sum.inl a : α ⊕ Computation α)
n : ℕ
some :
  s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = Option.some a → x (n + 1) = Option.some a) 0 =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦
      ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = Option.some a → x (n + 1) = Option.some a) 0
⊢ s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = Option.some a → x (n + 1) = Option.some a) n =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦
      ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = Option.some a → x (n + 1) = Option.some a) n
have some₁ : ∀ (n : ℕ)
  (IH :
    s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = Option.some a → x (n + 1) = Option.some a) n =
      (pure a).val (p := fun (x : Stream' (Option α)) ↦
        ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = Option.some a → x (n + 1) = Option.some a) n),
  s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = Option.some a → x (n + 1) = Option.some a)
      (n + 1) =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦
      ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = Option.some a → x (n + 1) = Option.some a) (n + 1)
Tactic: induction n with
    | zero => injection h with h'; rwa [h'] at f0
    | succ n IH => exact s.2 IH
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s s' : Computation α
⊢ s.destruct = Sum.inr s' → s = s'.think
have dsimp : Eq (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α)
        s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 with
      | none => Sum.inr s.tail
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (Sum.inr s' : α ⊕ Computation α) →
  s = s'.think
Tactic: dsimp [destruct]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s s' : Computation α
⊢ Eq (α := α ⊕ Computation α)
      (match (motive := Option α → α ⊕ Computation α)
          s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 with
        | none => Sum.inr s.tail
        | some a => Sum.inl a :
        α ⊕ Computation α)
      (Sum.inr s' : α ⊕ Computation α) →
    s = s'.think
have none : ∀ (f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = none),
  Eq.{u + 1} (α := α ⊕ Computation α)
      (match (motive := Option α → α ⊕ Computation α) none with
        | none => Sum.inr s.tail
        | some a => Sum.inl a :
        α ⊕ Computation α)
      (Sum.inr s' : α ⊕ Computation α) →
    s = s'.think
Tactic: rcases f0 : s.1 0 with - | a'
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s s' : Computation α
none :
  ∀
    (f0 :
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = Option.none),
    Eq.{u + 1} (α := α ⊕ Computation α)
        (match (motive := Option α → α ⊕ Computation α) Option.none with
          | Option.none => Sum.inr s.tail
          | some a => Sum.inl a :
          α ⊕ Computation α)
        (Sum.inr s' : α ⊕ Computation α) →
      s = s'.think
⊢ Eq (α := α ⊕ Computation α)
      (match (motive := Option α → α ⊕ Computation α)
          s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 with
        | Option.none => Sum.inr s.tail
        | some a => Sum.inl a :
        α ⊕ Computation α)
      (Sum.inr s' : α ⊕ Computation α) →
    s = s'.think
have some : ∀ (a' : α)
  (f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = some a'),
  Eq (α := α ⊕ Computation α)
      (match (motive := Option α → α ⊕ Computation α) some a' with
        | Option.none => Sum.inr s.tail
        | some a => Sum.inl a :
        α ⊕ Computation α)
      (Sum.inr s' : α ⊕ Computation α) →
    s = s'.think
Tactic: rcases f0 : s.1 0 with - | a'
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
s s' : Computation α
f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = none
h :
  Eq.{u + 1} (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α) none with
      | none => Sum.inr s.tail
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (Sum.inr s' : α ⊕ Computation α)
⊢ s = s'.think
have h' : s.tail = s'
Tactic: injection h with h'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s s' : Computation α
f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = none
h' : s.tail = s'
⊢ s = s'.think
have none : s = s.tail.think
Tactic: rw [← h']
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s s' : Computation α
f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = none
h' : s.tail = s'
⊢ s = s.tail.think
have none : ∀ (f : Stream' (Option α)) (al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
  (f0 :
    Subtype.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) 0 =
      none)
  (h' :
    tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) =
      s'),
  Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al =
    (tail
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f
          al)).think
Tactic: obtain ⟨f, al⟩ := s
Cleared hypotheses: s, f0, h'
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s' : Computation α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0 :
  Subtype.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) 0 =
    none
h' :
  tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) = s'
⊢ Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al =
    (tail
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f
          al)).think
have none : Subtype.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
    (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) =
  (tail
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f
            al)).think.val
    (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s' : Computation α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0 :
  Subtype.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) 0 =
    none
h' :
  tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) = s'
⊢ Subtype.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) =
    (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f
              al)).think.val
      (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a)
have none : f = Stream'.cons none f.tail
Tactic: dsimp [think, tail]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
s' : Computation α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0 :
  Subtype.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) 0 =
    none
h' :
  tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) = s'
⊢ f = Stream'.cons none f.tail
have none : f =
  Stream'.cons
    (Subtype.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
      (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) 0)
    f.tail
Tactic: rw [← f0]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
motive : Computation α → Sort v
s : Computation α
pure : (a : α) → motive (Computation.pure a)
think : (s : Computation α) → motive s.think
v : α
H : s.destruct = Sum.inl v
⊢ motive s
have rw : motive (Computation.pure v)
Tactic: rw [destruct_eq_pure H]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
motive : Computation α → Sort v
s : Computation α
pure : (a : α) → motive (Computation.pure a)
think : (s : Computation α) → motive s.think
v : Computation α
a : Stream' (Option α)
s' : ∀ ⦃n : ℕ⦄ ⦃a_1 : α⦄, a n = some a_1 → a (n + 1) = some a_1
H :
  s.destruct =
    Sum.inr (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) a s')
⊢ motive s
have rw : motive
  (Computation.think
    (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) a s'))
Tactic: rw [destruct_eq_think H]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
⊢ Computation α
have refine : ∀ (n : ℕ) (a' : α) (h : Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'),
  Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a'
Tactic: refine ⟨Stream'.corec' (Corec.f f) (Sum.inr b), fun n a' h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
h : Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'
⊢ Stream'.corec' (Corec.f f) (Sum.inr b) (n + 1) = some a'
have rw : Stream'.cons (Corec.f f (Sum.inr b)).fst (Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd) (n + 1) = some a'
Tactic: rw [Stream'.corec'_eq]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
h : Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'
⊢ Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd n = some a'
have revert : ∀ (h : Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'),
  Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd n = some a'
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
⊢ ∀ (h : Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'),
    Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd n = some a'
have generalize : ∀ (o : α ⊕ β) (h : Stream'.corec' (Corec.f f) o n = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
Tactic: generalize Sum.inr b = o
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
o : α ⊕ β
⊢ ∀ (h : Stream'.corec' (Corec.f f) o 0 = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd 0 = some a'
have zero : (Corec.f f o).fst = some a' → (Corec.f f (Corec.f f o).snd).fst = some a'
Tactic: change (Corec.f f o).1 = some a' → (Corec.f f (Corec.f f o).2).1 = some a'
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
o : α ⊕ β
⊢ (Corec.f f o).fst = some a' → (Corec.f f (Corec.f f o).snd).fst = some a'
have zero : ∀ (val : α), (Corec.f f (Sum.inl val)).fst = some a' → (Corec.f f (Corec.f f (Sum.inl val)).snd).fst = some a'
Tactic: rcases o with _ | b
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
o : α ⊕ β
zero : ∀ (val : α), (Corec.f f (Sum.inl val)).fst = some a' → (Corec.f f (Corec.f f (Sum.inl val)).snd).fst = some a'
⊢ (Corec.f f o).fst = some a' → (Corec.f f (Corec.f f o).snd).fst = some a'
have zero₁ : ∀ (b : β), (Corec.f f (Sum.inr b)).fst = some a' → (Corec.f f (Corec.f f (Sum.inr b)).snd).fst = some a'
Tactic: rcases o with _ | b
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b_1 : β
a' : α
b : β
h : (Corec.f f (Sum.inr b)).fst = some a'
⊢ (Corec.f f (Corec.f f (Sum.inr b)).snd).fst = some a'
have zero : Prod.fst (β := α ⊕ β)
    (match (motive := α ⊕ β → Option α × (α ⊕ β))
      Prod.snd (α := Option α)
        (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
        | Sum.inl a => (some a, Sum.inl a)
        | Sum.inr b =>
          (match (motive := α ⊕ β → Option α) f b with
            | Sum.inl a => some a
            | Sum.inr val => none,
            f b)) with
    | Sum.inl a => (some a, Sum.inl a)
    | Sum.inr b =>
      (match (motive := α ⊕ β → Option α) f b with
        | Sum.inl a => some a
        | Sum.inr val => none,
        f b)) =
  some a'
Tactic: unfold Corec.f at *
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b_1 : β
a' : α
b : β
h :
  Prod.fst (β := α ⊕ β)
      (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match (motive := α ⊕ β → Option α) f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)) =
    some a'
⊢ Prod.fst (β := α ⊕ β)
      (match (motive := α ⊕ β → Option α × (α ⊕ β))
        Prod.snd (α := Option α)
          (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
          | Sum.inl a => (some a, Sum.inl a)
          | Sum.inr b =>
            (match (motive := α ⊕ β → Option α) f b with
              | Sum.inl a => some a
              | Sum.inr val => none,
              f b)) with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match (motive := α ⊕ β → Option α) f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)) =
    some a'
have h_1 : ∀ (x : α ⊕ β) (a : α),
  Eq (α := α ⊕ β)
      (Prod.snd (α := Option α)
        (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
        | Sum.inl a => (some a, Sum.inl a)
        | Sum.inr b =>
          (match (motive := α ⊕ β → Option α) f b with
            | Sum.inl a => some a
            | Sum.inr val => none,
            f b)))
      (Sum.inl a) →
    Prod.fst (β := α ⊕ β) (some a, Sum.inl a) = some a'
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b_1 : β
a' : α
b : β
h :
  Prod.fst (β := α ⊕ β)
      (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match (motive := α ⊕ β → Option α) f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)) =
    some a'
h_1 :
  ∀ (x : α ⊕ β) (a : α),
    Eq (α := α ⊕ β)
        (Prod.snd (α := Option α)
          (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
          | Sum.inl a => (some a, Sum.inl a)
          | Sum.inr b =>
            (match (motive := α ⊕ β → Option α) f b with
              | Sum.inl a => some a
              | Sum.inr val => none,
              f b)))
        (Sum.inl a) →
      Prod.fst (β := α ⊕ β) (some a, Sum.inl a) = some a'
⊢ Prod.fst (β := α ⊕ β)
      (match (motive := α ⊕ β → Option α × (α ⊕ β))
        Prod.snd (α := Option α)
          (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
          | Sum.inl a => (some a, Sum.inl a)
          | Sum.inr b =>
            (match (motive := α ⊕ β → Option α) f b with
              | Sum.inl a => some a
              | Sum.inr val => none,
              f b)) with
      | Sum.inl a => (some a, Sum.inl a)
      | Sum.inr b =>
        (match (motive := α ⊕ β → Option α) f b with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f b)) =
    some a'
have h_2 : ∀ (x : α ⊕ β) (val : β),
  Eq (α := α ⊕ β)
      (Prod.snd (α := Option α)
        (match (motive := α ⊕ β → Option α × (α ⊕ β)) Sum.inr b with
        | Sum.inl a => (some a, Sum.inl a)
        | Sum.inr b =>
          (match (motive := α ⊕ β → Option α) f b with
            | Sum.inl a => some a
            | Sum.inr val => none,
            f b)))
      (Sum.inr val) →
    Prod.fst (β := α ⊕ β)
        (match (motive := α ⊕ β → Option α) f val with
          | Sum.inl a => some a
          | Sum.inr val => none,
          f val) =
      some a'
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
n : ℕ
IH :
  ∀ (o : α ⊕ β) (h : Stream'.corec' (Corec.f f) o n = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
o : α ⊕ β
⊢ ∀ (h : Stream'.corec' (Corec.f f) o (n + 1) = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd (n + 1) = some a'
have succ : ∀ (h : Stream'.cons (Corec.f f o).fst (Stream'.corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = some a'),
  Stream'.cons (Corec.f f (Corec.f f o).snd).fst (Stream'.corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd)
      (n + 1) =
    some a'
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.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
o : α ⊕ β
⊢ ∀ (h : Stream'.corec' (Corec.f f) o n = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
have zero : ∀ (o : α ⊕ β) (h : Stream'.corec' (Corec.f f) o 0 = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd 0 = some a'
Tactic: induction n generalizing o with
  | zero =>
    change (Corec.f f o).1 = some a' → (Corec.f f (Corec.f f o).2).1 = some a'
    rcases o with _ | b <;> intro h
    · exact h
    unfold Corec.f at *; split <;> simp_all
  | 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.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
o : α ⊕ β
zero :
  ∀ (o : α ⊕ β) (h : Stream'.corec' (Corec.f f) o 0 = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd 0 = some a'
⊢ ∀ (h : Stream'.corec' (Corec.f f) o n = some a'), Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
have succ : ∀ (n : ℕ)
  (IH :
    ∀ (o : α ⊕ β) (h : Stream'.corec' (Corec.f f) o n = some a'),
      Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a')
  (o : α ⊕ β) (h : Stream'.corec' (Corec.f f) o (n + 1) = some a'),
  Stream'.corec' (Corec.f f) (Corec.f f o).snd (n + 1) = some a'
Tactic: induction n generalizing o with
  | zero =>
    change (Corec.f f o).1 = some a' → (Corec.f f (Corec.f f o).2).1 = some a'
    rcases o with _ | b <;> intro h
    · exact h
    unfold Corec.f at *; split <;> simp_all
  | 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.Computation (goal)
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (corec f b).destruct = rmap (corec f) (f b)
have dsimp : Eq (α := α ⊕ Computation α)
  (match (motive := Option α → α ⊕ Computation α) Stream'.corec' (Corec.f f) (Sum.inr b) 0 with
    | none =>
      Sum.inr
        (tail
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            (Stream'.corec' (Corec.f f) (Sum.inr b)) sorry))
    | some a => Sum.inl a :
    α ⊕ Computation α)
  (match (motive := α ⊕ β → α ⊕ Computation α) f b with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
          (Stream'.corec' (Corec.f f) (Sum.inr b)) sorry) :
    α ⊕ Computation α)
Tactic: dsimp [corec, destruct]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ Stream'.corec' (Corec.f f) (Sum.inr b) 0 =
    Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (f b)
have dsimp : Eq (α := Option α)
  (match (motive := α ⊕ β → Option α) f b with
    | Sum.inl a => some a
    | Sum.inr val => none :
    Option α)
  (Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (f b) : Option α)
Tactic: dsimp [Corec.f, Stream'.corec', Stream'.corec, Stream'.map, Stream'.get, Stream'.iterate]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ Eq (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α) Stream'.corec' (Corec.f f) (Sum.inr b) 0 with
      | none =>
        Sum.inr
          (tail
            (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
              (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯))
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (match (motive := α ⊕ β → α ⊕ Computation α) f b with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            (Stream'.corec' (Corec.f f) (Sum.inr b)) ⋯) :
      α ⊕ Computation α)
have rw : Eq.{u + 1} (α := α ⊕ Computation α)
  (match (motive := Option α → α ⊕ Computation α)
      Sum.rec (motive := fun (x : α ⊕ β) ↦ Option α) some (fun (x : β) ↦ none) (f b) with
    | none =>
      Sum.inr
        (tail
          (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
            (Stream'.corec' (Corec.f f) (Sum.inr b)) sorry))
    | some a => Sum.inl a :
    α ⊕ Computation α)
  (match (motive := α ⊕ β → α ⊕ Computation α) f b with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)
          (Stream'.corec' (Corec.f f) (Sum.inr b)) sorry) :
    α ⊕ Computation α)
Tactic: rw [show Stream'.corec' (Corec.f f) (Sum.inr b) 0 =
    Sum.rec Option.some (fun _ ↦ none) (f b) by
    dsimp [Corec.f, Stream'.corec', Stream'.corec, Stream'.map, Stream'.get, Stream'.iterate]
    match (f b) with
    | Sum.inl x => rfl
    | Sum.inr x => rfl]