α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
ha : a ∈ s
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨
    ¬compress u v a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = compress u v a
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
ha : a ∈ s
⊢ compress u v a ∈ 𝓒 u v s
rw [mem_compression]
case pos
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
ha : a ∈ s
h : compress u v a ∈ s
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨
    ¬compress u v a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = compress u v a

case neg
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
ha : a ∈ s
h : ¬compress u v a ∈ s
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨
    ¬compress u v a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = compress u v a
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
ha : a ∈ s
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨
    ¬compress u v a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = compress u v a
by_cases h : compress u v a ∈ s
case pos
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
ha : a ∈ s
h : compress u v a ∈ s
⊢ compress u v a ∈ s ∧ compress u v a ∈ s ∨ ¬compress u v a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = compress u v a
case pos
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
ha : a ∈ s
h : compress u v a ∈ s
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨
    ¬compress u v a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = compress u v a
rw [compress_idem]
no goals
case pos
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
ha : a ∈ s
h : compress u v a ∈ s
⊢ compress u v a ∈ s ∧ compress u v a ∈ s ∨ ¬compress u v a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = compress u v a
exact Or.inl ⟨h, h⟩
no goals
case neg
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
ha : a ∈ s
h : ¬compress u v a ∈ s
⊢ compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨
    ¬compress u v a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = compress u v a
exact Or.inr ⟨h, a, ha, rfl⟩