case inl
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
H : InjOn f s
h : Set.Finite s
⊢ ncard (f '' s) = ncard s

case inr
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
H : InjOn f s
h : Set.Infinite s
⊢ ncard (f '' s) = ncard s
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
H : InjOn f s
⊢ ncard (f '' s) = ncard s
cases' s.finite_or_infinite with h h
no goals
case inr
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
H : InjOn f s
h : Set.Infinite s
⊢ ncard (f '' s) = ncard s
rw [h.ncard, ((infinite_image_iff H).mpr h).ncard]
case inl
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
H : InjOn f s
h : Set.Finite s
this : Fintype ↑s
⊢ ncard (f '' s) = ncard s
case inl
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
H : InjOn f s
h : Set.Finite s
⊢ ncard (f '' s) = ncard s
haveI := @Fintype.ofFinite s h.to_subtype
case inl
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
H : InjOn f s
h : Set.Finite s
this✝ : Fintype ↑s
this : Fintype ↑(f '' s)
⊢ ncard (f '' s) = ncard s
case inl
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
H : InjOn f s
h : Set.Finite s
this : Fintype ↑s
⊢ ncard (f '' s) = ncard s
haveI := @Fintype.ofFinite _ (h.image f).to_subtype
no goals
case inl
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
H : InjOn f s
h : Set.Finite s
this✝ : Fintype ↑s
this : Fintype ↑(f '' s)
⊢ ncard (f '' s) = ncard s
convert card_image_of_inj_on H <;> simp [ncard_def]