α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u a : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ ∅ ∧ IsCompressed (erase u x) (erase ∅ y) 𝒜
⊢ u = ∅
α : 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 = ∅
rintro rfl
α : 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
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u a : Finset α
huv : ∀ (x : α), x ∈ u → ∃ y, y ∈ ∅ ∧ IsCompressed (erase u x) (erase ∅ y) 𝒜
⊢ u = ∅
refine' eq_empty_of_forall_not_mem fun a ha => _
no goals
α : 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
obtain ⟨_, ⟨⟩, -⟩ := huv a ha