[GOAL]
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v : α
⊢ Set.InjOn (fun x => (x ⊔ u) \ v) {x | Disjoint u x ∧ v ≤ x}
[PROOFSTEP]
rintro a ha b hb hab
[GOAL]
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x => (x ⊔ u) \ v) a = (fun x => (x ⊔ u) \ v) b
⊢ a = b
[PROOFSTEP]
have h : ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v :=
  by
  dsimp at hab
  rw [hab]
[GOAL]
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x => (x ⊔ u) \ v) a = (fun x => (x ⊔ u) \ v) b
⊢ ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
[PROOFSTEP]
dsimp at hab
[GOAL]
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (a ⊔ u) \ v = (b ⊔ u) \ v
⊢ ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
[PROOFSTEP]
rw [hab]
[GOAL]
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x => (x ⊔ u) \ v) a = (fun x => (x ⊔ u) \ v) b
h : ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
⊢ a = b
[PROOFSTEP]
rwa [sdiff_sdiff_comm, ha.1.symm.sup_sdiff_cancel_right, sdiff_sdiff_comm, hb.1.symm.sup_sdiff_cancel_right,
  sdiff_sup_cancel ha.2, sdiff_sup_cancel hb.2] at h
[GOAL]
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
hva : Disjoint v a
hua : u ≤ a
⊢ compress u v ((a ⊔ v) \ u) = a
[PROOFSTEP]
rw [compress_of_disjoint_of_le disjoint_sdiff_self_right (le_sdiff.2 ⟨(le_sup_right : v ≤ a ⊔ v), hva.mono_right hua⟩),
  sdiff_sup_cancel (le_sup_of_le_left hua), hva.symm.sup_sdiff_cancel_right]
[GOAL]
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a b : α
⊢ a ∈ 𝓒 u v s ↔ a ∈ s ∧ compress u v a ∈ s ∨ ¬a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = a
[PROOFSTEP]
simp [compression, mem_union, mem_filter, mem_image, and_comm]
[GOAL]
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u✝ v a✝ b u a : α
⊢ compress u u a = a
[PROOFSTEP]
unfold compress
[GOAL]
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u✝ v a✝ b u a : α
⊢ (if Disjoint u a ∧ u ≤ a then (a ⊔ u) \ u else a) = a
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u✝ v a✝ b u a : α
h✝ : Disjoint u a ∧ u ≤ a
⊢ (a ⊔ u) \ u = a
[PROOFSTEP]
exact ‹Disjoint u a ∧ u ≤ a›.1.symm.sup_sdiff_cancel_right
[GOAL]
case neg
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u✝ v a✝ b u a : α
h✝ : ¬(Disjoint u a ∧ u ≤ a)
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a b u : α
s : Finset α
⊢ 𝓒 u u s = s
[PROOFSTEP]
unfold compression
[GOAL]
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a b u : α
s : Finset α
⊢ filter (fun a => compress u u a ∈ s) s ∪ filter (fun a => ¬a ∈ s) (image (compress u u) s) = s
[PROOFSTEP]
convert union_empty s
[GOAL]
case h.e'_2.h.e'_3
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a b u : α
s : Finset α
⊢ filter (fun a => compress u u a ∈ s) s = s
[PROOFSTEP]
ext a
[GOAL]
case h.e'_2.h.e'_3.a
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a✝ b u : α
s : Finset α
a : α
⊢ a ∈ filter (fun a => compress u u a ∈ s) s ↔ a ∈ s
[PROOFSTEP]
simp [mem_filter, compress_self, and_self_iff]
[GOAL]
case h.e'_2.h.e'_4
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a b u : α
s : Finset α
⊢ filter (fun a => ¬a ∈ s) (image (compress u u) s) = ∅
[PROOFSTEP]
refine' eq_empty_of_forall_not_mem fun a ha => _
[GOAL]
case h.e'_2.h.e'_4
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a✝ b u : α
s : Finset α
a : α
ha : a ∈ filter (fun a => ¬a ∈ s) (image (compress u u) s)
⊢ False
[PROOFSTEP]
simp_rw [mem_filter, mem_image, compress_self] at ha
[GOAL]
case h.e'_2.h.e'_4
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s✝ : Finset α
u✝ v a✝ b u : α
s : Finset α
a : α
ha : (∃ a_1, a_1 ∈ s ∧ a_1 = a) ∧ ¬a ∈ s
⊢ False
[PROOFSTEP]
obtain ⟨⟨b, hb, rfl⟩, hb'⟩ := ha
[GOAL]
case h.e'_2.h.e'_4.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✝ u : α
s : Finset α
b : α
hb : b ∈ s
hb' : ¬b ∈ s
⊢ False
[PROOFSTEP]
exact hb' hb
[GOAL]
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a✝ b✝ a b : α
⊢ compress (a \ b) (b \ a) b = a
[PROOFSTEP]
refine' (compress_of_disjoint_of_le disjoint_sdiff_self_left sdiff_le).trans _
[GOAL]
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a✝ b✝ a b : α
⊢ (b ⊔ a \ b) \ (b \ a) = a
[PROOFSTEP]
rw [sup_sdiff_self_right, sup_sdiff, disjoint_sdiff_self_right.sdiff_eq_left, sup_eq_right]
[GOAL]
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
s : Finset α
u v a✝ b✝ a b : α
⊢ b \ (b \ a) ≤ a
[PROOFSTEP]
exact sdiff_sdiff_le
[GOAL]
α : 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 a : α
⊢ compress u v (compress u v a) = compress u v a
[PROOFSTEP]
unfold compress
[GOAL]
α : 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 a : α
⊢ (if
        Disjoint u (if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ∧
          v ≤ if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a then
      ((if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ⊔ u) \ v
    else if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) =
    if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a
[PROOFSTEP]
split_ifs with h h'
[GOAL]
case pos
α : 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 a : α
h : Disjoint u a ∧ v ≤ a
h' : Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v
⊢ ((a ⊔ u) \ v ⊔ u) \ v = (a ⊔ u) \ v
[PROOFSTEP]
try rfl
[GOAL]
case pos
α : 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 a : α
h : Disjoint u a ∧ v ≤ a
h' : Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v
⊢ ((a ⊔ u) \ v ⊔ u) \ v = (a ⊔ u) \ v
[PROOFSTEP]
rfl
[GOAL]
case neg
α : 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 a : α
h : Disjoint u a ∧ v ≤ a
h' : ¬(Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v)
⊢ (a ⊔ u) \ v = (a ⊔ u) \ v
[PROOFSTEP]
try rfl
[GOAL]
case neg
α : 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 a : α
h : Disjoint u a ∧ v ≤ a
h' : ¬(Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v)
⊢ (a ⊔ u) \ v = (a ⊔ u) \ v
[PROOFSTEP]
rfl
[GOAL]
case neg
α : 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 a : α
h : ¬(Disjoint u a ∧ v ≤ a)
⊢ a = a
[PROOFSTEP]
try rfl
[GOAL]
case neg
α : 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 a : α
h : ¬(Disjoint u a ∧ v ≤ a)
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
case pos
α : 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 a : α
h : Disjoint u a ∧ v ≤ a
h' : Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v
⊢ ((a ⊔ u) \ v ⊔ u) \ v = (a ⊔ u) \ v
[PROOFSTEP]
rw [le_sdiff_iff.1 h'.2, sdiff_bot, sdiff_bot, sup_assoc, sup_idem]
[GOAL]
α : 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 ∈ 𝓒 u v s
[PROOFSTEP]
rw [mem_compression]
[GOAL]
α : 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 ∧ compress u v (compress u v a) ∈ s ∨
    ¬compress u v a ∈ s ∧ ∃ b, b ∈ s ∧ compress u v b = compress u v a
[PROOFSTEP]
by_cases h : compress u v a ∈ s
[GOAL]
case pos
α : 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 : compress u v a ∈ s
⊢ 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
[PROOFSTEP]
rw [compress_idem]
[GOAL]
case pos
α : 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 : 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
[PROOFSTEP]
exact Or.inl ⟨h, h⟩
[GOAL]
case neg
α : 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 : ¬compress u v a ∈ s
⊢ 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
[PROOFSTEP]
exact Or.inr ⟨h, a, ha, rfl⟩
[GOAL]
α : 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
[PROOFSTEP]
rw [mem_compression] at ha ⊢
[GOAL]
α : 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
[PROOFSTEP]
simp only [compress_idem, exists_prop]
[GOAL]
α : 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
[PROOFSTEP]
obtain ⟨_, ha⟩ | ⟨_, b, hb, rfl⟩ := ha
[GOAL]
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
[PROOFSTEP]
exact Or.inl ⟨ha, ha⟩
[GOAL]
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)
[PROOFSTEP]
exact Or.inr ⟨by rwa [compress_idem], b, hb, (compress_idem _ _ _).symm⟩
[GOAL]
α : 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
[PROOFSTEP]
rwa [compress_idem]
[GOAL]
α : 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 α
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s
[PROOFSTEP]
have h : filter (fun a => compress u v a ∉ 𝓒 u v s) (𝓒 u v s) = ∅ :=
  filter_false_of_mem fun a ha h => h <| compress_mem_compression_of_mem_compression ha
[GOAL]
α : 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 α
h : filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s
[PROOFSTEP]
rw [compression, image_filter]
[GOAL]
α : 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 α
h : filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ filter (fun a => compress u v a ∈ 𝓒 u v s) (𝓒 u v s) ∪
      image (compress u v) (filter ((fun a => ¬a ∈ 𝓒 u v s) ∘ compress u v) (𝓒 u v s)) =
    𝓒 u v s
[PROOFSTEP]
simp_rw [Function.comp]
[GOAL]
α : 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 α
h : filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ filter (fun a => compress u v a ∈ 𝓒 u v s) (𝓒 u v s) ∪
      image (compress u v) (filter (fun x => ¬compress u v x ∈ 𝓒 u v s) (𝓒 u v s)) =
    𝓒 u v s
[PROOFSTEP]
rw [h, image_empty, ← h]
[GOAL]
α : 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 α
h : filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = ∅
⊢ filter (fun a => compress u v a ∈ 𝓒 u v s) (𝓒 u v s) ∪ filter (fun a => ¬compress u v a ∈ 𝓒 u v s) (𝓒 u v s) = 𝓒 u v s
[PROOFSTEP]
exact filter_union_filter_neg_eq _ (compression u v s)
[GOAL]
α : 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
[PROOFSTEP]
rw [compression, card_disjoint_union (compress_disjoint _ _), image_filter, card_image_of_injOn, ← card_disjoint_union]
[GOAL]
α : 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)
[PROOFSTEP]
simp_rw [Function.comp]
[GOAL]
α : 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)
[PROOFSTEP]
rw [filter_union_filter_neg_eq]
[GOAL]
α : 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)
[PROOFSTEP]
rw [disjoint_iff_inter_eq_empty]
[GOAL]
α : 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 = ∅
[PROOFSTEP]
exact filter_inter_filter_neg_eq _ _ _
[GOAL]
α : 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)
[PROOFSTEP]
intro a ha b hb hab
[GOAL]
α : 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
[PROOFSTEP]
rw [mem_coe, mem_filter, Function.comp_apply] at ha hb
[GOAL]
α : 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
[PROOFSTEP]
rw [compress] at ha hab
[GOAL]
α : 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
[PROOFSTEP]
split_ifs at ha hab  with has
[GOAL]
case pos
α : 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
[PROOFSTEP]
rw [compress] at hb hab
[GOAL]
case pos
α : 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
[PROOFSTEP]
split_ifs at hb hab  with hbs
[GOAL]
case pos
α : 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
[PROOFSTEP]
exact sup_sdiff_injOn u v has hbs hab
[GOAL]
case neg
α : 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
[PROOFSTEP]
exact (hb.2 hb.1).elim
[GOAL]
case neg
α : 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
[PROOFSTEP]
exact (ha.2 ha.1).elim
[GOAL]
α : 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
[PROOFSTEP]
rw [mem_compression] at h
[GOAL]
α : 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
[PROOFSTEP]
obtain h | ⟨-, b, hb, hba⟩ := h
[GOAL]
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
[PROOFSTEP]
cases ha h.1
[GOAL]
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
[PROOFSTEP]
unfold compress at hba
[GOAL]
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
[PROOFSTEP]
split_ifs at hba  with h
[GOAL]
case pos
α : 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
[PROOFSTEP]
rw [← hba, le_sdiff]
[GOAL]
case pos
α : 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
[PROOFSTEP]
exact ⟨le_sup_right, h.1.mono_right h.2⟩
[GOAL]
case neg
α : 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
[PROOFSTEP]
cases ne_of_mem_of_not_mem hb ha hba
[GOAL]
α : 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
⊢ Disjoint v a
[PROOFSTEP]
rw [mem_compression] at h
[GOAL]
α : 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
⊢ Disjoint v a
[PROOFSTEP]
obtain h | ⟨-, b, hb, hba⟩ := h
[GOAL]
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
⊢ Disjoint v a
[PROOFSTEP]
cases ha h.1
[GOAL]
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
⊢ Disjoint v a
[PROOFSTEP]
unfold compress at hba
[GOAL]
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
⊢ Disjoint v a
[PROOFSTEP]
split_ifs at hba
[GOAL]
case pos
α : 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
⊢ Disjoint v a
[PROOFSTEP]
rw [← hba]
[GOAL]
case pos
α : 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
⊢ Disjoint v ((b ⊔ u) \ v)
[PROOFSTEP]
exact disjoint_sdiff_self_right
[GOAL]
case neg
α : 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
⊢ Disjoint v a
[PROOFSTEP]
cases ne_of_mem_of_not_mem hb ha hba
[GOAL]
α : 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
⊢ (a ⊔ v) \ u ∈ s
[PROOFSTEP]
rw [mem_compression] at h
[GOAL]
α : 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
⊢ (a ⊔ v) \ u ∈ s
[PROOFSTEP]
obtain h | ⟨-, b, hb, hba⟩ := h
[GOAL]
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
⊢ (a ⊔ v) \ u ∈ s
[PROOFSTEP]
cases ha h.1
[GOAL]
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
⊢ (a ⊔ v) \ u ∈ s
[PROOFSTEP]
unfold compress at hba
[GOAL]
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
⊢ (a ⊔ v) \ u ∈ s
[PROOFSTEP]
split_ifs at hba  with h
[GOAL]
case pos
α : 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
⊢ (a ⊔ v) \ u ∈ s
[PROOFSTEP]
rwa [← hba, sdiff_sup_cancel (le_sup_of_le_left h.2), sup_sdiff_right_self, h.1.symm.sdiff_eq_left]
[GOAL]
case neg
α : 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
⊢ (a ⊔ v) \ u ∈ s
[PROOFSTEP]
cases ne_of_mem_of_not_mem hb ha hba
[GOAL]
α : 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
[PROOFSTEP]
rw [mem_compression, compress_of_disjoint_of_le hua hva] at ha
[GOAL]
α : 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
[PROOFSTEP]
obtain ⟨_, ha⟩ | ⟨_, b, hb, rfl⟩ := ha
[GOAL]
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
[PROOFSTEP]
exact ha
[GOAL]
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
[PROOFSTEP]
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
[GOAL]
α : 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 = ⊥
[PROOFSTEP]
suffices Disjoint u (u \ v) by rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this
[GOAL]
α : 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 = ⊥
[PROOFSTEP]
rwa [(hua.mono_right hva).sdiff_eq_left, disjoint_self] at this
[GOAL]
α : 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)
[PROOFSTEP]
refine' hua.mono_right _
[GOAL]
α : 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
[PROOFSTEP]
rw [← compress_idem, compress_of_disjoint_of_le hua hva]
[GOAL]
α : 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
[PROOFSTEP]
exact sdiff_le_sdiff_right le_sup_right
[GOAL]
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
[PROOFSTEP]
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
[GOAL]
α : 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 = ⊥
[PROOFSTEP]
rw [← disjoint_self]
[GOAL]
α : 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
[PROOFSTEP]
apply Disjoint.mono_right hva
[GOAL]
α : 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)
[PROOFSTEP]
rw [← compress_idem, compress_of_disjoint_of_le hua hva]
[GOAL]
α : 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)
[PROOFSTEP]
exact disjoint_sdiff_self_right
[GOAL]
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
[PROOFSTEP]
rwa [hu, hv, compress_self, sup_bot_eq, sdiff_bot]
[GOAL]
α : 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
[PROOFSTEP]
rw [mem_compression] at ha
[GOAL]
α : 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
[PROOFSTEP]
obtain ha | ⟨_, b, hb, h⟩ := ha
[GOAL]
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
[PROOFSTEP]
exact ha.1
[GOAL]
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
[PROOFSTEP]
unfold compress at h
[GOAL]
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
[PROOFSTEP]
split_ifs at h
[GOAL]
case pos
α : 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
[PROOFSTEP]
rw [← h, le_sdiff_iff] at hva
[GOAL]
case pos
α : 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
[PROOFSTEP]
rwa [← h, hvu hva, hva, sup_bot_eq, sdiff_bot]
[GOAL]
case neg
α : 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
[PROOFSTEP]
rwa [← h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v a✝ : Finset α
huv : card u = card v
a : Finset α
⊢ card (compress u v a) = card a
[PROOFSTEP]
unfold compress
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v a✝ : Finset α
huv : card u = card v
a : Finset α
⊢ card (if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) = card a
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v a✝ : Finset α
huv : card u = card v
a : Finset α
h : Disjoint u a ∧ v ≤ a
⊢ card ((a ⊔ u) \ v) = card a
[PROOFSTEP]
rw [card_sdiff (h.2.trans le_sup_left), sup_eq_union, card_disjoint_union h.1.symm, huv, add_tsub_cancel_right]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v a✝ : Finset α
huv : card u = card v
a : Finset α
h : ¬(Disjoint u a ∧ v ≤ a)
⊢ card a = card a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v a : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
⊢ v = ∅ → u = ∅
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u a : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ ∅ ∧ IsCompressed (erase u x) (erase ∅ y) 𝒜
⊢ u = ∅
[PROOFSTEP]
refine' eq_empty_of_forall_not_mem fun a ha => _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u a✝ : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ ∅ ∧ IsCompressed (erase u x) (erase ∅ y) 𝒜
a : α
ha : a ∈ u
⊢ False
[PROOFSTEP]
obtain ⟨_, ⟨⟩, -⟩ := huv a ha
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
⊢ ∂ (𝓒 u v 𝒜) ⊆ 𝓒 u v (∂ 𝒜)
[PROOFSTEP]
set 𝒜' := 𝓒 u v 𝒜
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
⊢ ∂ 𝒜' ⊆ 𝓒 u v (∂ 𝒜)
[PROOFSTEP]
suffices H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
⊢ ∂ 𝒜' ⊆ 𝓒 u v (∂ 𝒜)
[PROOFSTEP]
rintro s hs'
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
⊢ s ∈ 𝓒 u v (∂ 𝒜)
[PROOFSTEP]
rw [mem_compression]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ ¬s ∈ ∂ 𝒜 ∧ ∃ b, b ∈ ∂ 𝒜 ∧ compress u v b = s
[PROOFSTEP]
by_cases hs : s ∈ 𝒜.shadow
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ ¬s ∈ ∂ 𝒜 ∧ ∃ b, b ∈ ∂ 𝒜 ∧ compress u v b = s
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : ¬s ∈ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ ¬s ∈ ∂ 𝒜 ∧ ∃ b, b ∈ ∂ 𝒜 ∧ compress u v b = s
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : ¬s ∈ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ ¬s ∈ ∂ 𝒜 ∧ ∃ b, b ∈ ∂ 𝒜 ∧ compress u v b = s
[PROOFSTEP]
obtain ⟨hus, hvs, h, _⟩ := H _ hs' hs
[GOAL]
case neg.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : ¬s ∈ ∂ 𝒜
hus : u ⊆ s
hvs : Disjoint v s
h : (s ∪ v) \ u ∈ ∂ 𝒜
right✝ : ¬(s ∪ v) \ u ∈ ∂ 𝒜'
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ ¬s ∈ ∂ 𝒜 ∧ ∃ b, b ∈ ∂ 𝒜 ∧ compress u v b = s
[PROOFSTEP]
exact Or.inr ⟨hs, _, h, compress_of_disjoint_of_le' hvs hus⟩
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ ¬s ∈ ∂ 𝒜 ∧ ∃ b, b ∈ ∂ 𝒜 ∧ compress u v b = s
[PROOFSTEP]
refine' Or.inl ⟨hs, _⟩
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
⊢ compress u v s ∈ ∂ 𝒜
[PROOFSTEP]
rw [compress]
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
⊢ (if Disjoint u s ∧ v ≤ s then (s ⊔ u) \ v else s) ∈ ∂ 𝒜
[PROOFSTEP]
split_ifs with huvs
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
huvs : Disjoint u s ∧ v ≤ s
⊢ (s ⊔ u) \ v ∈ ∂ 𝒜
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
huvs : ¬(Disjoint u s ∧ v ≤ s)
⊢ s ∈ ∂ 𝒜
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
huvs : ¬(Disjoint u s ∧ v ≤ s)
⊢ s ∈ ∂ 𝒜
[PROOFSTEP]
exact hs
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
huvs : Disjoint u s ∧ v ≤ s
⊢ (s ⊔ u) \ v ∈ ∂ 𝒜
[PROOFSTEP]
rw [mem_shadow_iff] at hs'
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
s : Finset α
hs' : ∃ t, t ∈ 𝒜' ∧ ∃ a, a ∈ t ∧ erase t a = s
hs : s ∈ ∂ 𝒜
huvs : Disjoint u s ∧ v ≤ s
⊢ (s ⊔ u) \ v ∈ ∂ 𝒜
[PROOFSTEP]
obtain ⟨t, Ht, a, hat, rfl⟩ := hs'
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a✝ u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : erase t a ∈ ∂ 𝒜
huvs : Disjoint u (erase t a) ∧ v ≤ erase t a
⊢ (erase t a ⊔ u) \ v ∈ ∂ 𝒜
[PROOFSTEP]
have hav : a ∉ v := not_mem_mono huvs.2 (not_mem_erase a t)
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a✝ u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : erase t a ∈ ∂ 𝒜
huvs : Disjoint u (erase t a) ∧ v ≤ erase t a
hav : ¬a ∈ v
⊢ (erase t a ⊔ u) \ v ∈ ∂ 𝒜
[PROOFSTEP]
have hvt : v ≤ t := huvs.2.trans (erase_subset _ t)
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a✝ u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : erase t a ∈ ∂ 𝒜
huvs : Disjoint u (erase t a) ∧ v ≤ erase t a
hav : ¬a ∈ v
hvt : v ≤ t
⊢ (erase t a ⊔ u) \ v ∈ ∂ 𝒜
[PROOFSTEP]
have ht : t ∈ 𝒜 := mem_of_mem_compression Ht hvt (aux huv)
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a✝ u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : erase t a ∈ ∂ 𝒜
huvs : Disjoint u (erase t a) ∧ v ≤ erase t a
hav : ¬a ∈ v
hvt : v ≤ t
ht : t ∈ 𝒜
⊢ (erase t a ⊔ u) \ v ∈ ∂ 𝒜
[PROOFSTEP]
by_cases hau : a ∈ u
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a✝ u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : erase t a ∈ ∂ 𝒜
huvs : Disjoint u (erase t a) ∧ v ≤ erase t a
hav : ¬a ∈ v
hvt : v ≤ t
ht : t ∈ 𝒜
hau : a ∈ u
⊢ (erase t a ⊔ u) \ v ∈ ∂ 𝒜
[PROOFSTEP]
obtain ⟨b, hbv, Hcomp⟩ := huv a hau
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a✝ u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : erase t a ∈ ∂ 𝒜
huvs : Disjoint u (erase t a) ∧ v ≤ erase t a
hav : ¬a ∈ v
hvt : v ≤ t
ht : t ∈ 𝒜
hau : a ∈ u
b : α
hbv : b ∈ v
Hcomp : IsCompressed (erase u a) (erase v b) 𝒜
⊢ (erase t a ⊔ u) \ v ∈ ∂ 𝒜
[PROOFSTEP]
refine' mem_shadow_iff_insert_mem.2 ⟨b, not_mem_sdiff_of_mem_right hbv, _⟩
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a✝ u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : erase t a ∈ ∂ 𝒜
huvs : Disjoint u (erase t a) ∧ v ≤ erase t a
hav : ¬a ∈ v
hvt : v ≤ t
ht : t ∈ 𝒜
hau : a ∈ u
b : α
hbv : b ∈ v
Hcomp : IsCompressed (erase u a) (erase v b) 𝒜
⊢ insert b ((erase t a ⊔ u) \ v) ∈ 𝒜
[PROOFSTEP]
rw [← Hcomp.eq] at ht
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a✝ u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : erase t a ∈ ∂ 𝒜
huvs : Disjoint u (erase t a) ∧ v ≤ erase t a
hav : ¬a ∈ v
hvt : v ≤ t
hau : a ∈ u
b : α
ht : t ∈ 𝓒 (erase u a) (erase v b) 𝒜
hbv : b ∈ v
Hcomp : IsCompressed (erase u a) (erase v b) 𝒜
⊢ insert b ((erase t a ⊔ u) \ v) ∈ 𝒜
[PROOFSTEP]
have hsb := sup_sdiff_mem_of_mem_compression ht ((erase_subset _ _).trans hvt) (disjoint_erase_comm.2 huvs.1)
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a✝ u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : erase t a ∈ ∂ 𝒜
huvs : Disjoint u (erase t a) ∧ v ≤ erase t a
hav : ¬a ∈ v
hvt : v ≤ t
hau : a ∈ u
b : α
ht : t ∈ 𝓒 (erase u a) (erase v b) 𝒜
hbv : b ∈ v
Hcomp : IsCompressed (erase u a) (erase v b) 𝒜
hsb : (t ⊔ erase u a) \ erase v b ∈ 𝒜
⊢ insert b ((erase t a ⊔ u) \ v) ∈ 𝒜
[PROOFSTEP]
rwa [sup_eq_union, sdiff_erase (mem_union_left _ <| hvt hbv), union_erase_of_mem hat, ← erase_union_of_mem hau] at hsb
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a✝ u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : erase t a ∈ ∂ 𝒜
huvs : Disjoint u (erase t a) ∧ v ≤ erase t a
hav : ¬a ∈ v
hvt : v ≤ t
ht : t ∈ 𝒜
hau : ¬a ∈ u
⊢ (erase t a ⊔ u) \ v ∈ ∂ 𝒜
[PROOFSTEP]
refine'
  mem_shadow_iff.2 ⟨(t ⊔ u) \ v, sup_sdiff_mem_of_mem_compression Ht hvt <| disjoint_of_erase_right hau huvs.1, a, _, _⟩
[GOAL]
case neg.refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a✝ u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : erase t a ∈ ∂ 𝒜
huvs : Disjoint u (erase t a) ∧ v ≤ erase t a
hav : ¬a ∈ v
hvt : v ≤ t
ht : t ∈ 𝒜
hau : ¬a ∈ u
⊢ a ∈ (t ⊔ u) \ v
[PROOFSTEP]
rw [sup_eq_union, mem_sdiff, mem_union]
[GOAL]
case neg.refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a✝ u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : erase t a ∈ ∂ 𝒜
huvs : Disjoint u (erase t a) ∧ v ≤ erase t a
hav : ¬a ∈ v
hvt : v ≤ t
ht : t ∈ 𝒜
hau : ¬a ∈ u
⊢ (a ∈ t ∨ a ∈ u) ∧ ¬a ∈ v
[PROOFSTEP]
exact ⟨Or.inl hat, hav⟩
[GOAL]
case neg.refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a✝ u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : erase t a ∈ ∂ 𝒜
huvs : Disjoint u (erase t a) ∧ v ≤ erase t a
hav : ¬a ∈ v
hvt : v ≤ t
ht : t ∈ 𝒜
hau : ¬a ∈ u
⊢ erase ((t ⊔ u) \ v) a = (erase t a ⊔ u) \ v
[PROOFSTEP]
rw [← erase_sdiff_comm, sup_eq_union, erase_union_distrib, erase_eq_of_not_mem hau]
[GOAL]
case H
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
⊢ ∀ (s : Finset α), s ∈ ∂ 𝒜' → ¬s ∈ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
[PROOFSTEP]
intro s hs𝒜' hs𝒜
[GOAL]
case H
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
[PROOFSTEP]
have m : ∀ y, y ∉ s → insert y s ∉ 𝒜 := fun y h a => hs𝒜 (mem_shadow_iff_insert_mem.2 ⟨y, h, a⟩)
[GOAL]
case H
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
[PROOFSTEP]
obtain ⟨x, _, _⟩ := mem_shadow_iff_insert_mem.1 hs𝒜'
[GOAL]
case H.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
[PROOFSTEP]
have hus : u ⊆ insert x s := le_of_mem_compression_of_not_mem ‹_ ∈ 𝒜'› (m _ ‹x ∉ s›)
[GOAL]
case H.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
[PROOFSTEP]
have hvs : Disjoint v (insert x s) := disjoint_of_mem_compression_of_not_mem ‹_› (m _ ‹x ∉ s›)
[GOAL]
case H.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
[PROOFSTEP]
have : (insert x s ∪ v) \ u ∈ 𝒜 := sup_sdiff_mem_of_mem_compression_of_not_mem ‹_› (m _ ‹x ∉ s›)
[GOAL]
case H.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this : (insert x s ∪ v) \ u ∈ 𝒜
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
[PROOFSTEP]
have hsv : Disjoint s v := hvs.symm.mono_left (subset_insert _ _)
[GOAL]
case H.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
[PROOFSTEP]
have hvu : Disjoint v u := disjoint_of_subset_right hus hvs
[GOAL]
case H.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
[PROOFSTEP]
have hxv : x ∉ v := disjoint_right.1 hvs (mem_insert_self _ _)
[GOAL]
case H.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
[PROOFSTEP]
have : v \ u = v := ‹Disjoint v u›.sdiff_eq_left
[GOAL]
case H.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this : v \ u = v
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
[PROOFSTEP]
have : x ∉ u := by
  intro hxu
  obtain ⟨y, hyv, hxy⟩ := huv x hxu
  apply
    m y
      (disjoint_right.1 hsv hyv)
        -- and we will use this `y` to contradict `m`, so we would like to show `insert y s ∈ 𝒜`.
            -- We do this by showing the below
  have : ((insert x s ∪ v) \ u ∪ erase u x) \ erase v y ∈ 𝒜 :=
    by
    refine'
      sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) _ (disjoint_of_subset_left (erase_subset _ _) disjoint_sdiff)
    rw [union_sdiff_distrib, ‹v \ u = v›]
    exact
      (erase_subset _ _).trans
        (subset_union_right _ _)
          -- and then arguing that it's the same
  convert this using 1
  rw [sdiff_union_erase_cancel (hus.trans <| subset_union_left _ _) ‹x ∈ u›, erase_union_distrib, erase_insert ‹x ∉ s›,
    erase_eq_of_not_mem ‹x ∉ v›, sdiff_erase (mem_union_right _ hyv), union_sdiff_cancel_right hsv]
    -- Now that this is done, it's immediate that `u ⊆ s`
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this : v \ u = v
⊢ ¬x ∈ u
[PROOFSTEP]
intro hxu
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this : v \ u = v
hxu : x ∈ u
⊢ False
[PROOFSTEP]
obtain ⟨y, hyv, hxy⟩ := huv x hxu
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (erase u x) (erase v y) 𝒜
⊢ False
[PROOFSTEP]
apply
  m y
    (disjoint_right.1 hsv hyv)
      -- and we will use this `y` to contradict `m`, so we would like to show `insert y s ∈ 𝒜`.
          -- We do this by showing the below
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (erase u x) (erase v y) 𝒜
⊢ insert y s ∈ 𝒜
[PROOFSTEP]
have : ((insert x s ∪ v) \ u ∪ erase u x) \ erase v y ∈ 𝒜 :=
  by
  refine'
    sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) _ (disjoint_of_subset_left (erase_subset _ _) disjoint_sdiff)
  rw [union_sdiff_distrib, ‹v \ u = v›]
  exact
    (erase_subset _ _).trans
      (subset_union_right _ _)
        -- and then arguing that it's the same
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (erase u x) (erase v y) 𝒜
⊢ ((insert x s ∪ v) \ u ∪ erase u x) \ erase v y ∈ 𝒜
[PROOFSTEP]
refine' sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) _ (disjoint_of_subset_left (erase_subset _ _) disjoint_sdiff)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (erase u x) (erase v y) 𝒜
⊢ (insert x s ∪ v) \ u ∈ 𝓒 (erase u x) (erase v y) 𝒜
[PROOFSTEP]
rwa [hxy.eq]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (erase u x) (erase v y) 𝒜
⊢ erase v y ≤ (insert x s ∪ v) \ u
[PROOFSTEP]
rw [union_sdiff_distrib, ‹v \ u = v›]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (erase u x) (erase v y) 𝒜
⊢ erase v y ≤ insert x s \ u ∪ v
[PROOFSTEP]
exact
  (erase_subset _ _).trans
    (subset_union_right _ _)
      -- and then arguing that it's the same
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝ : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (erase u x) (erase v y) 𝒜
this : ((insert x s ∪ v) \ u ∪ erase u x) \ erase v y ∈ 𝒜
⊢ insert y s ∈ 𝒜
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_4
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝ : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (erase u x) (erase v y) 𝒜
this : ((insert x s ∪ v) \ u ∪ erase u x) \ erase v y ∈ 𝒜
⊢ insert y s = ((insert x s ∪ v) \ u ∪ erase u x) \ erase v y
[PROOFSTEP]
rw [sdiff_union_erase_cancel (hus.trans <| subset_union_left _ _) ‹x ∈ u›, erase_union_distrib, erase_insert ‹x ∉ s›,
  erase_eq_of_not_mem ‹x ∉ v›, sdiff_erase (mem_union_right _ hyv), union_sdiff_cancel_right hsv]
  -- Now that this is done, it's immediate that `u ⊆ s`
[GOAL]
case H.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝ : v \ u = v
this : ¬x ∈ u
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
[PROOFSTEP]
have hus : u ⊆ s := by
  rwa [← erase_eq_of_not_mem ‹x ∉ u›, ← subset_insert_iff]
    -- and we already had that `v` and `s` are disjoint,
      -- so it only remains to get `(s ∪ v) \ u ∈ ∂ 𝒜 \ ∂ 𝒜'`
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝ : v \ u = v
this : ¬x ∈ u
⊢ u ⊆ s
[PROOFSTEP]
rwa [← erase_eq_of_not_mem ‹x ∉ u›, ← subset_insert_iff]
  -- and we already had that `v` and `s` are disjoint,
    -- so it only remains to get `(s ∪ v) \ u ∈ ∂ 𝒜 \ ∂ 𝒜'`
[GOAL]
case H.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝ : v \ u = v
this : ¬x ∈ u
hus : u ⊆ s
⊢ u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ ¬(s ∪ v) \ u ∈ ∂ 𝒜'
[PROOFSTEP]
simp_rw [mem_shadow_iff_insert_mem]
[GOAL]
case H.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝ : v \ u = v
this : ¬x ∈ u
hus : u ⊆ s
⊢ u ⊆ s ∧ Disjoint v s ∧ (∃ a x, insert a ((s ∪ v) \ u) ∈ 𝒜) ∧ ¬∃ a x, insert a ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
[PROOFSTEP]
refine'
  ⟨hus, hsv.symm, ⟨x, _, _⟩, _⟩
    -- `(s ∪ v) \ u ∈ ∂ 𝒜` is pretty direct:
[GOAL]
case H.intro.intro.refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝ : v \ u = v
this : ¬x ∈ u
hus : u ⊆ s
⊢ ¬x ∈ (s ∪ v) \ u
[PROOFSTEP]
exact not_mem_sdiff_of_not_mem_left (not_mem_union.2 ⟨‹x ∉ s›, ‹x ∉ v›⟩)
[GOAL]
case H.intro.intro.refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝ : v \ u = v
this : ¬x ∈ u
hus : u ⊆ s
⊢ insert x ((s ∪ v) \ u) ∈ 𝒜
[PROOFSTEP]
rwa [← insert_sdiff_of_not_mem _ ‹x ∉ u›, ← insert_union]
  -- For (s ∪ v) \ u ∉ ∂ 𝒜', we split up based on w ∈ u
[GOAL]
case H.intro.intro.refine'_3
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝ : v \ u = v
this : ¬x ∈ u
hus : u ⊆ s
⊢ ¬∃ a x, insert a ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
[PROOFSTEP]
rintro ⟨w, hwB, hw𝒜'⟩
[GOAL]
case H.intro.intro.refine'_3.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝ : v \ u = v
this : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : ¬w ∈ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
⊢ False
[PROOFSTEP]
have : v ⊆ insert w ((s ∪ v) \ u) := (subset_sdiff.2 ⟨subset_union_right _ _, hvu⟩).trans (subset_insert _ _)
[GOAL]
case H.intro.intro.refine'_3.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝¹ : v \ u = v
this✝ : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : ¬w ∈ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this : v ⊆ insert w ((s ∪ v) \ u)
⊢ False
[PROOFSTEP]
by_cases hwu : w ∈ u
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝¹ : v \ u = v
this✝ : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : ¬w ∈ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
⊢ False
[PROOFSTEP]
obtain ⟨z, hz, hxy⟩ := huv w hwu
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝¹ : v \ u = v
this✝ : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : ¬w ∈ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (erase u w) (erase v z) 𝒜
⊢ False
[PROOFSTEP]
apply m z (disjoint_right.1 hsv hz)
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝¹ : v \ u = v
this✝ : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : ¬w ∈ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (erase u w) (erase v z) 𝒜
⊢ insert z s ∈ 𝒜
[PROOFSTEP]
have : insert w ((s ∪ v) \ u) ∈ 𝒜 := mem_of_mem_compression hw𝒜' ‹_› (aux huv)
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝³ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝² : v \ u = v
this✝¹ : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : ¬w ∈ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this✝ : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (erase u w) (erase v z) 𝒜
this : insert w ((s ∪ v) \ u) ∈ 𝒜
⊢ insert z s ∈ 𝒜
[PROOFSTEP]
have : (insert w ((s ∪ v) \ u) ∪ erase u w) \ erase v z ∈ 𝒜 :=
  by
  refine' sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ((erase_subset _ _).trans ‹_›) _
  rw [← sdiff_erase (mem_union_left _ <| hus hwu)]
  exact disjoint_sdiff
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝³ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝² : v \ u = v
this✝¹ : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : ¬w ∈ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this✝ : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (erase u w) (erase v z) 𝒜
this : insert w ((s ∪ v) \ u) ∈ 𝒜
⊢ (insert w ((s ∪ v) \ u) ∪ erase u w) \ erase v z ∈ 𝒜
[PROOFSTEP]
refine' sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ((erase_subset _ _).trans ‹_›) _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝³ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝² : v \ u = v
this✝¹ : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : ¬w ∈ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this✝ : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (erase u w) (erase v z) 𝒜
this : insert w ((s ∪ v) \ u) ∈ 𝒜
⊢ insert w ((s ∪ v) \ u) ∈ 𝓒 (erase u w) (erase v z) 𝒜
[PROOFSTEP]
rwa [hxy.eq]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝³ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝² : v \ u = v
this✝¹ : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : ¬w ∈ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this✝ : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (erase u w) (erase v z) 𝒜
this : insert w ((s ∪ v) \ u) ∈ 𝒜
⊢ Disjoint (erase u w) (insert w ((s ∪ v) \ u))
[PROOFSTEP]
rw [← sdiff_erase (mem_union_left _ <| hus hwu)]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝³ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝² : v \ u = v
this✝¹ : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : ¬w ∈ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this✝ : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (erase u w) (erase v z) 𝒜
this : insert w ((s ∪ v) \ u) ∈ 𝒜
⊢ Disjoint (erase u w) ((s ∪ v) \ erase u w)
[PROOFSTEP]
exact disjoint_sdiff
[GOAL]
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝⁴ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝³ : v \ u = v
this✝² : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : ¬w ∈ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this✝¹ : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (erase u w) (erase v z) 𝒜
this✝ : insert w ((s ∪ v) \ u) ∈ 𝒜
this : (insert w ((s ∪ v) \ u) ∪ erase u w) \ erase v z ∈ 𝒜
⊢ insert z s ∈ 𝒜
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_4
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝⁴ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝³ : v \ u = v
this✝² : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : ¬w ∈ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this✝¹ : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∈ u
z : α
hz : z ∈ v
hxy : IsCompressed (erase u w) (erase v z) 𝒜
this✝ : insert w ((s ∪ v) \ u) ∈ 𝒜
this : (insert w ((s ∪ v) \ u) ∪ erase u w) \ erase v z ∈ 𝒜
⊢ insert z s = (insert w ((s ∪ v) \ u) ∪ erase u w) \ erase v z
[PROOFSTEP]
rw [insert_union_comm, insert_erase ‹w ∈ u›, sdiff_union_of_subset (hus.trans $ subset_union_left _ _),
  sdiff_erase (mem_union_right _ ‹z ∈ v›), union_sdiff_cancel_right hsv]
  -- If `w ∉ u`, we contradict `m` again
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝¹ : v \ u = v
this✝ : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : ¬w ∈ (s ∪ v) \ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : ¬w ∈ u
⊢ False
[PROOFSTEP]
rw [mem_sdiff, ← not_imp, Classical.not_not] at hwB
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝¹ : v \ u = v
this✝ : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : w ∈ s ∪ v → w ∈ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : ¬w ∈ u
⊢ False
[PROOFSTEP]
apply m w (hwu ∘ hwB ∘ mem_union_left _)
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝¹ : v \ u = v
this✝ : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : w ∈ s ∪ v → w ∈ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : ¬w ∈ u
⊢ insert w s ∈ 𝒜
[PROOFSTEP]
have : (insert w ((s ∪ v) \ u) ∪ u) \ v ∈ 𝒜 :=
  sup_sdiff_mem_of_mem_compression ‹insert w ((s ∪ v) \ u) ∈ 𝒜'› ‹_› (disjoint_insert_right.2 ⟨‹_›, disjoint_sdiff⟩)
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝³ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝² : v \ u = v
this✝¹ : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : w ∈ s ∪ v → w ∈ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this✝ : v ⊆ insert w ((s ∪ v) \ u)
hwu : ¬w ∈ u
this : (insert w ((s ∪ v) \ u) ∪ u) \ v ∈ 𝒜
⊢ insert w s ∈ 𝒜
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_4
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u✝ v✝ a u v : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ IsCompressed (erase u x) (erase v y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : ¬s ∈ ∂ 𝒜
m : ∀ (y : α), ¬y ∈ s → ¬insert y s ∈ 𝒜
x : α
w✝ : ¬x ∈ s
h✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝³ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : ¬x ∈ v
this✝² : v \ u = v
this✝¹ : ¬x ∈ u
hus : u ⊆ s
w : α
hwB : w ∈ s ∪ v → w ∈ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝓒 u v 𝒜
this✝ : v ⊆ insert w ((s ∪ v) \ u)
hwu : ¬w ∈ u
this : (insert w ((s ∪ v) \ u) ∪ u) \ v ∈ 𝒜
⊢ insert w s = (insert w ((s ∪ v) \ u) ∪ u) \ v
[PROOFSTEP]
rw [insert_union, sdiff_union_of_subset (hus.trans <| subset_union_left _ _),
  insert_sdiff_of_not_mem _ (hwu ∘ hwB ∘ mem_union_right _), union_sdiff_cancel_right hsv]


[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
⊢ dist G u v = 0 ↔ u = v ∨ ¬Reachable G u v
[PROOFSTEP]
simp [dist, Nat.sInf_eq_zero, Reachable]
[GOAL]
V : Type u_1
G : SimpleGraph V
v : V
⊢ dist G v v = 0
[PROOFSTEP]
simp
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
hr : Reachable G u v
⊢ dist G u v = 0 ↔ u = v
[PROOFSTEP]
simp [hr]
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
h : Reachable G u v
hne : u ≠ v
⊢ dist G u v ≠ 0
[PROOFSTEP]
simp [h, hne]
[GOAL]
V : Type u_1
G : SimpleGraph V
hconn : Connected G
u v : V
⊢ dist G u v = 0 ↔ u = v
[PROOFSTEP]
simp [hconn u v]
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
hconn : Connected G
hne : u ≠ v
⊢ dist G u v ≠ 0
[PROOFSTEP]
intro h
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
hconn : Connected G
hne : u ≠ v
h : dist G u v = 0
⊢ False
[PROOFSTEP]
exact False.elim (hne (hconn.dist_eq_zero_iff.mp h))
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬Reachable G u v
⊢ dist G u v = 0
[PROOFSTEP]
simp [h]
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
h : 0 < dist G u v
⊢ Set.Nonempty Set.univ
[PROOFSTEP]
simpa [Set.range_nonempty_iff_nonempty, Set.nonempty_iff_univ_nonempty] using Nat.nonempty_of_pos_sInf h
[GOAL]
V : Type u_1
G : SimpleGraph V
hconn : Connected G
u v w : V
⊢ dist G u w ≤ dist G u v + dist G v w
[PROOFSTEP]
obtain ⟨p, hp⟩ := hconn.exists_walk_of_dist u v
[GOAL]
case intro
V : Type u_1
G : SimpleGraph V
hconn : Connected G
u v w : V
p : Walk G u v
hp : Walk.length p = dist G u v
⊢ dist G u w ≤ dist G u v + dist G v w
[PROOFSTEP]
obtain ⟨q, hq⟩ := hconn.exists_walk_of_dist v w
[GOAL]
case intro.intro
V : Type u_1
G : SimpleGraph V
hconn : Connected G
u v w : V
p : Walk G u v
hp : Walk.length p = dist G u v
q : Walk G v w
hq : Walk.length q = dist G v w
⊢ dist G u w ≤ dist G u v + dist G v w
[PROOFSTEP]
rw [← hp, ← hq, ← Walk.length_append]
[GOAL]
case intro.intro
V : Type u_1
G : SimpleGraph V
hconn : Connected G
u v w : V
p : Walk G u v
hp : Walk.length p = dist G u v
q : Walk G v w
hq : Walk.length q = dist G v w
⊢ dist G u w ≤ Walk.length (Walk.append p q)
[PROOFSTEP]
apply dist_le
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
h : Reachable G u v
⊢ dist G u v ≤ dist G v u
[PROOFSTEP]
obtain ⟨p, hp⟩ := h.symm.exists_walk_of_dist
[GOAL]
case intro
V : Type u_1
G : SimpleGraph V
u v : V
h : Reachable G u v
p : Walk G v u
hp : Walk.length p = dist G v u
⊢ dist G u v ≤ dist G v u
[PROOFSTEP]
rw [← hp, ← Walk.length_reverse]
[GOAL]
case intro
V : Type u_1
G : SimpleGraph V
u v : V
h : Reachable G u v
p : Walk G v u
hp : Walk.length p = dist G v u
⊢ dist G u v ≤ Walk.length (Walk.reverse p)
[PROOFSTEP]
apply dist_le
[GOAL]
V : Type u_1
G : SimpleGraph V
u v : V
⊢ dist G u v = dist G v u
[PROOFSTEP]
by_cases h : G.Reachable u v
[GOAL]
case pos
V : Type u_1
G : SimpleGraph V
u v : V
h : Reachable G u v
⊢ dist G u v = dist G v u
[PROOFSTEP]
apply le_antisymm (dist_comm_aux h) (dist_comm_aux h.symm)
[GOAL]
case neg
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬Reachable G u v
⊢ dist G u v = dist G v u
[PROOFSTEP]
have h' : ¬G.Reachable v u := fun h' => absurd h'.symm h
[GOAL]
case neg
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬Reachable G u v
h' : ¬Reachable G v u
⊢ dist G u v = dist G v u
[PROOFSTEP]
simp [h, h', dist_eq_zero_of_not_reachable]