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))
α : 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))
ext u
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
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))
simp_rw [mem_Ico, mem_image, mem_ssubsets]
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

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
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
constructor
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
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
rintro ⟨hs, ht⟩
no goals
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
exact ⟨u \ s, sdiff_lt_sdiff_right ht hs, sup_sdiff_cancel_right hs⟩
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
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
rintro ⟨v, hv, rfl⟩
no goals
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
exact ⟨le_sup_left, sup_lt_of_lt_sdiff_left hv h⟩