α : Type u_1
β : Type ?u.39958
γ : Type ?u.39961
s t : Finset α
a b : α
h : s ⊂ t
⊢ ∃ a h, cons a s h ⊆ t
α : Type u_1
β : Type ?u.39958
γ : Type ?u.39961
s t : Finset α
a b : α
⊢ s ⊂ t ↔ ∃ a h, cons a s h ⊆ t
refine' ⟨fun h => _, fun ⟨a, ha, h⟩ => ssubset_of_ssubset_of_subset (ssubset_cons _) h⟩
case intro.intro
α : Type u_1
β : Type ?u.39958
γ : Type ?u.39961
s t : Finset α
a✝ b : α
h : s ⊂ t
a : α
hs : a ∈ t
ht : ¬a ∈ s
⊢ ∃ a h, cons a s h ⊆ t
α : Type u_1
β : Type ?u.39958
γ : Type ?u.39961
s t : Finset α
a b : α
h : s ⊂ t
⊢ ∃ a h, cons a s h ⊆ t
obtain ⟨a, hs, ht⟩ := not_subset.1 h.2
no goals
case intro.intro
α : Type u_1
β : Type ?u.39958
γ : Type ?u.39961
s t : Finset α
a✝ b : α
h : s ⊂ t
a : α
hs : a ∈ t
ht : ¬a ∈ s
⊢ ∃ a h, cons a s h ⊆ t
exact ⟨a, ht, cons_subset.2 ⟨hs, h.subset⟩⟩