rw [compression] at a ⊢
α : 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 : 𝓒 U V 𝒜 ≠ 𝒜
⊢ Finset.UV.familyMeasure (𝓒 U V 𝒜) < Finset.UV.familyMeasure 𝒜
α : 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) 𝒜) ≠ 𝒜
⊢ Finset.UV.familyMeasure (filter (fun x => compress U V x ∈ 𝒜) 𝒜 ∪ filter (fun x => x ∉ 𝒜) (image (compress U V) 𝒜)) <
    Finset.UV.familyMeasure 𝒜