awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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')
⊢ 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 α)))

Tactic:
⟨Stream'.eq_or_mem_of_mem_cons, fun o => ?_⟩

Premises used: Iff.intro, Stream'.eq_or_mem_of_mem_cons
-- 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 :
  ∀
    (o :
      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 α))))
⊢ 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 α)))

Tactic:
refine ⟨Stream'.eq_or_mem_of_mem_cons, fun o => ?_⟩
-- 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')
o :
  some (some a) = some (some a') ∨
    Any (fun (b : Option (Option α)) ↦ some (some a) = b) (↑s' : Stream' (Option (Option α)))
h1 :
  ∀ (e : some (some a) = some (some a')),
    Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α))))
h1₁ :
  ∀ (m : 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 α))))
⊢ Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α))))

Tactic:
rcases o with e | 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'))
i1 : x = a'
i2 : s = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
e : some (some a) = some (some a')
h1 : Any (fun (b : Option (Option α)) ↦ some (some a') = b) (some (some a') :: (↑s' : Stream' (Option (Option α))))
⊢ Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α))))

Tactic:
rw [e]
-- 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')
e : some (some a) = some (some a')
⊢ Any (fun (b : Option (Option α)) ↦ some (some a') = b) (some (some a') :: (↑s' : Stream' (Option (Option α))))

Tactic:
apply Stream'.mem_cons

Premises used: Stream'.mem_cons
-- 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_1 : (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')
m : 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 α))))

Tactic:
Stream'.mem_cons_of_mem _ m

Premises used: Stream'.mem_cons_of_mem
-- 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_1 : (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')
m : 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 α))))

Tactic:
exact Stream'.mem_cons_of_mem _ m

Premises used: Stream'.mem_cons_of_mem
-- 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.destruct = c
⊢ a ∈ s.think ↔ a = a' ∨ a ∈ s'

Tactic:
simp [IH this]
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
b a : α
⊢ some (b, s) ∈ (cons b s).destruct

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
b a : α
h : a ∈ s
⊢ a ∈ cons b s

Tactic:
(mem_cons_iff _ _).2 (Or.inr h)

Premises used: Iff.mpr, Stream'.WSeq.mem_cons_iff, Or.inr
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
⊢ a ∈ cons a s

Tactic:
(mem_cons_iff _ _).2 (Or.inl rfl)

Premises used: Iff.mpr, Stream'.WSeq.mem_cons_iff, Or.inl, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h : a ∈ s.tail
⊢ a ∈ s.tail

Tactic:
have := h
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h this : a ∈ s.tail
obtain : ∀ (n : ℕ) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))).get n), a ∈ s
⊢ a ∈ s

Tactic:
obtain ⟨n, e⟩ := h
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
this : a ∈ s.tail
n : ℕ
e : some (some a) = (↑s.tail : Stream' (Option (Option α))).get n
revert : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))).get n), a ∈ s
⊢ a ∈ s

Tactic:
revert s
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
zero : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) 0), a ∈ s
succ :
  ∀ (n : ℕ),
    (∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s) →
      ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) (n + 1)), a ∈ s
⊢ ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s

Tactic:
induction n
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
zero :
  ∀ (this : Membership.mem (γ := WSeq α) (tail nil) a)
    (e : some (some a) = (↑(tail nil) : Stream' (Option (Option α))) 0), Membership.mem (γ := WSeq α) nil a
zero₁ :
  ∀ (x : α) (s : WSeq α) (this : a ∈ (cons x s).tail)
    (e : some (some a) = (↑(cons x s).tail : Stream' (Option (Option α))) 0), a ∈ cons x s
zero₂ :
  ∀ (s : WSeq α) (this : a ∈ s.think.tail) (e : some (some a) = (↑s.think.tail : Stream' (Option (Option α))) 0),
    a ∈ s.think
⊢ ∀ (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) 0), a ∈ s

Tactic:
induction s using WSeq.recOn
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
s : WSeq α
succ :
  ∀ (this : Membership.mem (γ := WSeq α) (tail nil) a)
    (e : some (some a) = (↑(tail nil) : Stream' (Option (Option α))) (n + 1)), Membership.mem (γ := WSeq α) nil a
succ₁ :
  ∀ (x : α) (s : WSeq α) (this : a ∈ (cons x s).tail)
    (e : some (some a) = (↑(cons x s).tail : Stream' (Option (Option α))) (n + 1)), a ∈ cons x s
succ₂ :
  ∀ (s : WSeq α) (this : a ∈ s.think.tail) (e : some (some a) = (↑s.think.tail : Stream' (Option (Option α))) (n + 1)),
    a ∈ s.think
⊢ ∀ (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) (n + 1)), a ∈ s

Tactic:
induction s using WSeq.recOn
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
zero :
  ∀ (this : Membership.mem (γ := WSeq α) nil a) (e : some (some a) = Seq.get? nil 0), Membership.mem (γ := WSeq α) nil a
⊢ ∀ (this : Membership.mem (γ := WSeq α) (tail nil) a)
    (e : some (some a) = (↑(tail nil) : Stream' (Option (Option α))) 0), Membership.mem (γ := WSeq α) nil a

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a x : α
s : WSeq α
zero : ∀ (this : a ∈ s) (e : some (some a) = Seq.get? s 0), a = x ∨ a ∈ s
⊢ ∀ (this : a ∈ (cons x s).tail) (e : some (some a) = (↑(cons x s).tail : Stream' (Option (Option α))) 0), a ∈ cons x s

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
zero : ∀ (this : a ∈ s.tail) (e : some (some a) = Seq.get? s.tail.think 0), a ∈ s
⊢ ∀ (this : a ∈ s.think.tail) (e : some (some a) = (↑s.think.tail : Stream' (Option (Option α))) 0), a ∈ s.think

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
succ :
  ∀ (this : Membership.mem (γ := WSeq α) nil a) (e : some (some a) = Seq.get? nil (n + 1)),
    Membership.mem (γ := WSeq α) nil a
⊢ ∀ (this : Membership.mem (γ := WSeq α) (tail nil) a)
    (e : some (some a) = (↑(tail nil) : Stream' (Option (Option α))) (n + 1)), Membership.mem (γ := WSeq α) nil a

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
x : α
s : WSeq α
succ : ∀ (this : a ∈ s) (e : some (some a) = Seq.get? s (n + 1)), a = x ∨ a ∈ s
⊢ ∀ (this : a ∈ (cons x s).tail) (e : some (some a) = (↑(cons x s).tail : Stream' (Option (Option α))) (n + 1)),
    a ∈ cons x s

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
s : WSeq α
succ : ∀ (this : a ∈ s.tail) (e : some (some a) = Seq.get? s.tail.think (n + 1)), a ∈ s
⊢ ∀ (this : a ∈ s.think.tail) (e : some (some a) = (↑s.think.tail : Stream' (Option (Option α))) (n + 1)), a ∈ s.think

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
m : Membership.mem (γ := WSeq α) nil a
e : some (some a) = Seq.get? nil 0
⊢ Membership.mem (γ := WSeq α) nil a

Tactic:
injections
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
m : a ∈ s.tail
e : some (some a) = Seq.get? s.tail.think 0
⊢ a ∈ s

Tactic:
injections
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
m : Membership.mem (γ := WSeq α) nil a
e : some (some a) = Seq.get? nil (n + 1)
⊢ Membership.mem (γ := WSeq α) nil a

Tactic:
injections
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a x : α
s : WSeq α
m : a ∈ s
e : some (some a) = Seq.get? s 0
⊢ a = x ∨ a ∈ s

Tactic:
Or.inr m

Premises used: Or.inr
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a x : α
s : WSeq α
m : a ∈ s
e : some (some a) = Seq.get? s 0
⊢ a = x ∨ a ∈ s

Tactic:
exact Or.inr m

Premises used: Or.inr
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
x : α
s : WSeq α
m : a ∈ s
e : some (some a) = Seq.get? s (n + 1)
⊢ a = x ∨ a ∈ s

Tactic:
Or.inr m

Premises used: Or.inr
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
x : α
s : WSeq α
m : a ∈ s
e : some (some a) = Seq.get? s (n + 1)
⊢ a = x ∨ a ∈ s

Tactic:
exact Or.inr m

Premises used: Or.inr
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = Seq.get? s.tail.think (n + 1)
apply : some (some a) = (↑s.tail : Stream' (Option (Option α))) n
⊢ a ∈ s

Tactic:
apply IH m
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = Seq.get? s.tail.think (n + 1)
rw : Seq.get? s.tail.think (n + 1) = (↑s.tail : Stream' (Option (Option α))) n
⊢ some (some a) = (↑s.tail : Stream' (Option (Option α))) n

Tactic:
rw [e]
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = Seq.get? s.tail.think (n + 1)
mk :
  ∀ (val : Stream' (Option (Option α))) (property : val.IsSeq),
    Seq.get? (think (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) val property)) (n + 1) =
      (↑(Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) val property) : Stream' (Option (Option α)))
        n
⊢ Seq.get? s.tail.think (n + 1) = (↑s.tail : Stream' (Option (Option α))) n

Tactic:
cases tail s

Premises used: Stream'.WSeq.tail
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = Seq.get? s.tail.think (n + 1)
val : Stream' (Option (Option α))
property : val.IsSeq
⊢ Seq.get? (think (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) val property)) (n + 1) =
    (↑(Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) val property) : Stream' (Option (Option α))) n

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

Tactic:
induction n generalizing s
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
rcases : ∀ (o : Option (α × WSeq α)) (h1 : o ∈ (s.drop 0).destruct) (h2 : Prod.fst <$> o = some a), a ∈ s
⊢ a ∈ s

Tactic:
rcases Computation.exists_of_mem_map h with ⟨o, h1, h2⟩

Premises used: Computation.exists_of_mem_map
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
h : Option.some a ∈ s.get? 0
o : Option (α × WSeq α)
h1 : o ∈ (s.drop 0).destruct
h2 : Prod.fst <$> o = Option.some a
none :
  ∀ (h1 : Option.none ∈ (s.drop 0).destruct) (h2 : Functor.map (α := α × WSeq α) Prod.fst Option.none = Option.some a),
    a ∈ s
some :
  ∀ (o : α × WSeq α) (h1 : Option.some o ∈ (s.drop 0).destruct) (h2 : Prod.fst <$> Option.some o = Option.some a), a ∈ s
⊢ a ∈ s

Tactic:
rcases o with - | o
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
h1 : none ∈ (s.drop 0).destruct
h2 : Functor.map (α := α × WSeq α) Prod.fst none = some a
⊢ a ∈ s

Tactic:
injection h2
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
o : α × WSeq α
h1 : some o ∈ (s.drop 0).destruct
h2 : Prod.fst <$> some o = some a
⊢ o.1 = a

Tactic:
injection h2 with h'
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
h : Option.some a ∈ s.get? 0
o : α × WSeq α
h1 : Option.some o ∈ (s.drop 0).destruct
h' : o.1 = a
some : ∀ (a' : α) (s' : WSeq α) (h1 : Option.some (a', s') ∈ (s.drop 0).destruct) (h' : (a', s').1 = a), a ∈ s
⊢ a ∈ s

Tactic:
obtain ⟨a', s'⟩ := o
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
a' : α
s' : WSeq α
h1 : some (a', s') ∈ (s.drop 0).destruct
h' : (a', s').1 = a
⊢ a ∈ s

Tactic:
(eq_or_mem_iff_mem h1).2 (Or.inl h'.symm)

Premises used: Iff.mpr, Stream'.WSeq.drop, Stream'.WSeq.eq_or_mem_iff_mem, Or.inl, Eq.symm
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
a' : α
s' : WSeq α
h1 : some (a', s') ∈ (s.drop 0).destruct
h' : (a', s').1 = a
⊢ a ∈ s

Tactic:
exact (eq_or_mem_iff_mem h1).2 (Or.inl h'.symm)

Premises used: Iff.mpr, Stream'.WSeq.eq_or_mem_iff_mem, Or.inl, Eq.symm
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
⊢ a ∈ s

Tactic:
case zero =>
    rcases Computation.exists_of_mem_map h with ⟨o, h1, h2⟩
    rcases o with - | o
    · injection h2
    injection h2 with h'
    obtain ⟨a', s'⟩ := o
    exact (eq_or_mem_iff_mem h1).2 (Or.inl h'.symm)

Premises used: Computation.exists_of_mem_map
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
⊢ some a ∈ s.tail.get? n → a ∈ s.tail

Tactic:
have := @IH (tail s)
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
this : some a ∈ s.tail.get? n → a ∈ s.tail
⊢ some a ∈ s.get? (n + 1) → a ∈ s.tail

Tactic:
rw [get?_tail] at this

Premises used: Stream'.WSeq.get?_tail
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
this : some a ∈ s.get? (n + 1) → a ∈ s.tail
⊢ a ∈ s

Tactic:
mem_of_mem_tail (this h)

Premises used: Stream'.WSeq.mem_of_mem_tail
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
this : some a ∈ s.get? (n + 1) → a ∈ s.tail
⊢ a ∈ s

Tactic:
exact mem_of_mem_tail (this h)

Premises used: Stream'.WSeq.mem_of_mem_tail
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), (a = b ∨ ∃ (n : ℕ), some a ∈ s'.get? n) → ∃ (n : ℕ), some a ∈ (cons b s').get? n
h2 : ∀ (s : WSeq α), (∃ (n : ℕ), some a ∈ s.get? n) → ∃ (n : ℕ), some a ∈ s.think.get? n
⊢ ∃ (n : ℕ), some a ∈ s.get? n

Tactic:
apply mem_rec_on h

Premises used: Stream'.WSeq.mem_rec_on
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
h : a = a' ∨ ∃ (n : ℕ), some a ∈ s'.get? n
h1 : ∀ (h : a = a'), ∃ (n : ℕ), some a ∈ (cons a' s').get? n
h1₁ : ∀ (h : ∃ (n : ℕ), some a ∈ s'.get? n), ∃ (n : ℕ), some a ∈ (cons a' s').get? n
⊢ ∃ (n : ℕ), some a ∈ (cons a' s').get? n

Tactic:
rcases h with h | h
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
h : a = a'
h1 : some a ∈ (cons a' s').get? 0
⊢ ∃ (n : ℕ), some a ∈ (cons a' s').get? n

Tactic:
exists 0
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
h : a = a'
h1 : some a ∈ Computation.pure (some a')
⊢ some a ∈ (cons a' s').get? 0

Tactic:
simp only [get?, drop, head_cons]

Premises used: Stream'.WSeq.drop, Stream'.WSeq.get?, Stream'.WSeq.head_cons
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
h : a = a'
h1 : some a' ∈ Computation.pure (some a')
⊢ some a ∈ Computation.pure (some a')

Tactic:
rw [h]
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a' ∈ Computation.pure (some a')

Tactic:
apply ret_mem

Premises used: Computation.ret_mem
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
h : ∃ (n : ℕ), some a ∈ s'.get? n
h1 : ∀ (n : ℕ) (h : some a ∈ s'.get? n), ∃ (n : ℕ), some a ∈ (cons a' s').get? n
⊢ ∃ (n : ℕ), some a ∈ (cons a' s').get? n

Tactic:
obtain ⟨n, h⟩ := h
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
h1 : some a ∈ (cons a' s').get? (n + 1)
⊢ ∃ (n : ℕ), some a ∈ (cons a' s').get? n

Tactic:
exists n + 1
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ some a ∈ (cons a' s').get? (n + 1)

Tactic:
simpa [get?]

Premises used: Stream'.WSeq.get?
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
s' : WSeq α
h : ∃ (n : ℕ), some a ∈ s'.get? n
h2 : ∀ (n : ℕ) (h : some a ∈ s'.get? n), ∃ (n : ℕ), some a ∈ s'.think.get? n
⊢ ∃ (n : ℕ), some a ∈ s'.think.get? n

Tactic:
obtain ⟨n, h⟩ := h
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
h2 : some a ∈ s'.think.get? n
⊢ ∃ (n : ℕ), some a ∈ s'.think.get? n

Tactic:
exists n
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
h2 : some a ∈ (s'.drop n).head.think
⊢ some a ∈ s'.think.get? n

Tactic:
simp only [get?, dropn_think, head_think]

Premises used: Stream'.WSeq.dropn_think, Stream'.WSeq.get?, Stream'.WSeq.head_think
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ some a ∈ (s'.drop n).head.think

Tactic:
apply think_mem h

Premises used: Computation.think_mem
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
rcases : ∀ (o : Option (α × WSeq α)) (om : o ∈ (s.drop n).destruct), ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct
⊢ ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct

Tactic:
rcases (head_terminates_iff _).1 ⟨⟨_, h⟩⟩ with ⟨⟨o, om⟩⟩

Premises used: Computation.Terminates.mk, Stream'.WSeq.head_terminates_iff, Exists.intro, Iff.mp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : Option (α × WSeq α)
om : o ∈ (s.drop n).destruct
⊢ Prod.fst <$> o = some a

Tactic:
have := Computation.mem_unique (Computation.mem_map _ om) h
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : Option.some a ∈ s.get? n
o : Option (α × WSeq α)
om : o ∈ (s.drop n).destruct
this : Prod.fst <$> o = Option.some a
none :
  ∀ (om : Option.none ∈ (s.drop n).destruct)
    (this : Functor.map (α := α × WSeq α) Prod.fst Option.none = Option.some a),
    ∃ (s' : WSeq α), Option.some (a, s') ∈ (s.drop n).destruct
some :
  ∀ (o : α × WSeq α) (om : Option.some o ∈ (s.drop n).destruct) (this : Prod.fst <$> Option.some o = Option.some a),
    ∃ (s' : WSeq α), Option.some (a, s') ∈ (s.drop n).destruct
⊢ ∃ (s' : WSeq α), Option.some (a, s') ∈ (s.drop n).destruct

Tactic:
rcases o with - | o
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
om : none ∈ (s.drop n).destruct
this : Functor.map (α := α × WSeq α) Prod.fst none = some a
⊢ ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct

Tactic:
injection this
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : α × WSeq α
om : some o ∈ (s.drop n).destruct
this : Prod.fst <$> some o = some a
⊢ o.1 = a

Tactic:
injection this with i
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : Option.some a ∈ s.get? n
o : α × WSeq α
om : Option.some o ∈ (s.drop n).destruct
i : o.1 = a
some :
  ∀ (a' : α) (s' : WSeq α) (om : Option.some (a', s') ∈ (s.drop n).destruct) (i : (a', s').1 = a),
    ∃ (s' : WSeq α), Option.some (a, s') ∈ (s.drop n).destruct
⊢ ∃ (s' : WSeq α), Option.some (a, s') ∈ (s.drop n).destruct

Tactic:
obtain ⟨a', s'⟩ := o
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a', s') ∈ (s.drop n).destruct
i : a' = a
⊢ some (a, s') ∈ (s.drop n).destruct

Tactic:
rw [i] at om
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a', s') ∈ (s.drop n).destruct
i : a' = a
om₁ : some (a, s') ∈ (s.drop n).destruct
⊢ a' = a

Tactic:
rw [i] at om