English
Characterization of when x is a left move from the sum y₁+y₂: x ∈ₗ y₁+y₂ iff x ≡ z+y₂ for some z ∈ₗ y₁ or x ≡ y₁+z for some z ∈ₗ y₂.
Русский
Характеризация того, когда x является левым ходом из суммы y₁+y₂: x ∈ₗ y₁+y₂ тогда и только тогда, когда существует z ∈ₗ y₁ так, что x ≡ z+y₂, или существует z ∈ₗ y₂ так, что x ≡ y₁+z.
LaTeX
$$$ x \in_\ell (y_1+y_2) \iff (\exists z \in_\ell y_1, x \equiv z+y_2) \lor (\exists z \in_\ell y_2, x \equiv y_1+z) $$$
Lean4
theorem add_right {x₁ x₂ y} : x₁ ≡ x₂ → x₁ + y ≡ x₂ + y :=
match x₁, x₂, y with
| mk x₁l x₁r x₁L x₁R, mk x₂l x₂r x₂L x₂R, mk yl yr yL yR =>
by
intro h
refine ⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩ <;> rintro (_ | _) <;> try exact ⟨.inr _, h.add_right⟩
· exact (h.1.1 _).elim (⟨.inl ·, ·.add_right⟩)
· exact (h.1.2 _).elim (⟨.inl ·, ·.add_right⟩)
· exact (h.2.1 _).elim (⟨.inl ·, ·.add_right⟩)
· exact (h.2.2 _).elim (⟨.inl ·, ·.add_right⟩)
termination_by (x₁, x₂, y)
