α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
h : ncard (f '' s) = ncard s
hs : autoParam (Set.Finite s) _auto✝
hft : Fintype ↑s
⊢ InjOn f s
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
h : ncard (f '' s) = ncard s
hs : autoParam (Set.Finite s) _auto✝
⊢ InjOn f s
have hft := hs.fintype
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
h : Finset.card (Finite.toFinset (_ : Set.Finite (f '' s))) = Finset.card (Finite.toFinset hs)
hft : Fintype ↑s
⊢ InjOn f s
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
h : ncard (f '' s) = ncard s
hs : autoParam (Set.Finite s) _auto✝
hft : Fintype ↑s
⊢ InjOn f s
rw [@ncard_eq_toFinset_card _ _ (hs.image f), @ncard_eq_toFinset_card _ _ hs] at h
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
h : Finset.card (Finite.toFinset (_ : Set.Finite (f '' s))) = Finset.card (Finite.toFinset hs)
hft : Fintype ↑s
⊢ InjOn f ↑(toFinset s)
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
h : Finset.card (Finite.toFinset (_ : Set.Finite (f '' s))) = Finset.card (Finite.toFinset hs)
hft : Fintype ↑s
⊢ InjOn f s
rw [←coe_toFinset s]
case H
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
h : Finset.card (Finite.toFinset (_ : Set.Finite (f '' s))) = Finset.card (Finite.toFinset hs)
hft : Fintype ↑s
⊢ Finset.card (Finset.image f (toFinset s)) = Finset.card (toFinset s)
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
h : Finset.card (Finite.toFinset (_ : Set.Finite (f '' s))) = Finset.card (Finite.toFinset hs)
hft : Fintype ↑s
⊢ InjOn f ↑(toFinset s)
apply Finset.injOn_of_card_image_eq
case h.e'_2.h.e'_2
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
h : Finset.card (Finite.toFinset (_ : Set.Finite (f '' s))) = Finset.card (Finite.toFinset hs)
hft : Fintype ↑s
⊢ Finset.image f (toFinset s) = Finite.toFinset (_ : Set.Finite (f '' s))

case h.e'_3.h.e'_2
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
h : Finset.card (Finite.toFinset (_ : Set.Finite (f '' s))) = Finset.card (Finite.toFinset hs)
hft : Fintype ↑s
⊢ toFinset s = Finite.toFinset hs
case H
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
h : Finset.card (Finite.toFinset (_ : Set.Finite (f '' s))) = Finset.card (Finite.toFinset hs)
hft : Fintype ↑s
⊢ Finset.card (Finset.image f (toFinset s)) = Finset.card (toFinset s)
convert h
case h.e'_3.h.e'_2.a
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
h : Finset.card (Finite.toFinset (_ : Set.Finite (f '' s))) = Finset.card (Finite.toFinset hs)
hft : Fintype ↑s
a✝ : α
⊢ a✝ ∈ toFinset s ↔ a✝ ∈ Finite.toFinset hs
case h.e'_3.h.e'_2
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
h : Finset.card (Finite.toFinset (_ : Set.Finite (f '' s))) = Finset.card (Finite.toFinset hs)
hft : Fintype ↑s
⊢ toFinset s = Finite.toFinset hs
ext
no goals
case h.e'_3.h.e'_2.a
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
h : Finset.card (Finite.toFinset (_ : Set.Finite (f '' s))) = Finset.card (Finite.toFinset hs)
hft : Fintype ↑s
a✝ : α
⊢ a✝ ∈ toFinset s ↔ a✝ ∈ Finite.toFinset hs
simp
case h.e'_2.h.e'_2.a
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
h : Finset.card (Finite.toFinset (_ : Set.Finite (f '' s))) = Finset.card (Finite.toFinset hs)
hft : Fintype ↑s
a✝ : β
⊢ a✝ ∈ Finset.image f (toFinset s) ↔ a✝ ∈ Finite.toFinset (_ : Set.Finite (f '' s))
case h.e'_2.h.e'_2
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
h : Finset.card (Finite.toFinset (_ : Set.Finite (f '' s))) = Finset.card (Finite.toFinset hs)
hft : Fintype ↑s
⊢ Finset.image f (toFinset s) = Finite.toFinset (_ : Set.Finite (f '' s))
ext
no goals
case h.e'_2.h.e'_2.a
α : Type u_2
β : Type u_1
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
h : Finset.card (Finite.toFinset (_ : Set.Finite (f '' s))) = Finset.card (Finite.toFinset hs)
hft : Fintype ↑s
a✝ : β
⊢ a✝ ∈ Finset.image f (toFinset s) ↔ a✝ ∈ Finite.toFinset (_ : Set.Finite (f '' s))
simp