case h.e'_3.h.e'_2
α : Type u_1
β : Type ?u.42313
s✝ t : Set α
a b x y : α
f : α → β
P : α → Prop
s : Set α
⊢ s ∩ setOf P = (fun a => ↑a) '' {x | ↑x ∈ s}
α : Type u_1
β : Type ?u.42313
s✝ t : Set α
a b x y : α
f : α → β
P : α → Prop
s : Set α
⊢ ncard {x | ↑x ∈ s} = ncard (s ∩ setOf P)
convert (ncard_image_ofInjective _ (@Subtype.coe_injective _ P)).symm
case h.e'_3.h.e'_2.h
α : Type u_1
β : Type ?u.42313
s✝ t : Set α
a b x✝ y : α
f : α → β
P : α → Prop
s : Set α
x : α
⊢ x ∈ s ∩ setOf P ↔ x ∈ (fun a => ↑a) '' {x | ↑x ∈ s}
case h.e'_3.h.e'_2
α : Type u_1
β : Type ?u.42313
s✝ t : Set α
a b x y : α
f : α → β
P : α → Prop
s : Set α
⊢ s ∩ setOf P = (fun a => ↑a) '' {x | ↑x ∈ s}
ext x
no goals
case h.e'_3.h.e'_2.h
α : Type u_1
β : Type ?u.42313
s✝ t : Set α
a b x✝ y : α
f : α → β
P : α → Prop
s : Set α
x : α
⊢ x ∈ s ∩ setOf P ↔ x ∈ (fun a => ↑a) '' {x | ↑x ∈ s}
simp [←and_assoc, exists_eq_right]