awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : Seq.destruct nil = Seq.destruct (cons b ss)
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ (s : WSeq α), Membership.mem (γ := WSeq (WSeq α)) nil s ∧ a ∈ s

Tactic:
simp at this
-- 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
this : Seq.destruct (x.append s.join).think = Seq.destruct (cons b ss)
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1

Tactic:
simp at this
-- 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
this : Seq.destruct s.join.think = Seq.destruct (cons b ss)
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1

Tactic:
simp at this
-- 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
this : Seq.destruct (cons x (s.append S.join)) = Seq.destruct (cons b ss)
⊢ x = b ∧ s.append S.join = ss

Tactic:
simp at this
-- 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
this : Seq.destruct (s.append S.join).think = Seq.destruct (cons b ss)
⊢ a ∈ s.think ∨ ∃ s ∈ S, a ∈ s

Tactic:
simp at this
-- 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
this : x = b ∧ s.append S.join = ss
⊢ x = b

Tactic:
cases this
-- 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
this : x = b ∧ s.append S.join = ss
left : x = b
⊢ s.append S.join = ss

Tactic:
cases this
-- 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_1 : WSeq α
m : a ∈ (cons x s_1).append S.join
ej : cons x (s_1.append S.join) = cons b ss
b' : x = b
s : s_1.append S.join = ss
⊢ a = x ∨
    ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
      s.append S_1.join = s_1.append S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s

Tactic:
substs b' ss
-- 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_1 : WSeq α
m : a ∈ (cons x s_1).append S.join
ej : cons x (s_1.append S.join) = cons b ss
b' : x = b
s : s_1.append S.join = ss
o₁ :
  a = x ∨
    ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
      s.append S_1.join = s_1.append S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
⊢ cons x (s_1.append S.join) = cons x (s_1.append S.join)

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

Tactic:
simp only [cons_append, mem_cons_iff] at m ⊢

Premises used: Stream'.WSeq.cons_append, Stream'.WSeq.mem_cons_iff
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x : α
s : WSeq α
m : a ∈ (cons x s).append S.join
o :
  a = x ∨
    ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
      s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
ej : cons x (s.append S.join) = cons x (s.append S.join)
simp? : ∀ (m : a = x ∨ a ∈ s.append S.join), (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
⊢ a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s

Tactic:
simp? at m ⊢ says simp only [cons_append, mem_cons_iff] at m ⊢

Premises used: Stream'.WSeq.cons_append, Stream'.WSeq.mem_cons_iff
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x : α
s : WSeq α
o :
  a = x ∨
    ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
      s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
ej : cons x (s.append S.join) = cons x (s.append S.join)
m : a = x ∨ a ∈ s.append S.join
inl : ∀ (e : a = x), (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
inr :
  ∀
    (IH :
      ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
        s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s),
    (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
⊢ (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s

Tactic:
rcases o with e | IH
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x : α
s : WSeq α
ej : cons x (s.append S.join) = cons x (s.append S.join)
m : a = x ∨ a ∈ s.append S.join
e : a = x
⊢ (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s

Tactic:
simp [e]
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x : α
s : WSeq α
ej : cons x (s.append S.join) = cons x (s.append S.join)
m : a = x ∨ a ∈ s.append S.join
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
inr : ∀ (e : a = x), (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
inr₁ : ∀ (m : a ∈ s.append S.join), (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
⊢ (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s

Tactic:
rcases m with e | m
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x : α
s : WSeq α
ej : cons x (s.append S.join) = cons x (s.append S.join)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
e : a = x
⊢ (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s

Tactic:
simp [e]
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x : α
s : WSeq α
ej : cons x (s.append S.join) = cons x (s.append S.join)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
m : a ∈ s.append S.join
⊢ (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s

Tactic:
Or.imp_left Or.inr (IH _ _ rfl m)

Premises used: Or.imp_left, Or.inr, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x : α
s : WSeq α
ej : cons x (s.append S.join) = cons x (s.append S.join)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
m : a ∈ s.append S.join
⊢ (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s

Tactic:
exact Or.imp_left Or.inr (IH _ _ rfl m)

Premises used: Or.imp_left, Or.inr, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 α)
h2 : append nil S.join = ss.think → a ∈ append nil S.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S, a ∈ s
h2₁ :
  ∀ (x : α) (s : WSeq α),
    (cons x s).append S.join = ss.think → a ∈ (cons x s).append S.join → a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
h2₂ : ∀ (s : WSeq α), s.think.append S.join = ss.think → a ∈ s.think.append S.join → a ∈ s.think ∨ ∃ s ∈ S, a ∈ s
⊢ s.append S.join = ss.think → 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
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 (WSeq α)
h2 :
  append nil (join nil) = ss.think →
    Membership.mem (γ := WSeq α) (append nil (join nil)) a →
      Membership.mem (γ := WSeq α) nil a ∨ ∃ (s : WSeq α), Membership.mem (γ := WSeq (WSeq α)) nil s ∧ a ∈ s
h2₁ :
  ∀ (x : WSeq α) (s : WSeq (WSeq α)),
    append nil (cons x s).join = ss.think →
      a ∈ append nil (cons x s).join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1
h2₂ :
  ∀ (s : WSeq (WSeq α)),
    append nil s.think.join = ss.think →
      a ∈ append nil s.think.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1
⊢ append nil S.join = ss.think → 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
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 α)
h2 :
  append nil (join nil) = ss.think →
    Membership.mem (γ := WSeq α) (append nil (join nil)) a →
      Membership.mem (γ := WSeq α) nil a ∨ ∃ (s : WSeq α), Membership.mem (γ := WSeq (WSeq α)) nil s ∧ a ∈ s
h2₁ :
  ∀ (x : WSeq α) (s : WSeq (WSeq α)),
    append nil (cons x s).join = ss.think →
      a ∈ append nil (cons x s).join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1
h2₂ :
  ∀ (s : WSeq (WSeq α)),
    append nil s.think.join = ss.think →
      a ∈ append nil s.think.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1
h2₃ :
  ∀ (x : α) (s : WSeq α),
    (cons x s).append S.join = ss.think → a ∈ (cons x s).append S.join → a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
h2₄ : ∀ (s : WSeq α), s.think.append S.join = ss.think → a ∈ s.think.append S.join → a ∈ s.think ∨ ∃ s ∈ S, a ∈ s
⊢ s.append S.join = ss.think → 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
ss : WSeq α
IH : ∀ (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) = ss.think
m : Membership.mem (γ := WSeq α) (append nil (join nil)) a
⊢ nil = ss.think

Tactic:
simp at ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
ss : WSeq α
IH : ∀ (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 = ss.think
m : a ∈ append nil (cons x s).join
⊢ (x.append s.join).think = ss.think

Tactic:
simp at ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
ej : append nil s.think.join = ss.think
m : a ∈ append nil s.think.join
⊢ s.join.think = ss.think

Tactic:
simp at ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
x : α
s : WSeq α
ej : (cons x s).append S.join = ss.think
m : a ∈ (cons x s).append S.join
⊢ cons x (s.append S.join) = ss.think

Tactic:
simp at ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
s : WSeq α
ej : s.think.append S.join = ss.think
m : a ∈ s.think.append S.join
⊢ (s.append S.join).think = ss.think

Tactic:
simp at ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
ss : WSeq α
IH : ∀ (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 = ss.think
⊢ Seq.destruct nil = Seq.destruct ss.think

Tactic:
have := congr_arg Seq.destruct ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
ss : WSeq α
IH : ∀ (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 = ss.think
⊢ Seq.destruct (x.append s.join).think = Seq.destruct ss.think

Tactic:
have := congr_arg Seq.destruct ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
m : a ∈ append nil s.think.join
ej : s.join.think = ss.think
⊢ Seq.destruct s.join.think = Seq.destruct ss.think

Tactic:
have := congr_arg Seq.destruct ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
x : α
s : WSeq α
m : a ∈ (cons x s).append S.join
ej : cons x (s.append S.join) = ss.think
⊢ Seq.destruct (cons x (s.append S.join)) = Seq.destruct ss.think

Tactic:
have := congr_arg Seq.destruct ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
s : WSeq α
m : a ∈ s.think.append S.join
ej : (s.append S.join).think = ss.think
⊢ Seq.destruct (s.append S.join).think = Seq.destruct ss.think

Tactic:
have := congr_arg Seq.destruct ej
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
ss : WSeq α
IH : ∀ (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 = ss.think
this : Seq.destruct nil = Seq.destruct ss.think
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ (s : WSeq α), Membership.mem (γ := WSeq (WSeq α)) nil s ∧ a ∈ s

Tactic:
simp at this
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
ss : WSeq α
IH : ∀ (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 = ss.think
this : Seq.destruct (x.append s.join).think = Seq.destruct ss.think
⊢ x.append s.join = ss

Tactic:
simp at this
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
m : a ∈ append nil s.think.join
ej : s.join.think = ss.think
this : Seq.destruct s.join.think = Seq.destruct ss.think
⊢ s.join = ss

Tactic:
simp at this
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
x : α
s : WSeq α
m : a ∈ (cons x s).append S.join
ej : cons x (s.append S.join) = ss.think
this : Seq.destruct (cons x (s.append S.join)) = Seq.destruct ss.think
⊢ a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s

Tactic:
simp at this
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
s : WSeq α
m : a ∈ s.think.append S.join
ej : (s.append S.join).think = ss.think
this : Seq.destruct (s.append S.join).think = Seq.destruct ss.think
⊢ s.append S.join = ss

Tactic:
simp at this
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
ss : WSeq α
IH : ∀ (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 = ss.think
this : x.append s.join = ss
⊢ ∀ (s_1 : WSeq α) (S : WSeq (WSeq α)),
    s_1.append S.join = x.append s.join → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s

Tactic:
subst ss
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
ss : WSeq α
IH : ∀ (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 = ss.think
this : x.append s.join = ss
IH₁ :
  ∀ (s_1 : WSeq α) (S : WSeq (WSeq α)),
    s_1.append S.join = x.append s.join → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s
⊢ (x.append s.join).think = (x.append s.join).think

Tactic:
subst ss
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
m : a ∈ append nil s.think.join
ej : s.join.think = ss.think
this : s.join = ss
⊢ ∀ (s_1 : WSeq α) (S : WSeq (WSeq α)), s_1.append S.join = s.join → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s

Tactic:
subst ss
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
m : a ∈ append nil s.think.join
ej : s.join.think = ss.think
this : s.join = ss
IH₁ :
  ∀ (s_1 : WSeq α) (S : WSeq (WSeq α)), s_1.append S.join = s.join → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s
⊢ s.join.think = s.join.think

Tactic:
subst ss
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
s : WSeq α
m : a ∈ s.think.append S.join
ej : (s.append S.join).think = ss.think
this : s.append S.join = ss
⊢ ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s

Tactic:
subst ss
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
s : WSeq α
m : a ∈ s.think.append S.join
ej : (s.append S.join).think = ss.think
this : s.append S.join = ss
IH₁ :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
⊢ (s.append S.join).think = (s.append S.join).think

Tactic:
subst ss
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
m : a ∈ append nil (cons s S).join
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
ej : (s.append S.join).think = (s.append S.join).think
h₁ : ∃ s_1 ∈ cons s S, a ∈ s_1
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons s S, a ∈ s_1

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
m : a ∈ append nil (cons s S).join
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
ej : (s.append S.join).think = (s.append S.join).think
h₁ : ∀ (m : a ∈ s.append S.join), a ∈ s ∨ ∃ a_1 ∈ S, a ∈ a_1
⊢ ∃ s_1 ∈ cons s S, a ∈ s_1

Tactic:
simp only [join_cons, nil_append, mem_think, mem_cons_iff, exists_eq_or_imp] at m ⊢

Premises used: exists_eq_or_imp, Stream'.WSeq.join_cons, Stream'.WSeq.nil_append, Stream'.WSeq.mem_cons_iff, Stream'.WSeq.mem_think
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
ej : (s.append S.join).think = (s.append S.join).think
m : a ∈ s.append S.join
⊢ a ∈ s ∨ ∃ a_1 ∈ S, a ∈ a_1

Tactic:
IH s S rfl m

Premises used: rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
ej : (s.append S.join).think = (s.append S.join).think
m : a ∈ s.append S.join
⊢ a ∈ s ∨ ∃ a_1 ∈ S, a ∈ a_1

Tactic:
exact IH s S rfl m

Premises used: rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
x : WSeq α
s : WSeq (WSeq α)
m : a ∈ append nil (cons x s).join
IH :
  ∀ (s_1 : WSeq α) (S : WSeq (WSeq α)),
    s_1.append S.join = x.append s.join → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s
ej : (x.append s.join).think = (x.append s.join).think
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1

Tactic:
case cons s S =>
      apply Or.inr
      simp only [join_cons, nil_append, mem_think, mem_cons_iff, exists_eq_or_imp] at m ⊢
      exact IH s S rfl m

Premises used: Stream'.WSeq.cons, exists_eq_or_imp, Stream'.WSeq.join_cons, Stream'.WSeq.nil_append, Stream'.WSeq.mem_cons_iff, Stream'.WSeq.mem_think, Or.inr
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
m : a ∈ append nil S.think.join
IH : ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)), s.append S_1.join = S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
ej : S.join.think = S.join.think
h₁ : ∃ s ∈ S.think, a ∈ s
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S.think, a ∈ s

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
m : a ∈ append nil S.think.join
IH : ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)), s.append S_1.join = S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
ej : S.join.think = S.join.think
⊢ a ∈ S.join

Tactic:
simpa using m
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
m : a ∈ append nil S.think.join
IH : ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)), s.append S_1.join = S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
ej : S.join.think = S.join.think
⊢ a ∈ S.join

Tactic:
replace m : a ∈ S.join := by simpa using m
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
IH : ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)), s.append S_1.join = S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
ej : S.join.think = S.join.think
m : a ∈ S.join
⊢ append nil S.join = S.join

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

Tactic:
simp [m]