[STATEMENT]
lemma filter_mset_cong:
  assumes "M = M'" and "\<And>x. x \<in># M' \<Longrightarrow> f x \<longleftrightarrow> g x"
  shows "filter_mset f M = filter_mset g M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_mset f M = filter_mset g M'
[PROOF STEP]
unfolding \<open>M = M'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_mset f M' = filter_mset g M'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
M = M'
?x \<in># M' \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. filter_mset f M' = filter_mset g M'
[PROOF STEP]
by (auto intro: filter_mset_cong0)