awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
l : List α
nil : Membership.mem (γ := Computation (List α)) (toList (↑[] : WSeq α)) []
cons : ∀ (a : α) (l : List α) (IH : l ∈ (↑l : WSeq α).toList), a :: l ∈ (↑(a :: l) : WSeq α).toList
⊢ l ∈ (↑l : WSeq α).toList

Tactic:
induction l with
  | nil => simp
  | cons a l IH => simpa [ret_mem] using think_mem (Computation.mem_map _ IH)

Premises used: Stream'.WSeq.cons, Stream'.WSeq.nil, Computation.ret_mem
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : Seq α
simp :
  Eq.{u + 1} (α := Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (match (motive := Option (α × WSeq α) ⊕ WSeq α → Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
        match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
          Option.map (fun (a' : Option α) ↦ (a', (some <$> s).tail)) ((some <$> s).get? 0) with
        | none => Sum.inl none
        | some (none, s') => Sum.inr s'
        | some (some a, s') => Sum.inl (some (a, s')) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Computation.corec
            (fun (s : WSeq α) ↦
              match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
                Option.map (fun (a' : Option α) ↦ (a', Seq.tail s)) (Seq.get? s 0) with
              | none => Sum.inl none
              | some (none, s') => Sum.inr s'
              | some (some a, s') => Sum.inl (some (a, s')))
            b) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (Sum.inl (Option.map (fun (a : α) ↦ (a, some <$> s.tail)) (s.get? 0)) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
⊢ (↑s : WSeq α).destruct.destruct = Sum.inl (Option.map (fun (a : α) ↦ (a, (↑s.tail : WSeq α))) s.head)

Tactic:
simp only [destruct, Seq.destruct, Option.map_eq_map, ofSeq, Computation.corec_eq, rmap,
      Seq.head]

Premises used: Stream'.WSeq.destruct, Computation.rmap, Stream'.Seq.head, Stream'.WSeq.ofSeq, Computation.corec_eq, Stream'.Seq.destruct, Option.map_eq_map
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : Seq α
⊢ (some <$> s).get? 0 = some <$> s.get? 0

Tactic:
apply Seq.map_get?

Premises used: Stream'.Seq.map_get?
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : Seq α
rw :
  Eq.{u + 1} (α := Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (match (motive := Option (α × WSeq α) ⊕ WSeq α → Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
        match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
          Option.map (fun (a' : Option α) ↦ (a', (some <$> s).tail)) (some <$> s.get? 0) with
        | none => Sum.inl none
        | some (none, s') => Sum.inr s'
        | some (some a, s') => Sum.inl (some (a, s')) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Computation.corec
            (fun (s : WSeq α) ↦
              match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
                Option.map (fun (a' : Option α) ↦ (a', Seq.tail s)) (Seq.get? s 0) with
              | none => Sum.inl none
              | some (none, s') => Sum.inr s'
              | some (some a, s') => Sum.inl (some (a, s')))
            b) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (Sum.inl (Option.map (fun (a : α) ↦ (a, some <$> s.tail)) (s.get? 0)) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
⊢ Eq.{u + 1} (α := Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (match (motive := Option (α × WSeq α) ⊕ WSeq α → Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
        match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
          Option.map (fun (a' : Option α) ↦ (a', (some <$> s).tail)) ((some <$> s).get? 0) with
        | none => Sum.inl none
        | some (none, s') => Sum.inr s'
        | some (some a, s') => Sum.inl (some (a, s')) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Computation.corec
            (fun (s : WSeq α) ↦
              match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
                Option.map (fun (a' : Option α) ↦ (a', Seq.tail s)) (Seq.get? s 0) with
              | none => Sum.inl none
              | some (none, s') => Sum.inr s'
              | some (some a, s') => Sum.inl (some (a, s')))
            b) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (Sum.inl (Option.map (fun (a : α) ↦ (a, some <$> s.tail)) (s.get? 0)) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))

Tactic:
rw [show Seq.get? (some <$> s) 0 = some <$> Seq.get? s 0 by apply Seq.map_get?]
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : Seq α
⊢ Eq.{u + 1} (α := Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (match (motive := Option (α × WSeq α) ⊕ WSeq α → Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
        match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
          Option.map (fun (a' : Option α) ↦ (a', (some <$> s).tail)) (some <$> none) with
        | none => Sum.inl none
        | some (none, s') => Sum.inr s'
        | some (some a, s') => Sum.inl (some (a, s')) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Computation.corec
            (fun (s : WSeq α) ↦
              match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
                Option.map (fun (a' : Option α) ↦ (a', Seq.tail s)) (Seq.get? s 0) with
              | none => Sum.inl none
              | some (none, s') => Sum.inr s'
              | some (some a, s') => Sum.inl (some (a, s')))
            b) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (Sum.inl (Option.map (fun (a : α) ↦ (a, some <$> s.tail)) none) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))

Tactic:
rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : Seq α
a : α
⊢ Eq.{u + 1} (α := Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (match (motive := Option (α × WSeq α) ⊕ WSeq α → Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
        match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
          Option.map (fun (a' : Option α) ↦ (a', (Seq.map some s).tail)) (Option.map some (some a)) with
        | none => Sum.inl none
        | some (none, s') => Sum.inr s'
        | some (some a, s') => Sum.inl (some (a, s')) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Computation.corec
            (fun (s : WSeq α) ↦
              match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
                Option.map (fun (a' : Option α) ↦ (a', Seq.tail s)) (Seq.get? s 0) with
              | none => Sum.inl none
              | some (none, s') => Sum.inr s'
              | some (some a, s') => Sum.inl (some (a, s')))
            b) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (Sum.inl (Option.map (fun (a : α) ↦ (a, Seq.map some s.tail)) (some a)) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : Seq α
simp :
  Computation.pure (Option.map (comp (β := α × WSeq α) Prod.fst fun (a : α) ↦ (a, (↑s.tail : WSeq α))) s.head) =
    Computation.pure s.head
⊢ (↑s : WSeq α).head = Computation.pure s.head

Tactic:
simp only [head, Option.map_eq_map, destruct_ofSeq, Computation.map_pure, Option.map_map]

Premises used: Computation.map_pure, Stream'.WSeq.destruct_ofSeq, Option.map_map, Option.map_eq_map, Stream'.WSeq.head
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : Seq α
none :
  Eq.{u + 1} (α := Computation (Option α))
    (Computation.pure
      (Option.map (α := α) (comp (β := α × WSeq α) Prod.fst fun (a : α) ↦ (a, (↑s.tail : WSeq α))) Option.none))
    (Computation.pure Option.none)
some :
  ∀ (val : α),
    Computation.pure
        (Option.map (comp (β := α × WSeq α) Prod.fst fun (a : α) ↦ (a, (↑s.tail : WSeq α))) (Option.some val)) =
      Computation.pure (Option.some val)
⊢ Computation.pure (Option.map (comp (β := α × WSeq α) Prod.fst fun (a : α) ↦ (a, (↑s.tail : WSeq α))) s.head) =
    Computation.pure s.head

Tactic:
cases Seq.head s

Premises used: Stream'.Seq.head
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : Seq α
⊢ Eq.{u + 1} (α := Computation (Option α))
    (Computation.pure
      (Option.map (α := α) (comp (β := α × WSeq α) Prod.fst fun (a : α) ↦ (a, (↑s.tail : WSeq α))) none))
    (Computation.pure none)

Tactic:
rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : Seq α
val : α
⊢ Computation.pure (Option.map (comp (β := α × WSeq α) Prod.fst fun (a : α) ↦ (a, (↑s.tail : WSeq α))) (some val)) =
    Computation.pure (some val)

Tactic:
rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : Seq α
simp :
  Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd
      (Option.map (fun (a : α) ↦ (a, (↑s.tail : WSeq α))) s.head) =
    (↑s.tail : WSeq α)
⊢ (↑s : WSeq α).tail = (↑s.tail : WSeq α)

Tactic:
simp only [tail, destruct_ofSeq, map_pure', flatten_pure]

Premises used: Stream'.WSeq.destruct_ofSeq, Stream'.WSeq.tail, Stream'.WSeq.flatten_pure, Computation.map_pure'
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : Seq α
nil :
  Eq.{u + 1} (α := WSeq α)
    (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) WSeq.nil Prod.snd
        (Option.map (fun (a : α) ↦ (a, (↑(Seq.tail Seq.nil) : WSeq α))) (Seq.head Seq.nil)) :
      WSeq α)
    ((↑(Seq.tail Seq.nil) : WSeq α) : WSeq α)
cons :
  ∀ (x : α) (s : Seq α),
    Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) WSeq.nil Prod.snd
        (Option.map (fun (a : α) ↦ (a, (↑(Seq.cons x s).tail : WSeq α))) (Seq.cons x s).head) =
      (↑(Seq.cons x s).tail : WSeq α)
⊢ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) WSeq.nil Prod.snd
      (Option.map (fun (a : α) ↦ (a, (↑s.tail : WSeq α))) s.head) =
    (↑s.tail : WSeq α)

Tactic:
induction s using Seq.recOn

Premises used: Stream'.Seq.recOn
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
x : α
s : Seq α
⊢ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd
      (Option.map (fun (a : α) ↦ (a, (↑(Seq.cons x s).tail : WSeq α))) (Seq.cons x s).head) =
    (↑(Seq.cons x s).tail : WSeq α)

Tactic:
simp only [ofSeq, Seq.tail_nil, Seq.head_nil,
    Option.map_none, Seq.tail_cons, Seq.head_cons, Option.map_some]

Premises used: Stream'.Seq.tail_cons, Stream'.WSeq.ofSeq, Stream'.Seq.head_cons, Stream'.Seq.tail_nil, Option.map_some, Option.map_none, Stream'.Seq.head_nil
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := WSeq α) nil (some <$> Seq.nil)

Tactic:
rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
rw : (↑(s.drop n) : WSeq α).tail = (↑(s.drop n).tail : WSeq α)
rw₁ rw₂ : (↑(s.drop n).tail : WSeq α) = (↑(s.drop n).tail : WSeq α)
⊢ ((↑s : WSeq α).drop n).tail = (↑(s.drop n).tail : WSeq α)

Tactic:
rw [dropn_ofSeq s n, tail_ofSeq]

Premises used: Stream'.WSeq.tail_ofSeq
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
rw : (↑(s.drop n) : WSeq α).head = Computation.pure (s.get? n)
rw₁ : Computation.pure (s.drop n).head = Computation.pure (s.get? n)
rw₂ rw₃ : Computation.pure (s.get? n) = Computation.pure (s.get? n)
⊢ ((↑s : WSeq α).drop n).head = Computation.pure (s.get? n)

Tactic:
rw [dropn_ofSeq, head_ofSeq, Seq.head_dropn]

Premises used: Stream'.WSeq.head_ofSeq, Stream'.WSeq.dropn_ofSeq, Stream'.Seq.head_dropn
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
⊢ map f nil = nil

Tactic:
rfl

Premises used: Stream'.Seq.nil, Stream'.map, Stream'.WSeq.map, Stream'.WSeq.nil, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : WSeq α
⊢ map f (cons a s) = cons (f a) (map f s)

Tactic:
Seq.map_cons _ _ _

Premises used: Stream'.WSeq.cons, Stream'.Seq.map_cons, Stream'.WSeq.map, Stream'.WSeq
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ map f s.think = (map f s).think

Tactic:
Seq.map_cons _ _ _

Premises used: Stream'.Seq.map_cons, Stream'.WSeq.think, Stream'.WSeq.map, Stream'.WSeq
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
⊢ map id s = s

Tactic:
simp [map]

Premises used: Stream'.WSeq.map
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
a : α
⊢ map f (ret a) = ret (f a)

Tactic:
simp [ret]

Premises used: Stream'.WSeq.ret
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s t : WSeq α
⊢ map f (s.append t) = (map f s).append (map f t)

Tactic:
Seq.map_append _ _ _

Premises used: Stream'.Seq.map_append, Stream'.WSeq.map, Stream'.WSeq, Stream'.WSeq.append
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
rw : Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g ∘ Option.map f) s
⊢ Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g) (Seq.map (Option.map f) s)

Tactic:
rw [← Seq.map_comp]

Premises used: Stream'.Seq.map_comp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
h : Seq.map (Option.map (g ∘ f)) = Seq.map (Option.map g ∘ Option.map f)
⊢ Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g ∘ Option.map f) s

Tactic:
apply congr_fun

Premises used: congr_fun
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
h : Option.map (g ∘ f) = Option.map g ∘ Option.map f
⊢ Seq.map (Option.map (g ∘ f)) = Seq.map (Option.map g ∘ Option.map f)

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
h : ∀ (a : γ), Option.map (g ∘ f) none = some a ↔ (Option.map g ∘ Option.map f) none = some a
h₁ : ∀ (val : α) (a : γ), Option.map (g ∘ f) (some val) = some a ↔ (Option.map g ∘ Option.map f) (some val) = some a
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f

Tactic:
ext ⟨⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
a : γ
⊢ Option.map (g ∘ f) none = some a ↔ (Option.map g ∘ Option.map f) none = some a

Tactic:
rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
val : α
a : γ
⊢ Option.map (g ∘ f) (some val) = some a ↔ (Option.map g ∘ Option.map f) (some val) = some a

Tactic:
rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
a : α
s : WSeq α
⊢ a ∈ s → f a ∈ map f s

Tactic:
Seq.mem_map (Option.map f)

Premises used: Option.map, Stream'.WSeq.map, Stream'.Seq.mem_map, Stream'.WSeq.Mem
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
this :
  ∀ (ss : WSeq α),
    a ∈ ss → ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
h : a ∈ S.join
⊢ append nil S.join = S.join

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
this :
  ∀ (ss : WSeq α),
    a ∈ ss → ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
h : a ∈ S.join
⊢ a ∈ append nil S.join

Tactic:
simp [h]
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss :
  ∀ (ss : WSeq α),
    a ∈ ss → ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
⊢ ∀ {S : WSeq (WSeq α)}, a ∈ S.join → ∃ s ∈ S, a ∈ s

Tactic:
suffices
    ∀ ss : WSeq α,
      a ∈ ss → ∀ s S, append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
    from fun S h => (this _ h nil S (by simp) (by simp [h])).resolve_left (notMem_nil _)
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
h1 :
  ∀ (b : α) (s' : WSeq α),
    (a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = s' → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s) →
      ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = cons b s' → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
h2 :
  ∀ (s : WSeq α),
    (∀ (s_1 : WSeq α) (S : WSeq (WSeq α)), s_1.append S.join = s → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s) →
      ∀ (s_1 : WSeq α) (S : WSeq (WSeq α)),
        s_1.append S.join = s.think → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s
⊢ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s

Tactic:
apply mem_rec_on h

Premises used: Stream'.WSeq.mem_rec_on
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
h1 :
  ∀ (b : α) (ss : WSeq α)
    (o :
      a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s)
    (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
h2 :
  ∀ (ss : WSeq α)
    (IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s)
    (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss.think → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
⊢ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s

Tactic:
apply mem_rec_on h <;> [intro b ss o; intro ss IH]

Premises used: Stream'.WSeq.mem_rec_on
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s : WSeq α
S : WSeq (WSeq α)
h1 : append nil S.join = cons b ss → a ∈ append nil S.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S, a ∈ s
h1₁ :
  ∀ (x : α) (s : WSeq α),
    (cons x s).append S.join = cons b ss → a ∈ (cons x s).append S.join → a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
h1₂ : ∀ (s : WSeq α), s.think.append S.join = cons b ss → a ∈ s.think.append S.join → a ∈ s.think ∨ ∃ s ∈ S, a ∈ s
⊢ s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s

Tactic:
induction s using WSeq.recOn
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
h1 :
  append nil (join nil) = cons b ss →
    Membership.mem (γ := WSeq α) (append nil (join nil)) a →
      Membership.mem (γ := WSeq α) nil a ∨ ∃ (s : WSeq α), Membership.mem (γ := WSeq (WSeq α)) nil s ∧ a ∈ s
h1₁ :
  ∀ (x : WSeq α) (s : WSeq (WSeq α)),
    append nil (cons x s).join = cons b ss →
      a ∈ append nil (cons x s).join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1
h1₂ :
  ∀ (s : WSeq (WSeq α)),
    append nil s.think.join = cons b ss →
      a ∈ append nil s.think.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1
⊢ append nil S.join = cons b ss → a ∈ append nil S.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S, a ∈ s

Tactic:
induction S using WSeq.recOn
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s : WSeq α
S : WSeq (WSeq α)
h1 :
  append nil (join nil) = cons b ss →
    Membership.mem (γ := WSeq α) (append nil (join nil)) a →
      Membership.mem (γ := WSeq α) nil a ∨ ∃ (s : WSeq α), Membership.mem (γ := WSeq (WSeq α)) nil s ∧ a ∈ s
h1₁ :
  ∀ (x : WSeq α) (s : WSeq (WSeq α)),
    append nil (cons x s).join = cons b ss →
      a ∈ append nil (cons x s).join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1
h1₂ :
  ∀ (s : WSeq (WSeq α)),
    append nil s.think.join = cons b ss →
      a ∈ append nil s.think.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1
h1₃ :
  ∀ (x : α) (s : WSeq α),
    (cons x s).append S.join = cons b ss → a ∈ (cons x s).append S.join → a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
h1₄ : ∀ (s : WSeq α), s.think.append S.join = cons b ss → a ∈ s.think.append S.join → a ∈ s.think ∨ ∃ s ∈ S, a ∈ s
⊢ s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s

Tactic:
induction s using WSeq.recOn <;>
      [induction S using WSeq.recOn; skip; skip]
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
ej : append nil (join nil) = cons b ss
m : Membership.mem (γ := WSeq α) (append nil (join nil)) a
⊢ nil = cons b ss

Tactic:
simp at ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
x : WSeq α
s : WSeq (WSeq α)
ej : append nil (cons x s).join = cons b ss
m : a ∈ append nil (cons x s).join
⊢ (x.append s.join).think = cons b ss

Tactic:
simp at ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s : WSeq (WSeq α)
ej : append nil s.think.join = cons b ss
m : a ∈ append nil s.think.join
⊢ s.join.think = cons b ss

Tactic:
simp at ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
x : α
s : WSeq α
ej : (cons x s).append S.join = cons b ss
m : a ∈ (cons x s).append S.join
⊢ cons x (s.append S.join) = cons b ss

Tactic:
simp at ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
s : WSeq α
ej : s.think.append S.join = cons b ss
m : a ∈ s.think.append S.join
⊢ (s.append S.join).think = cons b ss

Tactic:
simp at ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
m : Membership.mem (γ := WSeq α) (append nil (join nil)) a
ej : nil = cons b ss
⊢ Seq.destruct nil = Seq.destruct (cons b ss)

Tactic:
have := congr_arg Seq.destruct ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
x : WSeq α
s : WSeq (WSeq α)
m : a ∈ append nil (cons x s).join
ej : (x.append s.join).think = cons b ss
⊢ Seq.destruct (x.append s.join).think = Seq.destruct (cons b ss)

Tactic:
have := congr_arg Seq.destruct ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s : WSeq (WSeq α)
m : a ∈ append nil s.think.join
ej : s.join.think = cons b ss
⊢ Seq.destruct s.join.think = Seq.destruct (cons b ss)

Tactic:
have := congr_arg Seq.destruct ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
x : α
s : WSeq α
m : a ∈ (cons x s).append S.join
ej : cons x (s.append S.join) = cons b ss
⊢ Seq.destruct (cons x (s.append S.join)) = Seq.destruct (cons b ss)

Tactic:
have := congr_arg Seq.destruct ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
s : WSeq α
m : a ∈ s.think.append S.join
ej : (s.append S.join).think = cons b ss
⊢ Seq.destruct (s.append S.join).think = Seq.destruct (cons b ss)

Tactic:
have := congr_arg Seq.destruct ej