Theorem: Usa2002P1.Finset.subtype_map_subtype (Compfiles/Usa2002P1.lean)

State before:
α : Type
p : α → Prop
inst✝ : DecidablePred p
x : Finset { a // p a }
⊢ Finset.subtype p (Finset.map (Function.Embedding.subtype p) x) = x
Tactic:
ext ⟨y, hy⟩
State after:
case a.mk
α : Type
p : α → Prop
inst✝ : DecidablePred p
x : Finset { a // p a }
y : α
hy : p y
⊢ ⟨y, hy⟩ ∈ Finset.subtype p (Finset.map (Function.Embedding.subtype p) x) ↔ ⟨y, hy⟩ ∈ x

State before:
case a.mk
α : Type
p : α → Prop
inst✝ : DecidablePred p
x : Finset { a // p a }
y : α
hy : p y
⊢ ⟨y, hy⟩ ∈ Finset.subtype p (Finset.map (Function.Embedding.subtype p) x) ↔ ⟨y, hy⟩ ∈ x
Tactic:
simp [hy]
State after:
no goals