English
If t1 and t2 are disjoint, then the intersection of a list l with the concatenation t1 ++ t2 is a permutation of the concatenation of the intersections l ∩ t1 and l ∩ t2.
Русский
Если t1 и t2 не имеют общих элементов, то пересечение списка l с конкатенацией t1 и t2 перестановочно эквивалентно конкатенации пересечений l ∩ t1 и l ∩ t2.
LaTeX
$$$\operatorname{Disjoint}(t_1,t_2) \Rightarrow l \cap (t_1 ++ t_2) \sim (l \cap t_1) ++ (l \cap t_2)$$$
Lean4
theorem inter_append {l t₁ t₂ : List α} (h : Disjoint t₁ t₂) : l ∩ (t₁ ++ t₂) ~ l ∩ t₁ ++ l ∩ t₂ := by
induction l with
| nil => simp
| cons x xs l_ih =>
by_cases h₁ : x ∈ t₁
· have h₂ : x ∉ t₂ := h h₁
simp [*]
by_cases h₂ : x ∈ t₂
· simp only [*, inter_cons_of_notMem, false_or, mem_append, inter_cons_of_mem, not_false_iff]
refine Perm.trans (Perm.cons _ l_ih) ?_
change [x] ++ xs ∩ t₁ ++ xs ∩ t₂ ~ xs ∩ t₁ ++ ([x] ++ xs ∩ t₂)
rw [← List.append_assoc]
solve_by_elim [Perm.append_right, perm_append_comm]
· simp [*]
