memₗ_add_iff — Mathlib

English

If hx : x₁ ≡ x₂ and hy : y₁ ≡ y₂, then x₁ + y₁ ≡ x₂ + y₂.

Русский

Если x₁ эквивалентен x₂, а y₁ эквивалентен y₂, то x₁ + y₁ эквивалентно x₂ + y₂.

LaTeX

$$$ hx : x_1 \equiv x_2 \Rightarrow hy : y_1 \equiv y_2 \Rightarrow x_1 + y_1 \equiv x_2 + y_2 $$$

Lean4

theorem memₗ_add_iff {x y₁ y₂ : PGame} : x ∈ₗ y₁ + y₂ ↔ (∃ z ∈ₗ y₁, x ≡ z + y₂) ∨ (∃ z ∈ₗ y₂, x ≡ y₁ + z) :=
  by
  obtain ⟨y₁l, y₁r, y₁L, y₁R⟩ := y₁
  obtain ⟨y₂l, y₂r, y₂L, y₂R⟩ := y₂
  constructor
  · rintro ⟨(i | i), hi⟩
    exacts [.inl ⟨y₁L i, moveLeft_memₗ _ _, hi⟩, .inr ⟨y₂L i, moveLeft_memₗ _ _, hi⟩]
  · rintro (⟨_, ⟨i, hi⟩, h⟩ | ⟨_, ⟨i, hi⟩, h⟩)
    exacts [⟨.inl i, h.trans hi.add_right⟩, ⟨.inr i, h.trans hi.add_left⟩]

Похожие утверждения