α : Type u_1
β : Type ?u.135552
γ : Type ?u.135555
t : Set α
s : Finset ↑t
a : α
ha : a ∈ ↑(map (Embedding.subtype fun x => x ∈ t) s)
⊢ a ∈ t
α : Type u_1
β : Type ?u.135552
γ : Type ?u.135555
t : Set α
s : Finset ↑t
⊢ ↑(map (Embedding.subtype fun x => x ∈ t) s) ⊆ t
intro a ha
α : Type u_1
β : Type ?u.135552
γ : Type ?u.135555
t : Set α
s : Finset ↑t
a : α
ha : a ∈ map (Embedding.subtype fun x => x ∈ t) s
⊢ a ∈ t
α : Type u_1
β : Type ?u.135552
γ : Type ?u.135555
t : Set α
s : Finset ↑t
a : α
ha : a ∈ ↑(map (Embedding.subtype fun x => x ∈ t) s)
⊢ a ∈ t
rw [mem_coe] at ha
no goals
α : Type u_1
β : Type ?u.135552
γ : Type ?u.135555
t : Set α
s : Finset ↑t
a : α
ha : a ∈ map (Embedding.subtype fun x => x ∈ t) s
⊢ a ∈ t
convert property_of_mem_map_subtype s ha