α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a b u : α
s : Finset α
⊢ filter (fun a => compress u u a ∈ s) s ∪ filter (fun a => ¬a ∈ s) (image (compress u u) s) = 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 : α
s : Finset α
⊢ 𝓒 u u s = s
unfold compression
case h.e'_2.h.e'_3
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a b u : α
s : Finset α
⊢ filter (fun a => compress u u a ∈ s) s = s

case h.e'_2.h.e'_4
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a b u : α
s : Finset α
⊢ filter (fun a => ¬a ∈ s) (image (compress u u) 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 : α
s : Finset α
⊢ filter (fun a => compress u u a ∈ s) s ∪ filter (fun a => ¬a ∈ s) (image (compress u u) s) = s
convert union_empty s
case h.e'_2.h.e'_3.a
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a✝ b u : α
s : Finset α
a : α
⊢ a ∈ filter (fun a => compress u u a ∈ s) s ↔ a ∈ s
case h.e'_2.h.e'_3
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a b u : α
s : Finset α
⊢ filter (fun a => compress u u a ∈ s) s = s
ext a
no goals
case h.e'_2.h.e'_3.a
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a✝ b u : α
s : Finset α
a : α
⊢ a ∈ filter (fun a => compress u u a ∈ s) s ↔ a ∈ s
simp [mem_filter, compress_self, and_self_iff]
case h.e'_2.h.e'_4
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a✝ b u : α
s : Finset α
a : α
ha : a ∈ filter (fun a => ¬a ∈ s) (image (compress u u) s)
⊢ False
case h.e'_2.h.e'_4
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a b u : α
s : Finset α
⊢ filter (fun a => ¬a ∈ s) (image (compress u u) s) = ∅
refine' eq_empty_of_forall_not_mem fun a ha => _
case h.e'_2.h.e'_4
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a✝ b u : α
s : Finset α
a : α
ha : (∃ a_1, a_1 ∈ s ∧ a_1 = a) ∧ ¬a ∈ s
⊢ False
case h.e'_2.h.e'_4
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a✝ b u : α
s : Finset α
a : α
ha : a ∈ filter (fun a => ¬a ∈ s) (image (compress u u) s)
⊢ False
simp_rw [mem_filter, mem_image, compress_self] at ha
case h.e'_2.h.e'_4.intro.intro.intro
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a b✝ u : α
s : Finset α
b : α
hb : b ∈ s
hb' : ¬b ∈ s
⊢ False
case h.e'_2.h.e'_4
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a✝ b u : α
s : Finset α
a : α
ha : (∃ a_1, a_1 ∈ s ∧ a_1 = a) ∧ ¬a ∈ s
⊢ False
obtain ⟨⟨b, hb, rfl⟩, hb'⟩ := ha
no goals
case h.e'_2.h.e'_4.intro.intro.intro
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a b✝ u : α
s : Finset α
b : α
hb : b ∈ s
hb' : ¬b ∈ s
⊢ False
exact hb' hb