-- Mathlib/Data/Multiset/Filter.lean
theorem count_map_eq_count [DecidableEq β] (f : α → β) (s : Multiset α)
    (hf : Set.InjOn f { x : α | x ∈ s }) (x) (H : x ∈ s) : (s.map f).count (f x) = s.count x

Proof state:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ count x (replicate (filter (fun a => f x = f a) s).card x) = (replicate (filter (fun a => f x = f a) s).card x).card

Tactic:
simp only [count_replicate, eq_self_iff_true, if_true, card_replicate]

Result:
no goals

Proof state:
α : Type u_1
β : Type v
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) = (filter (fun a => f x = f a) s).card
⊢ count x (filter (fun a => f x = f a) s) = count x s

Tactic:
exact count_filter_of_pos <| rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type v
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) = (filter (fun a => f x = f a) s).card

Tactic:
rw [eq_replicate_card.2 fun b hb => (hf H (mem_filter.1 hb).left _).symm]

Result:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ count x (replicate (filter (fun a => f x = f a) s).card x) = (replicate (filter (fun a => f x = f a) s).card x).card

α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ ∀ b ∈ filter (fun a => f x = f a) s, f x = f b

Proof state:
α : Type u_1
β : Type v
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

Tactic:
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

Result:
α : Type u_1
β : Type v
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) = (filter (fun a => f x = f a) s).card

Proof state:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ ∀ b ∈ filter (fun a => f x = f a) s, f x = f b

Tactic:
simp only [mem_filter, beq_iff_eq, and_imp, @eq_comm _ (f x), imp_self, implies_true]

Result:
no goals

Proof state:
α : Type u_1
β : Type v
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) = (filter (fun a => f x = f a) s).card
⊢ count (f x) (map f s) = count x s

Tactic:
rw [count, countP_map, ← this]

Result:
α : Type u_1
β : Type v
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) = (filter (fun a => f x = f a) s).card
⊢ count x (filter (fun a => f x = f a) s) = count x s