English
For a relation r on α that is transitive and symmetric, and for multisets s,t and element x, if Rel r s t holds then the counts of r x in s and t are equal.
Русский
Для отношения r на α, удовлетворяющего свойствам транзитивности и симметрии, и для мультимножества s,t и элемента x, если Rel r s t выполняется, то countP (r x) s = countP (r x) t.
LaTeX
$$(Rel r s t) \Rightarrow \operatorname{countP}(r x, s) = \operatorname{countP}(r x, t)$$
Lean4
theorem countP_eq (r : α → α → Prop) [IsTrans α r] [IsSymm α r] {s t : Multiset α} (x : α) [DecidablePred (r x)]
(h : Rel r s t) : countP (r x) s = countP (r x) t := by
induction s using Multiset.induction_on generalizing t with
| empty => rw [rel_zero_left.mp h]
| cons y s ih =>
obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp h
rw [countP_cons, countP_cons, ih hb2]
simp only [Nat.add_right_inj]
exact (if_congr ⟨fun h => _root_.trans h hb1, fun h => _root_.trans h (symm hb1)⟩ rfl rfl)
