α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
h : a ∈ s ∧ compress u v a ∈ s ∨ ¬a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = a
ha : ¬a ∈ s
⊢ u ≤ a
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
h : a ∈ 𝓒 u v s
ha : ¬a ∈ s
⊢ u ≤ a
rw [mem_compression] at h
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 : α
ha : ¬a ∈ s
h : a ∈ s ∧ compress u v a ∈ s
⊢ u ≤ 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 a b✝ : α
ha : ¬a ∈ s
b : α
hb : b ∈ s
hba : compress u v b = a
⊢ u ≤ a
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
h : a ∈ s ∧ compress u v a ∈ s ∨ ¬a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = a
ha : ¬a ∈ s
⊢ u ≤ a
obtain h | ⟨-, b, hb, hba⟩ := h
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✝ : α
ha : ¬a ∈ s
b : α
hb : b ∈ s
hba : (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) = a
⊢ u ≤ 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 a b✝ : α
ha : ¬a ∈ s
b : α
hb : b ∈ s
hba : compress u v b = a
⊢ u ≤ a
unfold compress at hba
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✝ : α
ha : ¬a ∈ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ u ≤ a

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✝ : α
ha : ¬a ∈ s
b : α
hb : b ∈ s
h : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ u ≤ 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 a b✝ : α
ha : ¬a ∈ s
b : α
hb : b ∈ s
hba : (if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) = a
⊢ u ≤ a
split_ifs at hba with 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 : α
ha : ¬a ∈ s
h : a ∈ s ∧ compress u v a ∈ s
⊢ u ≤ a
cases ha h.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✝ : α
ha : ¬a ∈ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ u ≤ b ⊔ u ∧ Disjoint u v
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✝ : α
ha : ¬a ∈ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ u ≤ a
rw [← hba, le_sdiff]
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✝ : α
ha : ¬a ∈ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ u ≤ b ⊔ u ∧ Disjoint u v
exact ⟨le_sup_right, h.1.mono_right h.2⟩
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✝ : α
ha : ¬a ∈ s
b : α
hb : b ∈ s
h : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ u ≤ a
cases ne_of_mem_of_not_mem hb ha hba