English
If an element a is a member of the concatenation append s1 s2, then a is a member of s1 or a member of s2.
Русский
Если элемент a принадлежит конкатенации append s1 s2, то он принадлежит либо s1, либо s2.
LaTeX
$$$\forall {s_1 s_2 : Seq \alpha} \; a \in append s_1 s_2 \Rightarrow a \in s_1 \lor a \in s_2$$$
Lean4
theorem of_mem_append {s₁ s₂ : Seq α} {a : α} (h : a ∈ append s₁ s₂) : a ∈ s₁ ∨ a ∈ s₂ :=
by
have := h; revert this
generalize e : append s₁ s₂ = ss; intro h; revert s₁
apply mem_rec_on h _
intro b s' o s₁
cases s₁ with
| nil =>
intro m _
apply Or.inr
simpa using m
| cons c t₁ =>
intro m e
have this := congr_arg destruct e
rcases show a = c ∨ a ∈ append t₁ s₂ by simpa using m with e' | m
· rw [e']
exact Or.inl (mem_cons _ _)
· obtain ⟨i1, i2⟩ := show c = b ∧ append t₁ s₂ = s' by simpa
rcases o with e' | IH
· simp [i1, e']
· exact Or.imp_left (mem_cons_of_mem _) (IH m i2)
