α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
h : filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s
have h : filter (fun a => compress u v a ∉ 𝓒 u v s) (𝓒 u v s) = ∅ :=
  filter_false_of_mem fun a ha h => h <| compress_mem_compression_of_mem_compression ha
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
h : filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ filter (fun a => compress u v a ∈ 𝓒 u v s) (𝓒 u v s) ∪
      image (compress u v) (filter ((fun a => ¬a ∈ 𝓒 u v s) ∘ compress u v) (𝓒 u v s)) =
    𝓒 u v s
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
h : filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s
rw [compression, image_filter]
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
h : filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ filter (fun a => compress u v a ∈ 𝓒 u v s) (𝓒 u v s) ∪
      image (compress u v) (filter (fun x => ¬compress u v x ∈ 𝓒 u v s) (𝓒 u v s)) =
    𝓒 u v s
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
h : filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ filter (fun a => compress u v a ∈ 𝓒 u v s) (𝓒 u v s) ∪
      image (compress u v) (filter ((fun a => ¬a ∈ 𝓒 u v s) ∘ compress u v) (𝓒 u v s)) =
    𝓒 u v s
simp_rw [Function.comp]
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
h : filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ filter (fun a => compress u v a ∈ 𝓒 u v s) (𝓒 u v s) ∪ filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = 𝓒 u v s
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
h : filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ filter (fun a => compress u v a ∈ 𝓒 u v s) (𝓒 u v s) ∪
      image (compress u v) (filter (fun x => ¬compress u v x ∈ 𝓒 u v s) (𝓒 u v s)) =
    𝓒 u v s
rw [h, image_empty, ← h]
no goals
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
h : filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ filter (fun a => compress u v a ∈ 𝓒 u v s) (𝓒 u v s) ∪ filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = 𝓒 u v s
exact filter_union_filter_neg_eq _ (compression u v s)