α : 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 ((∂ ) 𝒜)
α : 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 ((∂ ) 𝒜)
set 𝒜' := 𝓒 u v 𝒜
α : 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 ((∂ ) 𝒜)

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 ∈ (∂ ) 𝒜'
α : 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 ((∂ ) 𝒜)
suffices H : ∀ s ∈ (∂ ) 𝒜',
    s ∉ (∂ ) 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ (∂ ) 𝒜 ∧ (s ∪ v) \ u ∉ (∂ ) 𝒜'
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 ∈ (∂ ) 𝒜'
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 ∈ (∂ ) 𝒜'
intro s hs𝒜' hs𝒜
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 ∈ (∂ ) 𝒜'
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 ∈ (∂ ) 𝒜'
have m : ∀ y, y ∉ s → insert y s ∉ 𝒜 := fun y h a => hs𝒜 (mem_shadow_iff_insert_mem.2 ⟨y, h, a⟩)
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 ∈ (∂ ) 𝒜'
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 ∈ (∂ ) 𝒜'
obtain ⟨x, _, _⟩ := mem_shadow_iff_insert_mem.1 hs𝒜'
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 ∈ (∂ ) 𝒜'
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 ∈ (∂ ) 𝒜'
have hus : u ⊆ insert x s := le_of_mem_compression_of_not_mem ‹_ ∈ 𝒜'› (m _ ‹x ∉ s›)
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 ∈ (∂ ) 𝒜'
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 ∈ (∂ ) 𝒜'
have hvs : Disjoint v (insert x s) := disjoint_of_mem_compression_of_not_mem ‹_› (m _ ‹x ∉ s›)
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 ∈ (∂ ) 𝒜'
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 ∈ (∂ ) 𝒜'
have : (insert x s ∪ v) \ u ∈ 𝒜 := sup_sdiff_mem_of_mem_compression_of_not_mem ‹_› (m _ ‹x ∉ s›)
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 ∈ (∂ ) 𝒜'
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 ∈ (∂ ) 𝒜'
have hsv : Disjoint s v := hvs.symm.mono_left (subset_insert _ _)
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 ∈ (∂ ) 𝒜'
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 ∈ (∂ ) 𝒜'
have hvu : Disjoint v u := disjoint_of_subset_right hus hvs
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 ∈ (∂ ) 𝒜'
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 ∈ (∂ ) 𝒜'
have hxv : x ∉ v := disjoint_right.1 hvs (mem_insert_self _ _)
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 ∈ (∂ ) 𝒜'
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 ∈ (∂ ) 𝒜'
have : v \ u = v := ‹Disjoint v u›.sdiff_eq_left
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 ∈ (∂ ) 𝒜'
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 ∈ (∂ ) 𝒜'
have : x ∉ u := by
  intro hxu
  obtain ⟨y, hyv, hxy⟩ := huv x hxu
  apply m y (disjoint_right.1 hsv hyv)
  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 _ _)
  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]
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 ∈ (∂ ) 𝒜'
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 ∈ (∂ ) 𝒜'
have hus : u ⊆ s := by rwa [← erase_eq_of_not_mem ‹x ∉ u›, ← subset_insert_iff]
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 𝒜
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 ∈ (∂ ) 𝒜'
simp_rw [mem_shadow_iff_insert_mem]
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

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) ∈ 𝒜

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 𝒜
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 𝒜
refine' ⟨hus, hsv.symm, ⟨x, _, _⟩, _⟩
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
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 𝒜
rintro ⟨w, hwB, hw𝒜'⟩
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
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
have : v ⊆ insert w ((s ∪ v) \ u) :=
  (subset_sdiff.2 ⟨subset_union_right _ _, hvu⟩).trans (subset_insert _ _)
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

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
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
by_cases hwu : w ∈ u
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
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
rw [mem_sdiff, ← not_imp, Classical.not_not] at hwB
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 ∈ 𝒜
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
apply m w (hwu ∘ hwB ∘ mem_union_left _)
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 ∈ 𝒜
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 ∈ 𝒜
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⟩)
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
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 ∈ 𝒜
convert this using 1
no goals
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
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]
α : 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 ((∂ ) 𝒜)
α : 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 ((∂ ) 𝒜)
rintro s hs'
α : 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
α : 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 ((∂ ) 𝒜)
rw [mem_compression]
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
α : 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
by_cases hs : s ∈ 𝒜.shadow
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

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 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
swap
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 ∈ (∂ ) 𝒜
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
refine' Or.inl ⟨hs, _⟩
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) ∈ (∂ ) 𝒜
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 ∈ (∂ ) 𝒜
rw [compress]
case pos.inl
α : 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 pos.inr
α : 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 ∈ (∂ ) 𝒜
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) ∈ (∂ ) 𝒜
split_ifs with huvs
case pos.inr
α : 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 ∈ (∂ ) 𝒜

case pos.inl
α : 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 pos.inl
α : 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 pos.inr
α : 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 ∈ (∂ ) 𝒜
swap
case pos.inl
α : 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 ∈ (∂ ) 𝒜
case pos.inl
α : 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 ∈ (∂ ) 𝒜
rw [mem_shadow_iff] at hs'
case pos.inl.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 ∈ (∂ ) 𝒜
case pos.inl
α : 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 ∈ (∂ ) 𝒜
obtain ⟨t, Ht, a, hat, rfl⟩ := hs'
case pos.inl.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 ∈ (∂ ) 𝒜
case pos.inl.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 ∈ (∂ ) 𝒜
have hav : a ∉ v := not_mem_mono huvs.2 (not_mem_erase a t)
case pos.inl.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 ∈ (∂ ) 𝒜
case pos.inl.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 ∈ (∂ ) 𝒜
have hvt : v ≤ t := huvs.2.trans (erase_subset _ t)
case pos.inl.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 ∈ (∂ ) 𝒜
case pos.inl.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 ∈ (∂ ) 𝒜
have ht : t ∈ 𝒜 := mem_of_mem_compression Ht hvt (aux huv)
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 ∈ (∂ ) 𝒜

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 ∈ (∂ ) 𝒜
case pos.inl.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 ∈ (∂ ) 𝒜
by_cases hau : a ∈ u
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
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
obtain ⟨hus, hvs, h, _⟩ := H _ hs' hs
no goals
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
exact Or.inr ⟨hs, _, h, compress_of_disjoint_of_le' hvs hus⟩
no goals
case pos.inr
α : 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 ∈ (∂ ) 𝒜
exact hs
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 ∈ (∂ ) 𝒜
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 ∈ (∂ ) 𝒜
obtain ⟨b, hbv, Hcomp⟩ := huv a hau
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) ∈ 𝒜
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 ∈ (∂ ) 𝒜
refine' mem_shadow_iff_insert_mem.2 ⟨b, not_mem_sdiff_of_mem_right hbv, _⟩
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) ∈ 𝒜
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) ∈ 𝒜
rw [← Hcomp.eq] at ht
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) ∈ 𝒜
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) ∈ 𝒜
have hsb :=
  sup_sdiff_mem_of_mem_compression ht ((erase_subset _ _).trans hvt)
    (disjoint_erase_comm.2 huvs.1)
no goals
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) ∈ 𝒜
rwa [sup_eq_union, sdiff_erase (mem_union_left _ <| hvt hbv), union_erase_of_mem hat, ←
  erase_union_of_mem hau] at hsb
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

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
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 ∈ (∂ ) 𝒜
refine'
  mem_shadow_iff.2
    ⟨(t ⊔ u) \ v,
      sup_sdiff_mem_of_mem_compression Ht hvt <| disjoint_of_erase_right hau huvs.1, a, _, _⟩
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
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
rw [sup_eq_union, mem_sdiff, mem_union]
no goals
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
exact ⟨Or.inl hat, hav⟩
no goals
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
rw [← erase_sdiff_comm, sup_eq_union, erase_union_distrib, erase_eq_of_not_mem hau]
α : 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
α : 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
intro hxu
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
α : 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
obtain ⟨y, hyv, hxy⟩ := huv x hxu
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 ∈ 𝒜
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
apply m y (disjoint_right.1 hsv hyv)
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 ∈ 𝒜
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 ∈ 𝒜
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 _ _)
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
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 ∈ 𝒜
convert this using 1
no goals
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
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]
α : 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
α : 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 ∈ 𝒜
refine'
  sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) _
    (disjoint_of_subset_left (erase_subset _ _) disjoint_sdiff)
α : 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
α : 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
rw [union_sdiff_distrib, ‹v \ u = v›]
no goals
α : 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
exact (erase_subset _ _).trans (subset_union_right _ _)
no goals
α : 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) 𝒜
rwa [hxy.eq]
no goals
α : 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
rwa [← erase_eq_of_not_mem ‹x ∉ u›, ← subset_insert_iff]
no goals
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
exact not_mem_sdiff_of_not_mem_left (not_mem_union.2 ⟨‹x ∉ s›, ‹x ∉ v›⟩)
no goals
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) ∈ 𝒜
rwa [← insert_sdiff_of_not_mem _ ‹x ∉ u›, ← insert_union]
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
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
obtain ⟨z, hz, hxy⟩ := huv w hwu
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 ∈ 𝒜
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
apply m z (disjoint_right.1 hsv hz)
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 ∈ 𝒜
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 ∈ 𝒜
have : insert w ((s ∪ v) \ u) ∈ 𝒜 := mem_of_mem_compression hw𝒜' ‹_› (aux huv)
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 ∈ 𝒜
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 ∈ 𝒜
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
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
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 ∈ 𝒜
convert this using 1
no goals
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
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]
α : 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))
α : 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 ∈ 𝒜
refine' sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ((erase_subset _ _).trans ‹_›) _
α : 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)
α : 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))
rw [← sdiff_erase (mem_union_left _ <| hus hwu)]
no goals
α : 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)
exact disjoint_sdiff
no goals
α : 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) 𝒜
rwa [hxy.eq]