awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a_1 : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
s_2 : Seq (Seq1 γ)
y : γ
t : Seq γ
⊢ (join (((a, Seq.cons x s_1), Seq.cons (y, t) s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons (y, t) s_2), Seq.map join SS)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
⊢ LawfulMonad Seq1

Tactic:
LawfulMonad.mk'
  (id_map := @map_id)
  (bind_pure_comp := @bind_ret)
  (pure_bind := @ret_bind)
  (bind_assoc := @bind_assoc)

Premises used: Stream'.Seq1.ret_bind, Stream'.Seq1.map_id, LawfulMonad.mk', Stream'.Seq1.bind_assoc, Stream'.Seq1.bind_ret
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
c : Computation α
n : ℕ
a : α
h :
  Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
      n =
    some a
zero :
  ∀
    (h :
      Stream'.cons none
          (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)) 0 =
        some a),
    Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
        (HAdd.hAdd (α := ℕ) 0 1) =
      some a
succ :
  ∀ (n : ℕ)
    (h :
      Stream'.cons none
          (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a)) (n + 1) =
        some a),
    Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
        (n + 1 + 1) =
      some a
⊢ Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
      (n + 1) =
    some a

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
h :
  Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
      0 =
    some a
⊢ Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
      (HAdd.hAdd (α := ℕ) 0 1) =
    some a

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
n : ℕ
h :
  Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
      (n + 1) =
    some a
⊢ Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
      (n + 1 + 1) =
    some a

Tactic:
c.2 h

Premises used: Stream'.cons, Subtype.property
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
n : ℕ
h :
  Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
      (n + 1) =
    some a
⊢ Stream'.cons none (c.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a))
      (n + 1 + 1) =
    some a

Tactic:
exact c.2 h

Premises used: Subtype.property
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
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.inl a : α ⊕ Computation α) →
    s = pure a
⊢ s.destruct = Sum.inl a → s = pure a

Tactic:
dsimp [destruct]

Premises used: Computation.destruct
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
none :
  ∀
    (f0 :
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = Option.some a → f (n + 1) = Option.some a) 0 =
        Option.none),
    Eq.{u + 1} (α := α ⊕ Computation α)
        (match (motive := Option α → α ⊕ Computation α) Option.none with
          | Option.none => Sum.inr s.tail
          | Option.some a => Sum.inl a :
          α ⊕ Computation α)
        (Sum.inl a : α ⊕ Computation α) →
      s = pure a
some :
  ∀ (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),
    Eq (α := α ⊕ Computation α)
        (match (motive := Option α → α ⊕ Computation α) Option.some val with
          | Option.none => Sum.inr s.tail
          | Option.some a => Sum.inl a :
          α ⊕ Computation α)
        (Sum.inl a : α ⊕ Computation α) →
      s = pure a
⊢ Eq (α := α ⊕ Computation α)
      (match (motive := Option α → α ⊕ Computation α)
          s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = Option.some a → f (n + 1) = Option.some a)
            0 with
        | Option.none => Sum.inr s.tail
        | Option.some a => Sum.inl a :
        α ⊕ Computation α)
      (Sum.inl a : α ⊕ Computation α) →
    s = pure a

Tactic:
cases f0 : s.1 0

Premises used: OfNat.ofNat, Subtype.val
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a : α
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.inl a : α ⊕ Computation α)
⊢ s = pure a

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Computation
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 α)
some :
  s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = Option.some a → x (n + 1) = Option.some a) =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦
      ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = Option.some a → x (n + 1) = Option.some a)
⊢ s = pure a

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Computation
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 α)
some :
  ∀ (n : ℕ),
    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) =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦
      ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = Option.some a → x (n + 1) = Option.some a)

Tactic:
funext n
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a val : α
f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = some val
h :
  Eq (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α) some val with
      | none => Sum.inr s.tail
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (Sum.inl a : α ⊕ Computation α)
⊢ val = a

Tactic:
injection h with h'
-- Module: Mathlib.Data.Seq.Computation
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' : val = a
some some₁ some₂ some₃ :
  ∀
    (f0 :
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = Option.some a → f (n + 1) = Option.some a) 0 =
        Option.some a)
    (h' : val = a),
    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) 0 =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦
      ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = Option.some a → x (n + 1) = Option.some a) 0

Tactic:
rwa [h'] at f0
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a val : α
f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = some val
h :
  Eq (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α) some val with
      | none => Sum.inr s.tail
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (Sum.inl a : α ⊕ Computation α)
n : ℕ
IH :
  s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n
⊢ s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) (n + 1) =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) (n + 1)

Tactic:
s.2 IH

Premises used: Stream'.const, Subtype.property
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
a val : α
f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = some val
h :
  Eq (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α) some val with
      | none => Sum.inr s.tail
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (Sum.inl a : α ⊕ Computation α)
n : ℕ
IH :
  s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) n
⊢ s.val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) (n + 1) =
    (pure a).val (p := fun (x : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, x n = some a → x (n + 1) = some a) (n + 1)

Tactic:
exact s.2 IH

Premises used: Subtype.property
-- Module: Mathlib.Data.Seq.Computation
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
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)
⊢ 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

Tactic:
induction n with
    | zero => injection h with h'; rwa [h'] at f0
    | succ n IH => exact s.2 IH
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s s' : Computation α
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
⊢ s.destruct = Sum.inr s' → s = s'.think

Tactic:
dsimp [destruct]

Premises used: Computation.destruct
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s s' : Computation α
none :
  ∀
    (f0 :
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = Option.some a → f (n + 1) = Option.some a) 0 =
        Option.none),
    Eq.{u + 1} (α := α ⊕ Computation α)
        (match (motive := Option α → α ⊕ Computation α) Option.none with
          | Option.none => Sum.inr s.tail
          | Option.some a => Sum.inl a :
          α ⊕ Computation α)
        (Sum.inr s' : α ⊕ Computation α) →
      s = s'.think
some :
  ∀ (a' : α)
    (f0 :
      s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = Option.some a → f (n + 1) = Option.some a) 0 =
        Option.some a'),
    Eq (α := α ⊕ Computation α)
        (match (motive := Option α → α ⊕ Computation α) Option.some a' with
          | Option.none => Sum.inr s.tail
          | Option.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 = Option.some a → f (n + 1) = Option.some a)
            0 with
        | Option.none => Sum.inr s.tail
        | Option.some a => Sum.inl a :
        α ⊕ Computation α)
      (Sum.inr s' : α ⊕ Computation α) →
    s = s'.think

Tactic:
rcases f0 : s.1 0 with - | a'

Premises used: OfNat.ofNat, Subtype.val
-- Module: Mathlib.Data.Seq.Computation
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.tail = s'

Tactic:
injection h with h'
-- Module: Mathlib.Data.Seq.Computation
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 = Option.none
h' : s.tail = s'
none : s = s.tail.think
⊢ s = s'.think

Tactic:
rw [← h']
-- Module: Mathlib.Data.Seq.Computation
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 = Option.none
h' : s.tail = s'
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 =
        Option.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
⊢ s = s.tail.think

Tactic:
obtain ⟨f, al⟩ := s
-- Module: Mathlib.Data.Seq.Computation
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 =
    Option.none
h' :
  tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) = s'
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)
⊢ 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:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Computation
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 =
    Option.none
h' :
  tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) = s'
none : f = Stream'.cons Option.none f.tail
⊢ 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:
dsimp [think, tail]

Premises used: Computation.think, Computation.tail
-- Module: Mathlib.Data.Seq.Computation
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 =
    Option.none
h' :
  tail (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) f al) = s'
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
⊢ f = Stream'.cons Option.none f.tail

Tactic:
rw [← f0]
-- Module: Mathlib.Data.Seq.Computation
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
      (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:
(Stream'.eta f).symm

Premises used: Stream'.get, Stream'.eta, Eq.symm
-- Module: Mathlib.Data.Seq.Computation
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
      (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:
exact (Stream'.eta f).symm

Premises used: Stream'.eta, Eq.symm
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s s' : Computation α
a' : α
f0 : s.val (p := fun (f : Stream' (Option α)) ↦ ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a) 0 = some a'
h :
  Eq (α := α ⊕ Computation α)
    (match (motive := Option α → α ⊕ Computation α) some a' with
      | none => Sum.inr s.tail
      | some a => Sum.inl a :
      α ⊕ Computation α)
    (Sum.inr s' : α ⊕ Computation α)
⊢ s = s'.think

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
⊢ (pure a).destruct = Sum.inl a

Tactic:
rfl

Premises used: Computation.destruct, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
⊢ (empty α).destruct = Sum.inr (empty α)

Tactic:
rfl

Premises used: Computation.empty, Computation.tail, Computation.destruct, Stream'.get, Stream'.const, Stream'.tail, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
⊢ (pure a).head = some a

Tactic:
rfl

Premises used: Computation.head, Stream'.get, Stream'.const, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
⊢ s.think.head = none

Tactic:
rfl

Premises used: Computation.head, Stream'.get, Stream'.cons, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
⊢ (empty α).head = none

Tactic:
rfl

Premises used: Computation.head, Stream'.get, Stream'.const, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
a : α
⊢ (pure a).tail = pure a

Tactic:
rfl

Premises used: Computation.tail, Stream'.get, Computation.pure, Stream'.const, Stream'.tail, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
s : Computation α
⊢ s.think.tail = s

Tactic:
rfl

Premises used: Computation.tail, Computation, Stream'.get, Stream'.cons, Stream'.tail, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
⊢ (empty α).tail = empty α

Tactic:
rfl

Premises used: Computation.empty, Computation.tail, Stream'.get, Stream'.const, Stream'.tail, rfl
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
⊢ empty α = (empty α).think

Tactic:
destruct_eq_think destruct_empty

Premises used: Computation.destruct_empty, Computation.destruct_eq_think
-- Module: Mathlib.Data.Seq.Computation
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
rw : motive (Computation.pure v)
⊢ motive s

Tactic:
rw [destruct_eq_pure H]

Premises used: Computation.destruct_eq_pure
-- Module: Mathlib.Data.Seq.Computation
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 (Computation.pure v)

Tactic:
apply pure