English
Rel r (as0 + as1) bs is equivalent to the existence of bs0, bs1 with Rel r as0 bs0, Rel r as1 bs1, and bs = bs0 + bs1.
Русский
Относительно левого сложения: Rel r (as0 + as1) bs эквивалентно существованию bs0, bs1: Rel r as0 bs0, Rel r as1 bs1 и bs = bs0 + bs1.
LaTeX
$$$$ \forall as_0, as_1, \forall bs, \text{Rel}(r, as_0+as_1, bs) \iff \exists bs_0, bs_1, \text{Rel}(r, as_0, bs_0) \land \text{Rel}(r, as_1, bs_1) \land bs = bs_0 + bs_1 $$$$
Lean4
theorem rel_add_left {as₀ as₁} :
∀ {bs}, Rel r (as₀ + as₁) bs ↔ ∃ bs₀ bs₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁ :=
@(Multiset.induction_on as₀ (by simp) fun a s ih bs ↦
by
simp only [ih, cons_add, rel_cons_left]
constructor
· intro h
rcases h with ⟨b, bs', hab, h, rfl⟩
rcases h with ⟨bs₀, bs₁, h₀, h₁, rfl⟩
exact ⟨b ::ₘ bs₀, bs₁, ⟨b, bs₀, hab, h₀, rfl⟩, h₁, by simp⟩
· intro h
rcases h with ⟨bs₀, bs₁, h, h₁, rfl⟩
rcases h with ⟨b, bs, hab, h₀, rfl⟩
exact ⟨b, bs + bs₁, hab, ⟨bs, bs₁, h₀, h₁, rfl⟩, by simp⟩)
