English
For a finite set s and sets t1,t2 with s ⊆ t1 ∪ t2, there exist finite s1,s2 such that s1 ∪ s2 = s, with ↑s1 ⊆ t1 and ↑s2 ⊆ t2 \\ t1.
Русский
Для конечного множества s и множеств t1,t2 при условии s ⊆ t1 ∪ t2 существуют конечные s1,s2 такие, что s1 ∪ s2 = s, и ↑s1 ⊆ t1, ↑s2 ⊆ t2 \\ t1.
LaTeX
$$$\\exists s_1,s_2 : Finset\\ α,\\ s_1 \\cup s_2 = s\\;\\wedge\\;\\uparrow s_1 \\subseteq t_1 \\;\\wedge\\; \\uparrow s_2 \\subseteq t_2 \\setminus t_1,$\n given $s$ and $t_1,t_2$ with $\\uparrow s \\subseteq t_1 \\cup t_2$.$$
Lean4
theorem subset_union_elim {s : Finset α} {t₁ t₂ : Set α} (h : ↑s ⊆ t₁ ∪ t₂) :
∃ s₁ s₂ : Finset α, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁ := by
classical
refine ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩
· grind
· grind
· intro x
simp only [coe_filter, Set.mem_setOf_eq, Set.mem_diff, and_imp]
intro hx hx₂
exact
⟨Or.resolve_left (h hx) hx₂, hx₂⟩
-- This is not a good simp lemma, as it would prevent `Finset.mem_filter` from firing
-- on, e.g. `x ∈ s.filter (Eq b)`.
