α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
⊢ card (filter (fun a => compress u v a ∈ s) s ∪ filter ((fun a => ¬a ∈ s) ∘ compress u v) s) = card s

α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
⊢ Disjoint (filter (fun a => compress u v a ∈ s) s) (filter ((fun a => ¬a ∈ s) ∘ compress 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 u v : α
s : Finset α
⊢ Set.InjOn (compress u v) ↑(filter ((fun a => ¬a ∈ s) ∘ compress 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 u v : α
s : Finset α
⊢ card (𝓒 u v s) = card s
rw [compression, card_disjoint_union (compress_disjoint _ _), image_filter, card_image_of_injOn,
  ← card_disjoint_union]
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
⊢ card (filter (fun a => compress u v a ∈ s) s ∪ filter (fun x => ¬compress u v x ∈ s) s) = card s

α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
⊢ Disjoint (filter (fun a => compress u v a ∈ s) s) (filter ((fun a => ¬a ∈ s) ∘ compress 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 u v : α
s : Finset α
⊢ Set.InjOn (compress u v) ↑(filter ((fun a => ¬a ∈ s) ∘ compress 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 u v : α
s : Finset α
⊢ card (filter (fun a => compress u v a ∈ s) s ∪ filter ((fun a => ¬a ∈ s) ∘ compress u v) s) = card s

α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
⊢ Disjoint (filter (fun a => compress u v a ∈ s) s) (filter ((fun a => ¬a ∈ s) ∘ compress 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 u v : α
s : Finset α
⊢ Set.InjOn (compress u v) ↑(filter ((fun a => ¬a ∈ s) ∘ compress u v) s)
simp_rw [Function.comp]
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
⊢ Disjoint (filter (fun a => compress u v a ∈ s) s) (filter ((fun a => ¬a ∈ s) ∘ compress 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 u v : α
s : Finset α
⊢ Set.InjOn (compress u v) ↑(filter ((fun a => ¬a ∈ s) ∘ compress 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 u v : α
s : Finset α
⊢ card (filter (fun a => compress u v a ∈ s) s ∪ filter (fun x => ¬compress u v x ∈ s) s) = card s

α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
⊢ Disjoint (filter (fun a => compress u v a ∈ s) s) (filter ((fun a => ¬a ∈ s) ∘ compress 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 u v : α
s : Finset α
⊢ Set.InjOn (compress u v) ↑(filter ((fun a => ¬a ∈ s) ∘ compress u v) s)
rw [filter_union_filter_neg_eq]
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a✝ b✝ u v : α
s : Finset α
a : α
ha : a ∈ ↑(filter ((fun a => ¬a ∈ s) ∘ compress u v) s)
b : α
hb : b ∈ ↑(filter ((fun a => ¬a ∈ s) ∘ compress u v) s)
hab : compress u v a = compress u v b
⊢ a = b
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
⊢ Set.InjOn (compress u v) ↑(filter ((fun a => ¬a ∈ s) ∘ compress u v) s)
intro a ha b hb hab
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a✝ b✝ u v : α
s : Finset α
a : α
ha : a ∈ ↑(filter ((fun a => ¬a ∈ s) ∘ compress u v) s)
b : α
hb : b ∈ ↑(filter ((fun a => ¬a ∈ s) ∘ compress u v) s)
hab : compress u v a = compress u v b
⊢ a = b
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a✝ b✝ u v : α
s : Finset α
a : α
ha : a ∈ ↑(filter ((fun a => ¬a ∈ s) ∘ compress u v) s)
b : α
hb : b ∈ ↑(filter ((fun a => ¬a ∈ s) ∘ compress u v) s)
hab : compress u v a = compress u v b
⊢ a = b
dsimp at hab
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a✝ b✝ u v : α
s : Finset α
a : α
ha : a ∈ s ∧ ¬compress u v a ∈ s
b : α
hb : b ∈ s ∧ ¬compress u v b ∈ s
hab : compress u v a = compress u v b
⊢ a = b
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a✝ b✝ u v : α
s : Finset α
a : α
ha : a ∈ ↑(filter ((fun a => ¬a ∈ s) ∘ compress u v) s)
b : α
hb : b ∈ ↑(filter ((fun a => ¬a ∈ s) ∘ compress u v) s)
hab : compress u v a = compress u v b
⊢ a = b
rw [mem_coe, mem_filter, Function.comp_apply] at ha hb
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a✝ b✝ u v : α
s : Finset α
a : α
ha : a ∈ s ∧ ¬(if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ∈ s
b : α
hb : b ∈ s ∧ ¬compress u v b ∈ s
hab : (if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) = compress u v b
⊢ a = b
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a✝ b✝ u v : α
s : Finset α
a : α
ha : a ∈ s ∧ ¬compress u v a ∈ s
b : α
hb : b ∈ s ∧ ¬compress u v b ∈ s
hab : compress u v a = compress u v b
⊢ a = b
rw [compress] at ha hab
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✝ u v : α
s : Finset α
a b : α
hb : b ∈ s ∧ ¬compress u v b ∈ s
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ ¬(a ⊔ u) \ v ∈ s
hab : (a ⊔ u) \ v = compress u v b
⊢ a = b

case inr
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a✝ b✝ u v : α
s : Finset α
a b : α
hb : b ∈ s ∧ ¬compress u v b ∈ s
has : ¬(Disjoint u a ∧ v ≤ a)
ha : a ∈ s ∧ ¬a ∈ s
hab : a = compress u v b
⊢ a = b
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a✝ b✝ u v : α
s : Finset α
a : α
ha : a ∈ s ∧ ¬(if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ∈ s
b : α
hb : b ∈ s ∧ ¬compress u v b ∈ s
hab : (if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) = compress u v b
⊢ a = b
split_ifs at ha hab with has
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
⊢ filter (fun a => compress u v a ∈ s) s ∩ filter ((fun a => ¬a ∈ s) ∘ compress 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 u v : α
s : Finset α
⊢ Disjoint (filter (fun a => compress u v a ∈ s) s) (filter ((fun a => ¬a ∈ s) ∘ compress u v) s)
rw [disjoint_iff_inter_eq_empty]
no goals
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a b u v : α
s : Finset α
⊢ filter (fun a => compress u v a ∈ s) s ∩ filter ((fun a => ¬a ∈ s) ∘ compress u v) s = ∅
exact filter_inter_filter_neg_eq _ _ _
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✝ u v : α
s : Finset α
a b : α
hb : b ∈ s ∧ ¬(if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) ∈ s
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ ¬(a ⊔ u) \ v ∈ s
hab : (a ⊔ u) \ v = if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b
⊢ a = b
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✝ u v : α
s : Finset α
a b : α
hb : b ∈ s ∧ ¬compress u v b ∈ s
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ ¬(a ⊔ u) \ v ∈ s
hab : (a ⊔ u) \ v = compress u v b
⊢ a = b
rw [compress] at hb hab
case inl.inl
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a✝ b✝ u v : α
s : Finset α
a b : α
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ ¬(a ⊔ u) \ v ∈ s
hbs : Disjoint u b ∧ v ≤ b
hb : b ∈ s ∧ ¬(b ⊔ u) \ v ∈ s
hab : (a ⊔ u) \ v = (b ⊔ u) \ v
⊢ a = b

case inl.inr
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a✝ b✝ u v : α
s : Finset α
a b : α
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ ¬(a ⊔ u) \ v ∈ s
hbs : ¬(Disjoint u b ∧ v ≤ b)
hb : b ∈ s ∧ ¬b ∈ s
hab : (a ⊔ u) \ v = b
⊢ a = b
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✝ u v : α
s : Finset α
a b : α
hb : b ∈ s ∧ ¬(if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b) ∈ s
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ ¬(a ⊔ u) \ v ∈ s
hab : (a ⊔ u) \ v = if Disjoint u b ∧ v ≤ b then (b ⊔ u) \ v else b
⊢ a = b
split_ifs at hb hab with hbs
no goals
case inl.inl
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a✝ b✝ u v : α
s : Finset α
a b : α
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ ¬(a ⊔ u) \ v ∈ s
hbs : Disjoint u b ∧ v ≤ b
hb : b ∈ s ∧ ¬(b ⊔ u) \ v ∈ s
hab : (a ⊔ u) \ v = (b ⊔ u) \ v
⊢ a = b
exact sup_sdiff_injOn u v has hbs hab
no goals
case inl.inr
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a✝ b✝ u v : α
s : Finset α
a b : α
has : Disjoint u a ∧ v ≤ a
ha : a ∈ s ∧ ¬(a ⊔ u) \ v ∈ s
hbs : ¬(Disjoint u b ∧ v ≤ b)
hb : b ∈ s ∧ ¬b ∈ s
hab : (a ⊔ u) \ v = b
⊢ a = b
exact (hb.2 hb.1).elim
no goals
case inr
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v✝ a✝ b✝ u v : α
s : Finset α
a b : α
hb : b ∈ s ∧ ¬compress u v b ∈ s
has : ¬(Disjoint u a ∧ v ≤ a)
ha : a ∈ s ∧ ¬a ∈ s
hab : a = compress u v b
⊢ a = b
exact (ha.2 ha.1).elim