English
For a fixed element a in α, if a belongs to the join of S, then there exists s in S with a ∈ s.
Русский
Для фиксированного a ∈ α, если a принадлежит объединению join S, то существует s ∈ S such that a ∈ s.
LaTeX
$$$$ \\forall a \\in \\alpha,\\forall S : \\mathrm{WSeq}(\\mathrm{WSeq}\\, \\alpha),\\ a \\in \\mathrm{join} S \\Rightarrow \\exists s \\in S, a \\in s $$$$
Lean4
theorem exists_of_mem_join {a : α} : ∀ {S : WSeq (WSeq α)}, a ∈ join S → ∃ s, s ∈ S ∧ a ∈ s :=
by
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 _)
intro ss h; apply mem_rec_on h <;> [intro b ss o; intro ss IH] <;> intro s S
· induction s using WSeq.recOn <;> [induction S using WSeq.recOn; skip; skip] <;> intro ej m <;> simp at ej <;>
have := congr_arg Seq.destruct ej <;> simp at this; cases this
case cons.intro b' s =>
substs b' ss
simp? at m ⊢ says simp only [cons_append, mem_cons_iff] at m ⊢
rcases o with e | IH
· simp [e]
rcases m with e | m
· simp [e]
exact Or.imp_left Or.inr (IH _ _ rfl m)
· induction s using WSeq.recOn <;> [induction S using WSeq.recOn; skip; skip] <;> intro ej m <;> simp at ej <;>
have := congr_arg Seq.destruct ej <;> simp at this <;> subst ss
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
case think S =>
apply Or.inr
replace m : a ∈ S.join := by simpa using m
rcases (IH nil S (by simp) (by simp [m])).resolve_left (notMem_nil _) with ⟨s, sS, as⟩
exact ⟨s, by simp [sS], as⟩
· simp only [think_append, mem_think] at m IH ⊢
apply IH _ _ rfl m
