α : Type u
β : Type v
γ : Type w
a : α
⊢ ∀ (ss : WSeq α),
    a ∈ ss →
      ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
α : Type u
β : Type v
γ : Type w
a : α
⊢ ∀ {S : WSeq (WSeq α)}, a ∈ join S → ∃ s, s ∈ S ∧ a ∈ s
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 _)
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
⊢ ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
α : Type u
β : Type v
γ : Type w
a : α
⊢ ∀ (ss : WSeq α),
    a ∈ ss →
      ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
intro ss h
case h1
α : Type u
β : Type v
γ : Type w
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o :
  a = b ∨
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
s : WSeq α
S : WSeq (WSeq α)
⊢ append s (join S) = cons b ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s

case h2
α : Type u
β : Type v
γ : Type w
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
s : WSeq α
S : WSeq (WSeq α)
⊢ append s (join S) = think ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
⊢ ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
apply mem_rec_on h <;> [intro b ss o; intro ss IH] <;> intro s S
no goals
α : Type u
β : Type v
γ : Type w
a : α
this :
  ∀ (ss : WSeq α),
    a ∈ ss →
      ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
h : a ∈ join S
⊢ append nil (join S) = join S
simp
no goals
α : Type u
β : Type v
γ : Type w
a : α
this :
  ∀ (ss : WSeq α),
    a ∈ ss →
      ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
h : a ∈ join S
⊢ a ∈ append nil (join S)
simp [h]
case h1.h2
α : Type u
β : Type v
γ : Type w
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o :
  a = b ∨
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
b' : α
s : WSeq α
m : a ∈ append (cons b' s) (join S)
ej : cons b' (append s (join S)) = cons b ss
this : b' = b ∧ append s (join S) = ss
⊢ a ∈ cons b' s ∨ ∃ s, s ∈ S ∧ a ∈ s
case h1
α : Type u
β : Type v
γ : Type w
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o :
  a = b ∨
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
s : WSeq α
S : WSeq (WSeq α)
⊢ append s (join S) = cons b ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
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
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o :
  a = b ∨
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
b' : α
s : WSeq α
m : a ∈ append (cons b' s) (join S)
ej : cons b' (append s (join S)) = cons b ss
left✝ : b' = b
right✝ : append s (join S) = ss
⊢ a ∈ cons b' s ∨ ∃ s, s ∈ S ∧ a ∈ s
case h1.h2
α : Type u
β : Type v
γ : Type w
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o :
  a = b ∨
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
b' : α
s : WSeq α
m : a ∈ append (cons b' s) (join S)
ej : cons b' (append s (join S)) = cons b ss
this : b' = b ∧ append s (join S) = ss
⊢ a ∈ cons b' s ∨ ∃ s, s ∈ S ∧ a ∈ s
try cases this; try contradiction
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
m : a ∈ append (cons b s) (join S)
o :
  a = b ∨
    ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
      append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : cons b (append s (join S)) = cons b (append s (join S))
⊢ a ∈ cons b s ∨ ∃ s, s ∈ S ∧ a ∈ s
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o :
  a = b ∨
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
b' : α
s : WSeq α
m : a ∈ append (cons b' s) (join S)
ej : cons b' (append s (join S)) = cons b ss
left✝ : b' = b
right✝ : append s (join S) = ss
⊢ a ∈ cons b' s ∨ ∃ s, s ∈ S ∧ a ∈ s
substs b' ss
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
o :
  a = b ∨
    ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
      append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : cons b (append s (join S)) = cons b (append s (join S))
m : a = b ∨ a ∈ append s (join S)
⊢ (a = b ∨ a ∈ s) ∨ ∃ s, s ∈ S ∧ a ∈ s
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
m : a ∈ append (cons b s) (join S)
o :
  a = b ∨
    ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
      append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : cons b (append s (join S)) = cons b (append s (join S))
⊢ a ∈ cons b s ∨ ∃ s, s ∈ S ∧ a ∈ s
simp at m⊢
case h1.h2.intro.inl
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
ej : cons b (append s (join S)) = cons b (append s (join S))
m : a = b ∨ a ∈ append s (join S)
e : a = b
⊢ (a = b ∨ a ∈ s) ∨ ∃ s, s ∈ S ∧ a ∈ s

case h1.h2.intro.inr
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
ej : cons b (append s (join S)) = cons b (append s (join S))
m : a = b ∨ a ∈ append s (join S)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
⊢ (a = b ∨ a ∈ s) ∨ ∃ s, s ∈ S ∧ a ∈ s
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
o :
  a = b ∨
    ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
      append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : cons b (append s (join S)) = cons b (append s (join S))
m : a = b ∨ a ∈ append s (join S)
⊢ (a = b ∨ a ∈ s) ∨ ∃ s, s ∈ S ∧ a ∈ s
cases' o with e IH
case h1.h2.intro.inr.inl
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
ej : cons b (append s (join S)) = cons b (append s (join S))
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
e : a = b
⊢ (a = b ∨ a ∈ s) ∨ ∃ s, s ∈ S ∧ a ∈ s

case h1.h2.intro.inr.inr
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
ej : cons b (append s (join S)) = cons b (append s (join S))
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
m : a ∈ append s (join S)
⊢ (a = b ∨ a ∈ s) ∨ ∃ s, s ∈ S ∧ a ∈ s
case h1.h2.intro.inr
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
ej : cons b (append s (join S)) = cons b (append s (join S))
m : a = b ∨ a ∈ append s (join S)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
⊢ (a = b ∨ a ∈ s) ∨ ∃ s, s ∈ S ∧ a ∈ s
cases' m with e m
no goals
case h1.h2.intro.inr.inr
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
ej : cons b (append s (join S)) = cons b (append s (join S))
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
m : a ∈ append s (join S)
⊢ (a = b ∨ a ∈ s) ∨ ∃ s, s ∈ S ∧ a ∈ s
exact Or.imp_left Or.inr (IH _ _ rfl m)
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o :
  a = b ∨
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
b' : α
s : WSeq α
m : a ∈ append (cons b' s) (join S)
ej : cons b' (append s (join S)) = cons b ss
left✝ : b' = b
right✝ : append s (join S) = ss
⊢ a ∈ cons b' s ∨ ∃ s, s ∈ S ∧ a ∈ s
case h1.h2
α : Type u
β : Type v
γ : Type w
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o :
  a = b ∨
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
b' : α
s : WSeq α
m : a ∈ append (cons b' s) (join S)
ej : cons b' (append s (join S)) = cons b ss
this : b' = b ∧ append s (join S) = ss
⊢ a ∈ cons b' s ∨ ∃ s, s ∈ S ∧ a ∈ s
cases this
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o :
  a = b ∨
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
b' : α
s : WSeq α
m : a ∈ append (cons b' s) (join S)
ej : cons b' (append s (join S)) = cons b ss
left✝ : b' = b
right✝ : append s (join S) = ss
⊢ a ∈ cons b' s ∨ ∃ s, s ∈ S ∧ a ∈ s
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o :
  a = b ∨
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
b' : α
s : WSeq α
m : a ∈ append (cons b' s) (join S)
ej : cons b' (append s (join S)) = cons b ss
left✝ : b' = b
right✝ : append s (join S) = ss
⊢ a ∈ cons b' s ∨ ∃ s, s ∈ S ∧ a ∈ s
try contradiction
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o :
  a = b ∨
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
b' : α
s : WSeq α
m : a ∈ append (cons b' s) (join S)
ej : cons b' (append s (join S)) = cons b ss
left✝ : b' = b
right✝ : append s (join S) = ss
⊢ a ∈ cons b' s ∨ ∃ s, s ∈ S ∧ a ∈ s
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o :
  a = b ∨
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
S : WSeq (WSeq α)
b' : α
s : WSeq α
m : a ∈ append (cons b' s) (join S)
ej : cons b' (append s (join S)) = cons b ss
left✝ : b' = b
right✝ : append s (join S) = ss
⊢ a ∈ cons b' s ∨ ∃ s, s ∈ S ∧ a ∈ s
contradiction
no goals
case h1.h2.intro.inl
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
ej : cons b (append s (join S)) = cons b (append s (join S))
m : a = b ∨ a ∈ append s (join S)
e : a = b
⊢ (a = b ∨ a ∈ s) ∨ ∃ s, s ∈ S ∧ a ∈ s
simp [e]
no goals
case h1.h2.intro.inr.inl
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
b : α
S : WSeq (WSeq α)
s : WSeq α
ej : cons b (append s (join S)) = cons b (append s (join S))
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
e : a = b
⊢ (a = b ∨ a ∈ s) ∨ ∃ s, s ∈ S ∧ a ∈ s
simp [e]
case h2.h1.h2
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
m : a ∈ append nil (join (cons s S))
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
⊢ a ∈ nil ∨ ∃ s_1, s_1 ∈ cons s S ∧ a ∈ s_1

case h2.h1.h3
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
m : a ∈ append nil (join (think S))
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    append s (join S_1) = join S → a ∈ append s (join S_1) → a ∈ s ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (join S) = think (join S)
⊢ a ∈ nil ∨ ∃ s, s ∈ think S ∧ a ∈ s

case h2.h3
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
s : WSeq α
m : a ∈ append (think s) (join S)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
⊢ a ∈ think s ∨ ∃ s, s ∈ S ∧ a ∈ s
case h2
α : Type u
β : Type v
γ : Type w
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
s : WSeq α
S : WSeq (WSeq α)
⊢ append s (join S) = think ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
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 <;>
  try { try { have := this.1 }; contradiction } <;> subst ss
case h2.h1.h2.h
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
m : a ∈ append nil (join (cons s S))
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
⊢ ∃ s_1, s_1 ∈ cons s S ∧ a ∈ s_1
case h2.h1.h2
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
m : a ∈ append nil (join (cons s S))
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
⊢ a ∈ nil ∨ ∃ s_1, s_1 ∈ cons s S ∧ a ∈ s_1
apply Or.inr
case h2.h1.h2.h
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
m : a ∈ append s (join S)
⊢ ∃ s_1, (s_1 = s ∨ s_1 ∈ S) ∧ a ∈ s_1
case h2.h1.h2.h
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
m : a ∈ append nil (join (cons s S))
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
⊢ ∃ s_1, s_1 ∈ cons s S ∧ a ∈ s_1
simp [-exists_eq_or_imp] at m ⊢
case h2.h1.h2.h.inl
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
m : a ∈ append s (join S)
as : a ∈ s
⊢ ∃ s_1, (s_1 = s ∨ s_1 ∈ S) ∧ a ∈ s_1

case h2.h1.h2.h.inr
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
m : a ∈ append s (join S)
ex : ∃ s, s ∈ S ∧ a ∈ s
⊢ ∃ s_1, (s_1 = s ∨ s_1 ∈ S) ∧ a ∈ s_1
case h2.h1.h2.h
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
m : a ∈ append s (join S)
⊢ ∃ s_1, (s_1 = s ∨ s_1 ∈ S) ∧ a ∈ s_1
cases' IH s S rfl m with as ex
no goals
case h2.h1.h2.h.inl
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
m : a ∈ append s (join S)
as : a ∈ s
⊢ ∃ s_1, (s_1 = s ∨ s_1 ∈ S) ∧ a ∈ s_1
exact ⟨s, Or.inl rfl, as⟩
case h2.h1.h2.h.inr.intro.intro
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
m : a ∈ append s (join S)
s' : WSeq α
sS : s' ∈ S
as : a ∈ s'
⊢ ∃ s_1, (s_1 = s ∨ s_1 ∈ S) ∧ a ∈ s_1
case h2.h1.h2.h.inr
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
m : a ∈ append s (join S)
ex : ∃ s, s ∈ S ∧ a ∈ s
⊢ ∃ s_1, (s_1 = s ∨ s_1 ∈ S) ∧ a ∈ s_1
rcases ex with ⟨s', sS, as⟩
no goals
case h2.h1.h2.h.inr.intro.intro
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
m : a ∈ append s (join S)
s' : WSeq α
sS : s' ∈ S
as : a ∈ s'
⊢ ∃ s_1, (s_1 = s ∨ s_1 ∈ S) ∧ a ∈ s_1
exact ⟨s', Or.inr sS, as⟩
case h2.h1.h3.h
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
m : a ∈ append nil (join (think S))
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    append s (join S_1) = join S → a ∈ append s (join S_1) → a ∈ s ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (join S) = think (join S)
⊢ ∃ s, s ∈ think S ∧ a ∈ s
case h2.h1.h3
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
m : a ∈ append nil (join (think S))
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    append s (join S_1) = join S → a ∈ append s (join S_1) → a ∈ s ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (join S) = think (join S)
⊢ a ∈ nil ∨ ∃ s, s ∈ think S ∧ a ∈ s
apply Or.inr
case h2.h1.h3.h
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    append s (join S_1) = join S → a ∈ append s (join S_1) → a ∈ s ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (join S) = think (join S)
m : a ∈ join S
⊢ ∃ s, s ∈ think S ∧ a ∈ s
case h2.h1.h3.h
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
m : a ∈ append nil (join (think S))
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    append s (join S_1) = join S → a ∈ append s (join S_1) → a ∈ s ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (join S) = think (join S)
⊢ ∃ s, s ∈ think S ∧ a ∈ s
simp at m
case h2.h1.h3.h.intro.intro
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    append s (join S_1) = join S → a ∈ append s (join S_1) → a ∈ s ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (join S) = think (join S)
m : a ∈ join S
s : WSeq α
sS : s ∈ S
as : a ∈ s
⊢ ∃ s, s ∈ think S ∧ a ∈ s
case h2.h1.h3.h
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    append s (join S_1) = join S → a ∈ append s (join S_1) → a ∈ s ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (join S) = think (join S)
m : a ∈ join S
⊢ ∃ s, s ∈ think S ∧ a ∈ s
rcases (IH nil S (by simp) (by simp [m])).resolve_left (not_mem_nil _) with ⟨s, sS, as⟩
no goals
case h2.h1.h3.h.intro.intro
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    append s (join S_1) = join S → a ∈ append s (join S_1) → a ∈ s ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (join S) = think (join S)
m : a ∈ join S
s : WSeq α
sS : s ∈ S
as : a ∈ s
⊢ ∃ s, s ∈ think S ∧ a ∈ s
exact ⟨s, by simp [sS], as⟩
no goals
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    append s (join S_1) = join S → a ∈ append s (join S_1) → a ∈ s ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (join S) = think (join S)
m : a ∈ join S
⊢ append nil (join S) = join S
simp
no goals
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    append s (join S_1) = join S → a ∈ append s (join S_1) → a ∈ s ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (join S) = think (join S)
m : a ∈ join S
⊢ a ∈ append nil (join S)
simp [m]
no goals
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
IH :
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    append s (join S_1) = join S → a ∈ append s (join S_1) → a ∈ s ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (join S) = think (join S)
m : a ∈ join S
s : WSeq α
sS : s ∈ S
as : a ∈ s
⊢ s ∈ think S
simp [sS]
case h2.h3
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
s : WSeq α
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
m : a ∈ append s (join S)
⊢ a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
case h2.h3
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
s : WSeq α
m : a ∈ append (think s) (join S)
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
⊢ a ∈ think s ∨ ∃ s, s ∈ S ∧ a ∈ s
simp at m IH⊢
no goals
case h2.h3
α : Type u
β : Type v
γ : Type w
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
s : WSeq α
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    append s_1 (join S_1) = append s (join S) → a ∈ append s_1 (join S_1) → a ∈ s_1 ∨ ∃ s, s ∈ S_1 ∧ a ∈ s
ej : think (append s (join S)) = think (append s (join S))
m : a ∈ append s (join S)
⊢ a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
apply IH _ _ rfl m