case h.e'_2
α : Type u_1
β : Type ?u.47787
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
⊢ Nat.card ↑s = ncard univ

case h.e'_3
α : Type u_1
β : Type ?u.47787
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
⊢ ncard s = ncard ((fun a => ↑a) '' univ)

case convert_1
α : Type u_1
β : Type ?u.47787
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
⊢ Type ?u.47955

case convert_2
α : Type u_1
β : Type ?u.47787
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
⊢ ?convert_1 → Prop
α : Type u_1
β : Type ?u.47787
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
⊢ Nat.card ↑s = ncard s
convert (ncard_image_ofInjective univ Subtype.coe_injective).symm using 1
no goals
case h.e'_3
α : Type u_1
β : Type ?u.47787
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
⊢ ncard s = ncard ((fun a => ↑a) '' univ)
simp
no goals
case h.e'_2
α : Type u_1
β : Type ?u.47787
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
⊢ Nat.card ↑s = ncard univ
rw [ncard_univ]