rwa [z, union_empty] at uA
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜) ≠ 𝒜
q : ∀ Q ∈ filter (fun A => compress U V A ∉ 𝒜) 𝒜, compress U V Q ≠ Q
uA : filter (fun A => compress U V A ∈ 𝒜) 𝒜 ∪ filter (fun A => compress U V A ∉ 𝒜) 𝒜 = 𝒜
z : filter (fun A => compress U V A ∉ 𝒜) 𝒜 = ∅
⊢ filter (fun x => compress U V x ∈ 𝒜) 𝒜 = 𝒜
no goals