-- Mathlib/Data/Seq/WSeq.lean
theorem exists_of_mem_join {a : α} : ∀ {S : WSeq (WSeq α)}, a ∈ join S → ∃ s, s ∈ S ∧ a ∈ s

Proof state:
α : Type u
a : α
⊢ ∀ {S : WSeq (WSeq α)}, a ∈ S.join → ∃ s, 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 (not_mem_nil _)

Result:
α : Type u
a : α
⊢ ∀ (ss : WSeq α),
    a ∈ ss → ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s

Proof state:
α : 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 ∈ S_1 ∧ a ∈ s
ej : S.join.think = S.join.think
m : a ∈ S.join
s : WSeq α
sS : s ∈ S
as : a ∈ s
⊢ s ∈ S.think

Tactic:
simp [sS]

Result:
no goals

Proof state:
case h1.h2.intro.inr.inr
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
ej : cons b (s.append S.join) = cons b (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 ∈ S_1 ∧ a ∈ s
m : a ∈ s.append S.join
⊢ (a = b ∨ a ∈ s) ∨ ∃ s, s ∈ S ∧ a ∈ s

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

Result:
no goals

Proof state:
case h1.h2.intro
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
m : a ∈ (cons b s).append S.join
o :
  a = b ∨
    ∀ (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 ∈ S_1 ∧ a ∈ s
ej : cons b (s.append S.join) = cons b (s.append S.join)
⊢ a ∈ cons b s ∨ ∃ s, s ∈ S ∧ a ∈ s

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

Result:
case h1.h2.intro
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
o :
  a = b ∨
    ∀ (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 ∈ S_1 ∧ a ∈ s
ej : cons b (s.append S.join) = cons b (s.append S.join)
m : a = b ∨ a ∈ s.append S.join
⊢ (a = b ∨ a ∈ s) ∨ ∃ s, s ∈ S ∧ a ∈ s

Proof state:
case h2.h1.h3.h
α : 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 ∈ S_1 ∧ a ∈ s
ej : S.join.think = S.join.think
m : a ∈ S.join
⊢ ∃ s, s ∈ S.think ∧ a ∈ s

Tactic:
rcases (IH nil S (by simp) (by simp [m])).resolve_left (not_mem_nil _) with ⟨s, sS, as⟩

Result:
case h2.h1.h3.h.intro.intro
α : 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 ∈ S_1 ∧ a ∈ s
ej : S.join.think = S.join.think
m : a ∈ S.join
s : WSeq α
sS : s ∈ S
as : a ∈ s
⊢ ∃ s, s ∈ S.think ∧ a ∈ s

Proof state:
case h1.h2.intro.inl
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
ej : cons b (s.append S.join) = cons b (s.append S.join)
m : a = b ∨ a ∈ s.append S.join
e : a = b
⊢ (a = b ∨ a ∈ s) ∨ ∃ s, s ∈ S ∧ a ∈ s

Tactic:
simp [e]

Result:
no goals

Proof state:
case h2.h3
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
s : WSeq α
m : a ∈ s.think.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 ∈ S_1 ∧ a ∈ s
ej : (s.append S.join).think = (s.append S.join).think
⊢ a ∈ s.think ∨ ∃ s, s ∈ S ∧ a ∈ s

Tactic:
simp only [think_append, mem_think] at m IH ⊢

Result:
case h2.h3
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
s : 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 ∈ S_1 ∧ a ∈ s
ej : (s.append S.join).think = (s.append S.join).think
m : a ∈ s.append S.join
⊢ a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s

Proof state:
case h2.h1.h2.h.inr.intro.intro
α : 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 ∈ S_1 ∧ a ∈ s
ej : (s.append S.join).think = (s.append S.join).think
m : a ∈ s.append S.join
s' : WSeq α
sS : s' ∈ S
as : a ∈ s'
⊢ ∃ s_1, (s_1 = s ∨ s_1 ∈ S) ∧ a ∈ s_1

Tactic:
exact ⟨s', Or.inr sS, as⟩

Result:
no goals

Proof state:
α : Type u
a : α
⊢ ∀ (ss : WSeq α),
    a ∈ ss → ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s

Tactic:
intro ss h

Result:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
⊢ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s

Proof state:
case h2.h1.h3.h
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
m : a ∈ nil.append 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 ∈ S_1 ∧ a ∈ s
ej : S.join.think = S.join.think
⊢ ∃ s, s ∈ S.think ∧ a ∈ s

Tactic:
simp? at m says simp only [join_think, nil_append, mem_think] at m

Result:
case h2.h1.h3.h
α : 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 ∈ S_1 ∧ a ∈ s
ej : S.join.think = S.join.think
m : a ∈ S.join
⊢ ∃ s, s ∈ S.think ∧ a ∈ s

Proof state:
case h1
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
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 ∈ S ∧ a ∈ s
s : WSeq α
S : WSeq (WSeq α)
⊢ s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s

Tactic:
induction' s using WSeq.recOn with b' s s <;>
  [induction' S using WSeq.recOn with s S S; skip; skip] <;>
  intro ej m <;> simp at ej <;> have := congr_arg Seq.destruct ej <;>
  simp at this

Result:
case h1.h2
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
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 ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
b' : α
s : WSeq α
m : a ∈ (cons b' s).append S.join
ej : cons b' (s.append S.join) = cons b ss
this : b' = b ∧ s.append S.join = ss
⊢ a ∈ cons b' s ∨ ∃ s, s ∈ S ∧ a ∈ s

Proof state:
case h1.h2
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
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 ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
b' : α
s : WSeq α
m : a ∈ (cons b' s).append S.join
ej : cons b' (s.append S.join) = cons b ss
this : b' = b ∧ s.append S.join = ss
⊢ a ∈ cons b' s ∨ ∃ s, s ∈ S ∧ a ∈ s

Tactic:
cases this

Result:
case h1.h2.intro
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
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 ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
b' : α
s : WSeq α
m : a ∈ (cons b' s).append S.join
ej : cons b' (s.append S.join) = cons b ss
left✝ : b' = b
right✝ : s.append S.join = ss
⊢ a ∈ cons b' s ∨ ∃ s, s ∈ S ∧ a ∈ s

Proof state:
case h2.h1.h3.h.intro.intro
α : 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 ∈ S_1 ∧ a ∈ s
ej : S.join.think = S.join.think
m : a ∈ S.join
s : WSeq α
sS : s ∈ S
as : a ∈ s
⊢ ∃ s, s ∈ S.think ∧ a ∈ s

Tactic:
exact ⟨s, by simp [sS], as⟩

Result:
no goals