α : Type u_2
β : Type u_1
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H :
  ↑Multiset.card { val := dedup (Multiset.map f s.val), nodup := (_ : Nodup (dedup (Multiset.map f s.val))) }.val =
    ↑Multiset.card s.val
⊢ Set.InjOn f ↑s
α : Type u_2
β : Type u_1
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : card (image f s) = card s
⊢ Set.InjOn f ↑s
rw [card_def, card_def, image, toFinset] at H
α : Type u_2
β : Type u_1
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
⊢ Set.InjOn f ↑s
α : Type u_2
β : Type u_1
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H :
  ↑Multiset.card { val := dedup (Multiset.map f s.val), nodup := (_ : Nodup (dedup (Multiset.map f s.val))) }.val =
    ↑Multiset.card s.val
⊢ Set.InjOn f ↑s
dsimp only at H
α : Type u_2
β : Type u_1
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
this : dedup (Multiset.map f s.val) = Multiset.map f s.val
⊢ Set.InjOn f ↑s
α : Type u_2
β : Type u_1
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
⊢ Set.InjOn f ↑s
have : (s.1.map f).dedup = s.1.map f := by
  refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_
  simp only [H, Multiset.card_map, le_rfl]
α : Type u_2
β : Type u_1
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
this : Nodup (Multiset.map f s.val)
⊢ Set.InjOn f ↑s
α : Type u_2
β : Type u_1
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
this : dedup (Multiset.map f s.val) = Multiset.map f s.val
⊢ Set.InjOn f ↑s
rw [Multiset.dedup_eq_self] at this
no goals
α : Type u_2
β : Type u_1
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
this : Nodup (Multiset.map f s.val)
⊢ Set.InjOn f ↑s
exact inj_on_of_nodup_map this
α : Type u_2
β : Type u_1
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
⊢ ↑Multiset.card (Multiset.map f s.val) ≤ ↑Multiset.card (dedup (Multiset.map f s.val))
α : Type u_2
β : Type u_1
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
⊢ dedup (Multiset.map f s.val) = Multiset.map f s.val
refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_
no goals
α : Type u_2
β : Type u_1
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
⊢ ↑Multiset.card (Multiset.map f s.val) ≤ ↑Multiset.card (dedup (Multiset.map f s.val))
simp only [H, Multiset.card_map, le_rfl]