English
Rel r (a ::ₘ as) bs holds exactly when there exist b and bs' with r a b, Rel r as bs', and bs = b ::ₘ bs'.
Русский
Rel r (a ::ₘ as) bs выполняется тогда, когда существуют b и bs' такие, что r a b, Rel r as bs' и bs = b ::ₘ bs'.
LaTeX
$$$Rel\ r( Multiset.cons\ a\ as)\ bs \iff \exists b\ exists bs' , r\ a\ b \land Rel\ r\ as\ bs' \land bs = b ::ₘ bs'$$$
Lean4
theorem rel_cons_left {a as bs} : Rel r (a ::ₘ as) bs ↔ ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs' :=
by
constructor
· generalize hm : a ::ₘ as = m
intro h
induction h generalizing as with
| zero => simp at hm
| @cons a' b as' bs ha'b h
ih =>
rcases cons_eq_cons.1 hm with (⟨eq₁, eq₂⟩ | ⟨_h, cs, eq₁, eq₂⟩)
· subst eq₁
subst eq₂
exact ⟨b, bs, ha'b, h, rfl⟩
· rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩
· exact fun ⟨b, bs', hab, h, Eq⟩ => Eq.symm ▸ Rel.cons hab h
