α : 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 ∨ ¬a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = a
⊢ 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 ∈ 𝓒 u v s
⊢ compress u v a ∈ 𝓒 u v s
rw [mem_compression] at ha⊢
α : 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 ∨ ¬a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = a
⊢ 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
α : 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 ∨ ¬a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = a
⊢ 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
simp only [compress_idem, exists_prop]
case inl.intro
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
left✝ : a ∈ s
ha : 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 inr.intro.intro.intro
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v b✝ b : α
hb : b ∈ s
left✝ : ¬compress u v b ∈ s
⊢ compress u v (compress u v b) ∈ s ∧ compress u v (compress u v b) ∈ s ∨
    ¬compress u v (compress u v b) ∈ s ∧ ∃ b_1, b_1 ∈ s ∧ compress u v b_1 = compress u v (compress u v b)
α : 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 ∨ ¬a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = a
⊢ 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
obtain ⟨_, ha⟩ | ⟨_, b, hb, rfl⟩ := ha
no goals
case inl.intro
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
left✝ : a ∈ s
ha : 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 ⟨ha, ha⟩
no goals
case inr.intro.intro.intro
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v b✝ b : α
hb : b ∈ s
left✝ : ¬compress u v b ∈ s
⊢ compress u v (compress u v b) ∈ s ∧ compress u v (compress u v b) ∈ s ∨
    ¬compress u v (compress u v b) ∈ s ∧ ∃ b_1, b_1 ∈ s ∧ compress u v b_1 = compress u v (compress u v b)
exact Or.inr ⟨by rwa [compress_idem], b, hb, (compress_idem _ _ _).symm⟩
no goals
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v b✝ b : α
hb : b ∈ s
left✝ : ¬compress u v b ∈ s
⊢ ¬compress u v (compress u v b) ∈ s
rwa [compress_idem]