α : Type u_2
β : Type u_1
γ : Type ?u.415864
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ count x (filter (fun a => f x = f a) s) = ↑card (filter (fun a => f x = f a) s)
α : Type u_2
β : Type u_1
γ : Type ?u.415864
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ count (f x) (map f s) = count x s
suffices (filter (fun a : α => f x = f a) s).count x = card (filter (fun a : α => f x = f a) s) by
  rw [count, countp_map, ← this]
  exact count_filter_of_pos $ rfl
α : Type u_2
β : Type u_1
γ : Type ?u.415864
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
this : count x (filter (fun a => f x = f a) s) = ↑card (filter (fun a => f x = f a) s)
⊢ count x (filter (fun a => f x = f a) s) = count x s
α : Type u_2
β : Type u_1
γ : Type ?u.415864
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
this : count x (filter (fun a => f x = f a) s) = ↑card (filter (fun a => f x = f a) s)
⊢ count (f x) (map f s) = count x s
rw [count, countp_map, ← this]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.415864
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
this : count x (filter (fun a => f x = f a) s) = ↑card (filter (fun a => f x = f a) s)
⊢ count x (filter (fun a => f x = f a) s) = count x s
exact count_filter_of_pos $ rfl
α : Type u_2
β : Type u_1
γ : Type ?u.415864
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ count x (replicate (↑card (filter (fun a => f x = f a) s)) x) =
    ↑card (replicate (↑card (filter (fun a => f x = f a) s)) x)

α : Type u_2
β : Type u_1
γ : Type ?u.415864
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ ∀ (b : α), b ∈ filter (fun a => f x = f a) s → f x = f b
α : Type u_2
β : Type u_1
γ : Type ?u.415864
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ count x (filter (fun a => f x = f a) s) = ↑card (filter (fun a => f x = f a) s)
rw [eq_replicate_card.2 fun b hb => (hf H (mem_filter.1 hb).left _).symm]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.415864
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ count x (replicate (↑card (filter (fun a => f x = f a) s)) x) =
    ↑card (replicate (↑card (filter (fun a => f x = f a) s)) x)
simp only [count_replicate, eq_self_iff_true, if_true, card_replicate]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.415864
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ ∀ (b : α), b ∈ filter (fun a => f x = f a) s → f x = f b
simp only [mem_filter, beq_iff_eq, and_imp, @eq_comm _ (f x), imp_self, implies_true]