awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
t' : α × WSeq α
ht' : some t' ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some t') = t
td₁ :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some t'))) (some a)
⊢ some t' ∈ s.destruct

Tactic:
rw [← ht2] at td
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
t' : α × WSeq α
ht' : some t' ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some t') = t
td₁ :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some t'))) (some a)
ht'₁ : some t' ∈ s.destruct
⊢ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some t') = t

Tactic:
rw [← ht2] at td
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)) (some a)
ht' : none ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none = t
⊢ Membership.mem (γ := Computation (Option (α × WSeq α))) (Computation.pure none) (some a)

Tactic:
simp only [destruct_nil] at td

Premises used: Stream'.WSeq.destruct_nil
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none = t
td : Membership.mem (γ := Computation (Option (α × WSeq α))) (Computation.pure none) (some a)
⊢ some a = none

Tactic:
have := mem_unique td (ret_mem _)
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none = t
td : Membership.mem (γ := Computation (Option (α × WSeq α))) (Computation.pure none) (some a)
this : some a = none
⊢ ∃ (a' : α × WSeq α), some a' ∈ s.destruct

Tactic:
contradiction
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
t' : α × WSeq α
td : some a ∈ t'.2.destruct
ht' : some t' ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some t') = t
⊢ ∃ (a' : α × WSeq α), some a' ∈ s.destruct

Tactic:
⟨_, ht'⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
t' : α × WSeq α
td : some a ∈ t'.2.destruct
ht' : some t' ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some t') = t
⊢ ∃ (a' : α × WSeq α), some a' ∈ s.destruct

Tactic:
exact ⟨_, ht'⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h :
  Membership.mem (γ := Computation (Option α))
    (Computation.map (fun (x : Option (α × WSeq α)) ↦ Prod.fst <$> x) s.tail.destruct) (some a)
rcases :
  ∀ (o : Option (α × WSeq α)) (md : o ∈ s.tail.destruct) (e : Prod.fst <$> o = some a), ∃ (a' : α), some a' ∈ s.head
⊢ ∃ (a' : α), some a' ∈ s.head

Tactic:
rcases Computation.exists_of_mem_map h with ⟨o, md, e⟩

Premises used: Computation.exists_of_mem_map
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
o : Option (α × WSeq α)
md : o ∈ s.tail.destruct
e : Prod.fst <$> o = Option.some a
none :
  ∀ (md : Option.none ∈ s.tail.destruct) (e : Functor.map (α := α × WSeq α) Prod.fst Option.none = Option.some a),
    ∃ (a' : α), Option.some a' ∈ s.head
some :
  ∀ (o : α × WSeq α) (md : Option.some o ∈ s.tail.destruct) (e : Prod.fst <$> Option.some o = Option.some a),
    ∃ (a' : α), Option.some a' ∈ s.head
⊢ ∃ (a' : α), Option.some a' ∈ s.head

Tactic:
rcases o with - | o
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
md : none ∈ s.tail.destruct
e : Functor.map (α := α × WSeq α) Prod.fst none = some a
⊢ ∃ (a' : α), some a' ∈ s.head

Tactic:
injection e
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
o : α × WSeq α
md : some o ∈ s.tail.destruct
e : Prod.fst <$> some o = some a
⊢ o.1 = a

Tactic:
injection e with h'
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
o : Option (α × WSeq α)
md : o ∈ s.tail.destruct
e : Prod.fst <$> o = Option.some a
some : ∀ (o : α × WSeq α) (md : Option.some o ∈ s.tail.destruct) (h' : o.1 = a), ∃ (a' : α), Option.some a' ∈ s.head
⊢ ∃ (a' : α), Option.some a' ∈ s.head

Tactic:
rcases o with - | o <;> [injection e; injection e with h']
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
o : α × WSeq α
md : Option.some o ∈ s.tail.destruct
some : ∀ (a : α × WSeq α) (am : Option.some a ∈ s.destruct), ∃ (a' : α), Option.some a' ∈ s.head
⊢ ∃ (a' : α), Option.some a' ∈ s.head

Tactic:
obtain ⟨a, am⟩ := destruct_some_of_destruct_tail_some md

Premises used: Stream'.WSeq.destruct_some_of_destruct_tail_some
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a_1 : α
o : α × WSeq α
md : some o ∈ s.tail.destruct
a : α × WSeq α
am : some a ∈ s.destruct
⊢ ∃ (a' : α), some a' ∈ s.head

Tactic:
⟨_, Computation.mem_map (@Prod.fst α (WSeq α) <$> ·) am⟩

Premises used: Prod.fst, Exists.intro, Computation.mem_map, Functor.map
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a_1 : α
o : α × WSeq α
md : some o ∈ s.tail.destruct
a : α × WSeq α
am : some a ∈ s.destruct
⊢ ∃ (a' : α), some a' ∈ s.head

Tactic:
exact ⟨_, Computation.mem_map (@Prod.fst α (WSeq α) <$> ·) am⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h : some a ∈ s.get? 0
⊢ ∃ (a' : α), some a' ∈ s.head

Tactic:
⟨_, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h : some a ∈ s.get? 0
⊢ ∃ (a' : α), some a' ∈ s.head

Tactic:
exact ⟨_, h⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
n : ℕ
IH : ∀ {a : α} (h : some a ∈ s.get? n), ∃ (a' : α), some a' ∈ s.head
a : α
h : some a ∈ s.get? (n + 1)
succ : ∀ (a' : α) (h' : some a' ∈ (s.drop n).head), ∃ (a' : α), some a' ∈ s.head
⊢ ∃ (a' : α), some a' ∈ s.head

Tactic:
let ⟨a', h'⟩ := head_some_of_head_tail_some h
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
n : ℕ
IH : ∀ {a : α} (h : some a ∈ s.get? n), ∃ (a' : α), some a' ∈ s.head
a : α
h : some a ∈ s.get? (n + 1)
a' : α
h' : some a' ∈ (s.drop n).head
⊢ ∃ (a' : α), some a' ∈ s.head

Tactic:
IH h'
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
n : ℕ
IH : ∀ {a : α} (h : some a ∈ s.get? n), ∃ (a' : α), some a' ∈ s.head
a : α
h : some a ∈ s.get? (n + 1)
a' : α
h' : some a' ∈ (s.drop n).head
⊢ ∃ (a' : α), some a' ∈ s.head

Tactic:
exact IH h'
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
n : ℕ
h : some a ∈ s.get? n
zero : ∀ {a : α} (h : some a ∈ s.get? 0), ∃ (a' : α), some a' ∈ s.head
succ :
  ∀ (n : ℕ) (IH : ∀ {a : α} (h : some a ∈ s.get? n), ∃ (a' : α), some a' ∈ s.head) {a : α}
    (h : some a ∈ s.get? (n + 1)), ∃ (a' : α), some a' ∈ s.head
⊢ ∃ (a' : α), some a' ∈ s.head

Tactic:
induction n generalizing a with
  | zero => exact ⟨_, h⟩
  | succ n IH =>
      let ⟨a', h'⟩ := head_some_of_head_tail_some h
      exact IH h'
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
m n : ℕ
⊢ (s.get? m).Terminates → (s.get? m).Terminates

Tactic:
id

Premises used: id
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
m n : ℕ
⊢ (s.get? m).Terminates → (s.get? m).Terminates

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
m n m_1 : ℕ
h : m.le m_1
IH : (s.get? m_1).Terminates → (s.get? m).Terminates
⊢ (s.get? m_1.succ).Terminates → (s.get? m).Terminates

Tactic:
fun T ↦ IH (@head_terminates_of_head_tail_terminates _ _ T)

Premises used: Stream'.WSeq.drop, Stream'.WSeq.head_terminates_of_head_tail_terminates
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
m n m_1 : ℕ
h : m.le m_1
IH : (s.get? m_1).Terminates → (s.get? m).Terminates
⊢ (s.get? m_1.succ).Terminates → (s.get? m).Terminates

Tactic:
exact fun T ↦ IH (@head_terminates_of_head_tail_terminates _ _ T)

Premises used: Stream'.WSeq.drop, Stream'.WSeq.head_terminates_of_head_tail_terminates
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
m n : ℕ
h : m ≤ n
refl : (s.get? m).Terminates → (s.get? m).Terminates
step :
  ∀ {m_1 : ℕ},
    m.le m_1 →
      ∀ (IH : (s.get? m_1).Terminates → (s.get? m).Terminates), (s.get? m_1.succ).Terminates → (s.get? m).Terminates
⊢ (s.get? n).Terminates → (s.get? m).Terminates

Tactic:
induction h with
  | refl => exact id
  | step _ IH => exact fun T ↦ IH (@head_terminates_of_head_tail_terminates _ _ T)

Premises used: id, refl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
n : ℕ
⊢ (s.get? n).Terminates → s.head.Terminates

Tactic:
get?_terminates_le (Nat.zero_le n)

Premises used: Nat.zero_le, Stream'.WSeq.drop, Stream'.WSeq.get?, Stream'.WSeq.get?_terminates_le
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
n : ℕ
T : (s.get? n).Terminates
⊢ s.destruct.Terminates

Tactic:
(head_terminates_iff _).1 <| head_terminates_of_get?_terminates T

Premises used: Stream'.WSeq.head_terminates_iff, Iff.mp, Stream'.WSeq.head_terminates_of_get?_terminates
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
apply : ∀ (b : Option α) (s' : Seq (Option α)), some a = b ∨ C s' → C (Seq.cons b s')
⊢ C s

Tactic:
apply Seq.mem_rec_on M

Premises used: Stream'.Seq.mem_rec_on
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
o : Option α
s' : Seq (Option α)
h : Option.some a = o ∨ C s'
none : ∀ (h : Option.some a = Option.none ∨ C s'), C (Seq.cons Option.none s')
some : ∀ (b : α) (h : Option.some a = Option.some b ∨ C s'), C (Seq.cons (Option.some b) s')
⊢ C (Seq.cons o s')

Tactic:
rcases o with - | b
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
h : some a = Option.none ∨ C s'
none : C s'
⊢ C (Seq.cons Option.none s')

Tactic:
apply h2
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
h : some a = Option.none ∨ C s'
none : some a = Option.none → C s'
none₁ : C s' → C s'
⊢ C s'

Tactic:
cases h
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
h : some a = none
⊢ C s'

Tactic:
contradiction
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
h : C s'
⊢ C s'

Tactic:
assumption
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
b : α
h : Option.some a = Option.some b ∨ C s'
some : a = b ∨ C s'
⊢ C (Seq.cons (Option.some b) s')

Tactic:
apply h1
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
b : α
h : some a = some b ∨ C s'
apply : some a = some b → a = b
⊢ a = b ∨ C s'

Tactic:
apply Or.imp_left _ h

Premises used: Or.imp_left
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
b : α
h_1 : some a = some b ∨ C s'
h : some a = some b
⊢ a = b

Tactic:
injection h
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
obtain :
  ∀ (f : Stream' (Option (Option α))) (al : f.IsSeq),
    a ∈ think (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) f al) ↔
      a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) f al
⊢ a ∈ s.think ↔ a ∈ s

Tactic:
obtain ⟨f, al⟩ := s
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
change : some (some a) ∈ some none :: f ↔ some (some a) ∈ f
⊢ a ∈ think (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) f al) ↔
    a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) f al

Tactic:
change (some (some a) ∈ some none::f) ↔ some (some a) ∈ f

Premises used: Option.some, Membership.mem, Option.none, Stream'.cons
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
mp : some (some a) ∈ some none :: f → some (some a) ∈ f
mpr : some (some a) ∈ f → some (some a) ∈ some none :: f
⊢ some (some a) ∈ some none :: f ↔ some (some a) ∈ f

Tactic:
constructor
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ some none :: f
mp : ¬some (some a) = some none
⊢ some (some a) ∈ f

Tactic:
apply (Stream'.eq_or_mem_of_mem_cons h).resolve_left

Premises used: Or.resolve_left, Stream'.eq_or_mem_of_mem_cons
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ some none :: f
h_1 : some (some a) = some none
⊢ False

Tactic:
injections
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ f
⊢ some (some a) ∈ some none :: f

Tactic:
apply Stream'.mem_cons_of_mem _ h

Premises used: Stream'.mem_cons_of_mem
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a a' : α
s' : WSeq α
generalize :
  ∀ (c : Computation (Option (α × WSeq α))) (e : s.destruct = c), some (a', s') ∈ c → (a ∈ s ↔ a = a' ∨ a ∈ s')
⊢ some (a', s') ∈ s.destruct → (a ∈ s ↔ a = a' ∨ a ∈ s')

Tactic:
generalize e : destruct s = c

Premises used: Stream'.WSeq.destruct
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
e : s.destruct = c
h : some (a', s') ∈ c
revert : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
⊢ a ∈ s ↔ a = a' ∨ a ∈ s'

Tactic:
revert s
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
h1 : ∀ {s : WSeq α} (e : s.destruct = Computation.pure (some (a', s'))), a ∈ s ↔ a = a' ∨ a ∈ s'
h2 :
  ∀ (s : Computation (Option (α × WSeq α))),
    (∀ {s_1 : WSeq α} (e : s_1.destruct = s), a ∈ s_1 ↔ a = a' ∨ a ∈ s') →
      ∀ {s_1 : WSeq α} (e : s_1.destruct = s.think), a ∈ s_1 ↔ a = a' ∨ a ∈ s'
⊢ ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'

Tactic:
apply Computation.memRecOn h

Premises used: Computation.memRecOn
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
h1 : ∀ {s : WSeq α} (e : s.destruct = Computation.pure (some (a', s'))), a ∈ s ↔ a = a' ∨ a ∈ s'
h2 :
  ∀ (c : Computation (Option (α × WSeq α))) (IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s')
    {s : WSeq α} (e : s.destruct = c.think), a ∈ s ↔ a = a' ∨ a ∈ s'
⊢ ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'

Tactic:
apply Computation.memRecOn h <;> [skip; intro c IH]

Premises used: Computation.memRecOn
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s : WSeq α
h1 : ∀ (e : destruct nil = Computation.pure (some (a', s'))), Membership.mem (γ := WSeq α) nil a ↔ a = a' ∨ a ∈ s'
h1₁ :
  ∀ (x : α) (s : WSeq α) (e : (cons x s).destruct = Computation.pure (some (a', s'))), a ∈ cons x s ↔ a = a' ∨ a ∈ s'
h1₂ : ∀ (s : WSeq α) (e : s.think.destruct = Computation.pure (some (a', s'))), a ∈ s.think ↔ a = a' ∨ a ∈ s'
⊢ ∀ (e : s.destruct = Computation.pure (some (a', s'))), a ∈ s ↔ a = a' ∨ a ∈ s'

Tactic:
induction s using WSeq.recOn
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c_1 : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c_1
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
s : WSeq α
h2 : ∀ (e : destruct nil = c.think), Membership.mem (γ := WSeq α) nil a ↔ a = a' ∨ a ∈ s'
h2₁ : ∀ (x : α) (s : WSeq α) (e : (cons x s).destruct = c.think), a ∈ cons x s ↔ a = a' ∨ a ∈ s'
h2₂ : ∀ (s : WSeq α) (e : s.think.destruct = c.think), a ∈ s.think ↔ a = a' ∨ a ∈ s'
⊢ ∀ (e : s.destruct = c.think), a ∈ s ↔ a = a' ∨ a ∈ s'

Tactic:
induction s using WSeq.recOn
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
m : destruct nil = Computation.pure (some (a', s'))
⊢ Computation.destruct (destruct nil) = (Computation.pure (some (a', s'))).destruct

Tactic:
have := congr_arg Computation.destruct m
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
⊢ (cons x s).destruct.destruct = (Computation.pure (some (a', s'))).destruct

Tactic:
have := congr_arg Computation.destruct m
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s : WSeq α
m : s.think.destruct = Computation.pure (some (a', s'))
⊢ s.think.destruct.destruct = (Computation.pure (some (a', s'))).destruct

Tactic:
have := congr_arg Computation.destruct m
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c_1 : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c_1
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
m : destruct nil = c.think
⊢ Computation.destruct (destruct nil) = c.think.destruct

Tactic:
have := congr_arg Computation.destruct m
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c_1 : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c_1
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
x : α
s : WSeq α
m : (cons x s).destruct = c.think
⊢ (cons x s).destruct.destruct = c.think.destruct

Tactic:
have := congr_arg Computation.destruct m
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c_1 : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c_1
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
s : WSeq α
m : s.think.destruct = c.think
⊢ s.think.destruct.destruct = c.think.destruct

Tactic:
have := congr_arg Computation.destruct m
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
m : destruct nil = Computation.pure (some (a', s'))
this : Computation.destruct (destruct nil) = (Computation.pure (some (a', s'))).destruct
⊢ Membership.mem (γ := WSeq α) nil a ↔ a = a' ∨ a ∈ s'

Tactic:
simp at this
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
this : (cons x s).destruct.destruct = (Computation.pure (some (a', s'))).destruct
⊢ x = a' ∧ s = s'

Tactic:
simp at this
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s : WSeq α
m : s.think.destruct = Computation.pure (some (a', s'))
this : s.think.destruct.destruct = (Computation.pure (some (a', s'))).destruct
⊢ a ∈ s.think ↔ a = a' ∨ a ∈ s'

Tactic:
simp at this
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c_1 : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c_1
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
m : destruct nil = c.think
this : Computation.destruct (destruct nil) = c.think.destruct
⊢ Membership.mem (γ := WSeq α) nil a ↔ a = a' ∨ a ∈ s'

Tactic:
simp at this
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c_1 : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c_1
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
x : α
s : WSeq α
m : (cons x s).destruct = c.think
this : (cons x s).destruct.destruct = c.think.destruct
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'

Tactic:
simp at this
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c_1 : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c_1
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
s : WSeq α
m : s.think.destruct = c.think
this : s.think.destruct.destruct = c.think.destruct
⊢ s.destruct = c

Tactic:
simp at this
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
this : x = a' ∧ s = s'
⊢ x = a'

Tactic:
obtain ⟨i1, i2⟩ := this
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
this : x = a' ∧ s = s'
i1 : x = a'
⊢ s = s'

Tactic:
obtain ⟨i1, i2⟩ := this
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
h1 : a ∈ cons a' s' ↔ a = a' ∨ a ∈ s'
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'

Tactic:
rw [i1, i2]
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
⊢ a = a' ↔ some (some a) = some (some a')

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
⊢ a = a' ↔ some (some a) = some (some a')

Tactic:
have h_a_eq_a' : a = a' ↔ some (some a) = some (some a') := by simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
h1 :
  Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α)))) ↔
    some (some a) = some (some a') ∨
      Any (fun (b : Option (Option α)) ↦ some (some a) = b) (↑s' : Stream' (Option (Option α)))
⊢ Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α)))) ↔
    a = a' ∨ Any (fun (b : Option (Option α)) ↦ some (some a) = b) (↑s' : Stream' (Option (Option α)))

Tactic:
rw [h_a_eq_a']