α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ Set.InjOn ((fun x x_1 => x ∪ x_1) s) ↑(powerset (t \ s))
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ card (Icc s t) = 2 ^ (card t - card s)
rw [← card_sdiff h, ← card_powerset, Icc_eq_image_powerset h, Finset.card_image_iff]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hu : u ∈ ↑(powerset (t \ s))
v : Finset α
hv : v ∈ ↑(powerset (t \ s))
huv : s ⊔ u = s ⊔ v
⊢ u = v
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ Set.InjOn ((fun x x_1 => x ∪ x_1) s) ↑(powerset (t \ s))
rintro u hu v hv (huv : s ⊔ u = s ⊔ v)
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hu : u ⊆ t \ s
v : Finset α
hv : v ⊆ t \ s
huv : s ⊔ u = s ⊔ v
⊢ u = v
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hu : u ∈ ↑(powerset (t \ s))
v : Finset α
hv : v ∈ ↑(powerset (t \ s))
huv : s ⊔ u = s ⊔ v
⊢ u = v
rw [mem_coe, mem_powerset] at hu hv
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hu : u ⊆ t \ s
v : Finset α
hv : v ⊆ t \ s
huv : s ⊔ u = s ⊔ v
⊢ u = v
rw [← (disjoint_sdiff.mono_right hu : Disjoint s u).sup_sdiff_cancel_left, ←
  (disjoint_sdiff.mono_right hv : Disjoint s v).sup_sdiff_cancel_left, huv]