case intro.intro
α : Type u_1
β : Type ?u.135235
γ : Type ?u.135238
p : α → Prop
s : Finset { x // p x }
x : { x // p x }
left✝ : x ∈ s
h : ↑(Embedding.subtype fun x => p x) x ∈ map (Embedding.subtype fun x => p x) s
⊢ p (↑(Embedding.subtype fun x => p x) x)
α : Type u_1
β : Type ?u.135235
γ : Type ?u.135238
p : α → Prop
s : Finset { x // p x }
a : α
h : a ∈ map (Embedding.subtype fun x => p x) s
⊢ p a
rcases mem_map.1 h with ⟨x, _, rfl⟩
no goals
case intro.intro
α : Type u_1
β : Type ?u.135235
γ : Type ?u.135238
p : α → Prop
s : Finset { x // p x }
x : { x // p x }
left✝ : x ∈ s
h : ↑(Embedding.subtype fun x => p x) x ∈ map (Embedding.subtype fun x => p x) s
⊢ p (↑(Embedding.subtype fun x => p x) x)
exact x.2