α : 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
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
⊢ a ∈ s
α : 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
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
⊢ a ∈ s
rw [mem_compression] at ha
case inl
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
ha : a ∈ s ∧ compress u v a ∈ s
⊢ a ∈ s

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 a b✝ : α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : ¬a ∈ s
b : α
hb : b ∈ s
h : compress u v b = a
⊢ a ∈ s
α : 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
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
⊢ a ∈ s
obtain ha | ⟨_, b, hb, h⟩ := ha
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 a b✝ : α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : ¬a ∈ s
b : α
hb : b ∈ s
h : (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) = a
⊢ a ∈ s
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 a b✝ : α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : ¬a ∈ s
b : α
hb : b ∈ s
h : compress u v b = a
⊢ a ∈ s
unfold compress at h
case inr.intro.intro.intro.inl
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b✝ : α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : ¬a ∈ s
b : α
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ a ∈ s

case inr.intro.intro.intro.inr
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b✝ : α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : ¬a ∈ s
b : α
hb : b ∈ s
h✝ : ¬(Disjoint u b ∧ v ≤ b)
h : b = a
⊢ a ∈ s
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 a b✝ : α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : ¬a ∈ s
b : α
hb : b ∈ s
h : (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) = a
⊢ a ∈ s
split_ifs at h
no goals
case inl
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
ha : a ∈ s ∧ compress u v a ∈ s
⊢ a ∈ s
exact ha.1
case inr.intro.intro.intro.inl
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b✝ : α
hvu : v = ⊥ → u = ⊥
left✝ : ¬a ∈ s
b : α
hva : v = ⊥
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ a ∈ s
case inr.intro.intro.intro.inl
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b✝ : α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : ¬a ∈ s
b : α
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ a ∈ s
rw [← h, le_sdiff_iff] at hva
no goals
case inr.intro.intro.intro.inl
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b✝ : α
hvu : v = ⊥ → u = ⊥
left✝ : ¬a ∈ s
b : α
hva : v = ⊥
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ a ∈ s
rwa [← h, hvu hva, hva, sup_bot_eq, sdiff_bot]
no goals
case inr.intro.intro.intro.inr
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b✝ : α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : ¬a ∈ s
b : α
hb : b ∈ s
h✝ : ¬(Disjoint u b ∧ v ≤ b)
h : b = a
⊢ a ∈ s
rwa [← h]