α : 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 ∧ (a ⊔ u) \ v ∈ s ∨ ¬a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = a
hva : v ≤ a
hua : Disjoint u a
⊢ (a ⊔ u) \ v ∈ 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
hua : Disjoint u a
⊢ (a ⊔ u) \ v ∈ s
rw [mem_compression, compress_of_disjoint_of_le hua hva] at ha
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 : α
hva : v ≤ a
hua : Disjoint u a
left✝ : a ∈ s
ha : (a ⊔ u) \ v ∈ s
⊢ (a ⊔ u) \ v ∈ 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 b✝ b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
⊢ (compress u v b ⊔ u) \ v ∈ 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 ∧ (a ⊔ u) \ v ∈ s ∨ ¬a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = a
hva : v ≤ a
hua : Disjoint u a
⊢ (a ⊔ u) \ v ∈ s
obtain ⟨_, ha⟩ | ⟨_, b, hb, rfl⟩ := 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 b✝ b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
hu : u = ⊥
⊢ (compress u v b ⊔ u) \ v ∈ 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 b✝ b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
⊢ (compress u v b ⊔ u) \ v ∈ s
have hu : u = ⊥ := by
  suffices Disjoint u (u \ v) by rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this
  refine' hua.mono_right _
  rw [← compress_idem, compress_of_disjoint_of_le hua hva]
  exact sdiff_le_sdiff_right le_sup_right
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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
hu : u = ⊥
hv : v = ⊥
⊢ (compress u v b ⊔ u) \ v ∈ 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 b✝ b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
hu : u = ⊥
⊢ (compress u v b ⊔ u) \ v ∈ s
have hv : v = ⊥ := by
  rw [← disjoint_self]
  apply Disjoint.mono_right hva
  rw [← compress_idem, compress_of_disjoint_of_le hua hva]
  exact disjoint_sdiff_self_right
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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
hu : u = ⊥
hv : v = ⊥
⊢ (compress u v b ⊔ u) \ v ∈ s
rwa [hu, hv, compress_self, sup_bot_eq, sdiff_bot]
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 : α
hva : v ≤ a
hua : Disjoint u a
left✝ : a ∈ s
ha : (a ⊔ u) \ v ∈ s
⊢ (a ⊔ u) \ v ∈ s
exact ha
α : 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
⊢ Disjoint u (u \ v)
α : 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
⊢ u = ⊥
suffices Disjoint u (u \ v) by rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this
α : 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
⊢ 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 b✝ b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
⊢ Disjoint u (u \ v)
refine' hua.mono_right _
α : 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
⊢ u \ v ≤ (compress u v b ⊔ u) \ v
α : 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
⊢ u \ v ≤ compress u v b
rw [← compress_idem, compress_of_disjoint_of_le hua hva]
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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
⊢ u \ v ≤ (compress u v b ⊔ u) \ v
exact sdiff_le_sdiff_right le_sup_right
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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
this : Disjoint u (u \ v)
⊢ u = ⊥
rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this
α : 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
hu : u = ⊥
⊢ Disjoint v v
α : 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
hu : u = ⊥
⊢ v = ⊥
rw [← disjoint_self]
α : 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
hu : u = ⊥
⊢ Disjoint 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 b✝ b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
hu : u = ⊥
⊢ Disjoint v v
apply Disjoint.mono_right hva
α : 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
hu : u = ⊥
⊢ Disjoint v ((compress u v b ⊔ u) \ v)
α : 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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
hu : u = ⊥
⊢ Disjoint v (compress u v b)
rw [← compress_idem, compress_of_disjoint_of_le hua hva]
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
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : ¬compress u v b ∈ s
hu : u = ⊥
⊢ Disjoint v ((compress u v b ⊔ u) \ v)
exact disjoint_sdiff_self_right