[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ∈ (fun s t => filter ((fun x x_1 => x ⊆ x_1) s) (powerset t)) s t ↔ s ≤ u ∧ u ≤ t
[PROOFSTEP]
rw [mem_filter, mem_powerset]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ⊆ t ∧ (fun x x_1 => x ⊆ x_1) s u ↔ s ≤ u ∧ u ≤ t
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ∈ (fun s t => filter ((fun x x_1 => x ⊆ x_1) s) (ssubsets t)) s t ↔ s ≤ u ∧ u < t
[PROOFSTEP]
rw [mem_filter, mem_ssubsets]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ⊂ t ∧ (fun x x_1 => x ⊆ x_1) s u ↔ s ≤ u ∧ u < t
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ∈ (fun s t => filter ((fun x x_1 => x ⊂ x_1) s) (powerset t)) s t ↔ s < u ∧ u ≤ t
[PROOFSTEP]
rw [mem_filter, mem_powerset]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ⊆ t ∧ (fun x x_1 => x ⊂ x_1) s u ↔ s < u ∧ u ≤ t
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ∈ (fun s t => filter ((fun x x_1 => x ⊂ x_1) s) (ssubsets t)) s t ↔ s < u ∧ u < t
[PROOFSTEP]
rw [mem_filter, mem_ssubsets]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t u : Finset α
⊢ u ⊂ t ∧ (fun x x_1 => x ⊂ x_1) s u ↔ s < u ∧ u < t
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ Icc s t = image ((fun x x_1 => x ∪ x_1) s) (powerset (t \ s))
[PROOFSTEP]
ext u
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ u ∈ Icc s t ↔ u ∈ image ((fun x x_1 => x ∪ x_1) s) (powerset (t \ s))
[PROOFSTEP]
simp_rw [mem_Icc, mem_image, mem_powerset]
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u ≤ t ↔ ∃ a, a ⊆ t \ s ∧ s ∪ a = u
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u ≤ t → ∃ a, a ⊆ t \ s ∧ s ∪ a = u
[PROOFSTEP]
rintro ⟨hs, ht⟩
[GOAL]
case a.mp.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hs : s ≤ u
ht : u ≤ t
⊢ ∃ a, a ⊆ t \ s ∧ s ∪ a = u
[PROOFSTEP]
exact ⟨u \ s, sdiff_le_sdiff_right ht, sup_sdiff_cancel_right hs⟩
[GOAL]
case a.mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ (∃ a, a ⊆ t \ s ∧ s ∪ a = u) → s ≤ u ∧ u ≤ t
[PROOFSTEP]
rintro ⟨v, hv, rfl⟩
[GOAL]
case a.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
v : Finset α
hv : v ⊆ t \ s
⊢ s ≤ s ∪ v ∧ s ∪ v ≤ t
[PROOFSTEP]
exact ⟨le_sup_left, union_subset h <| hv.trans <| sdiff_subset _ _⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ Ico s t = image ((fun x x_1 => x ∪ x_1) s) (ssubsets (t \ s))
[PROOFSTEP]
ext u
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ u ∈ Ico s t ↔ u ∈ image ((fun x x_1 => x ∪ x_1) s) (ssubsets (t \ s))
[PROOFSTEP]
simp_rw [mem_Ico, mem_image, mem_ssubsets]
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u < t ↔ ∃ a, a ⊂ t \ s ∧ s ∪ a = u
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u < t → ∃ a, a ⊂ t \ s ∧ s ∪ a = u
[PROOFSTEP]
rintro ⟨hs, ht⟩
[GOAL]
case a.mp.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hs : s ≤ u
ht : u < t
⊢ ∃ a, a ⊂ t \ s ∧ s ∪ a = u
[PROOFSTEP]
exact ⟨u \ s, sdiff_lt_sdiff_right ht hs, sup_sdiff_cancel_right hs⟩
[GOAL]
case a.mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ (∃ a, a ⊂ t \ s ∧ s ∪ a = u) → s ≤ u ∧ u < t
[PROOFSTEP]
rintro ⟨v, hv, rfl⟩
[GOAL]
case a.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
v : Finset α
hv : v ⊂ t \ s
⊢ s ≤ s ∪ v ∧ s ∪ v < t
[PROOFSTEP]
exact ⟨le_sup_left, sup_lt_of_lt_sdiff_left hv h⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ card (Icc s t) = 2 ^ (card t - card s)
[PROOFSTEP]
rw [← card_sdiff h, ← card_powerset, Icc_eq_image_powerset h, Finset.card_image_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ Set.InjOn ((fun x x_1 => x ∪ x_1) s) ↑(powerset (t \ s))
[PROOFSTEP]
rintro u hu v hv (huv : s ⊔ u = s ⊔ v)
[GOAL]
α : 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
[PROOFSTEP]
rw [mem_coe, mem_powerset] at hu hv 
[GOAL]
α : 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
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ card (Ico s t) = 2 ^ (card t - card s) - 1
[PROOFSTEP]
rw [card_Ico_eq_card_Icc_sub_one, card_Icc_finset h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ card (Ioc s t) = 2 ^ (card t - card s) - 1
[PROOFSTEP]
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc_finset h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ card (Ioo s t) = 2 ^ (card t - card s) - 2
[PROOFSTEP]
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc_finset h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ card (Iic s) = 2 ^ card s
[PROOFSTEP]
rw [Iic_eq_powerset, card_powerset]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ card (Iio s) = 2 ^ card s - 1
[PROOFSTEP]
rw [Iio_eq_ssubsets, ssubsets, card_erase_of_mem (mem_powerset_self _), card_powerset]
