-- Mathlib/SetTheory/Game/PGame.lean
lemma memᵣ_add_iff {x y₁ y₂ : PGame} :
    x ∈ᵣ y₁ + y₂ ↔ (∃ z ∈ᵣ y₁, x ≡ z + y₂) ∨ (∃ z ∈ᵣ y₂, x ≡ y₁ + z)

Proof state:
case mk.mk.mp.intro.inl
x : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
y₂l y₂r : Type u_1
y₂L : y₂l → PGame
y₂R : y₂r → PGame
i : y₁r
hi : x ≡ (mk y₁l y₁r y₁L y₁R + mk y₂l y₂r y₂L y₂R).moveRight (Sum.inl i)
⊢ (∃ z, z ∈ᵣ mk y₁l y₁r y₁L y₁R ∧ x ≡ z + mk y₂l y₂r y₂L y₂R) ∨
    ∃ z, z ∈ᵣ mk y₂l y₂r y₂L y₂R ∧ x ≡ mk y₁l y₁r y₁L y₁R + z

case mk.mk.mp.intro.inr
x : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
y₂l y₂r : Type u_1
y₂L : y₂l → PGame
y₂R : y₂r → PGame
i : y₂r
hi : x ≡ (mk y₁l y₁r y₁L y₁R + mk y₂l y₂r y₂L y₂R).moveRight (Sum.inr i)
⊢ (∃ z, z ∈ᵣ mk y₁l y₁r y₁L y₁R ∧ x ≡ z + mk y₂l y₂r y₂L y₂R) ∨
    ∃ z, z ∈ᵣ mk y₂l y₂r y₂L y₂R ∧ x ≡ mk y₁l y₁r y₁L y₁R + z

Tactic:
exacts [.inl ⟨y₁R i, moveRight_memᵣ _ _, hi⟩, .inr ⟨y₂R i, moveRight_memᵣ _ _, hi⟩]

Result:
no goals

Proof state:
case mk
x y₂ : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
⊢ x ∈ᵣ mk y₁l y₁r y₁L y₁R + y₂ ↔ (∃ z, z ∈ᵣ mk y₁l y₁r y₁L y₁R ∧ x ≡ z + y₂) ∨ ∃ z, z ∈ᵣ y₂ ∧ x ≡ mk y₁l y₁r y₁L y₁R + z

Tactic:
obtain ⟨y₂l, y₂r, y₂L, y₂R⟩ := y₂

Result:
case mk.mk
x : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
y₂l y₂r : Type u_1
y₂L : y₂l → PGame
y₂R : y₂r → PGame
⊢ x ∈ᵣ mk y₁l y₁r y₁L y₁R + mk y₂l y₂r y₂L y₂R ↔
    (∃ z, z ∈ᵣ mk y₁l y₁r y₁L y₁R ∧ x ≡ z + mk y₂l y₂r y₂L y₂R) ∨
      ∃ z, z ∈ᵣ mk y₂l y₂r y₂L y₂R ∧ x ≡ mk y₁l y₁r y₁L y₁R + z

Proof state:
case mk.mk
x : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
y₂l y₂r : Type u_1
y₂L : y₂l → PGame
y₂R : y₂r → PGame
⊢ x ∈ᵣ mk y₁l y₁r y₁L y₁R + mk y₂l y₂r y₂L y₂R ↔
    (∃ z, z ∈ᵣ mk y₁l y₁r y₁L y₁R ∧ x ≡ z + mk y₂l y₂r y₂L y₂R) ∨
      ∃ z, z ∈ᵣ mk y₂l y₂r y₂L y₂R ∧ x ≡ mk y₁l y₁r y₁L y₁R + z

Tactic:
constructor

Result:
case mk.mk.mp
x : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
y₂l y₂r : Type u_1
y₂L : y₂l → PGame
y₂R : y₂r → PGame
⊢ x ∈ᵣ mk y₁l y₁r y₁L y₁R + mk y₂l y₂r y₂L y₂R →
    (∃ z, z ∈ᵣ mk y₁l y₁r y₁L y₁R ∧ x ≡ z + mk y₂l y₂r y₂L y₂R) ∨
      ∃ z, z ∈ᵣ mk y₂l y₂r y₂L y₂R ∧ x ≡ mk y₁l y₁r y₁L y₁R + z

case mk.mk.mpr
x : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
y₂l y₂r : Type u_1
y₂L : y₂l → PGame
y₂R : y₂r → PGame
⊢ ((∃ z, z ∈ᵣ mk y₁l y₁r y₁L y₁R ∧ x ≡ z + mk y₂l y₂r y₂L y₂R) ∨
      ∃ z, z ∈ᵣ mk y₂l y₂r y₂L y₂R ∧ x ≡ mk y₁l y₁r y₁L y₁R + z) →
    x ∈ᵣ mk y₁l y₁r y₁L y₁R + mk y₂l y₂r y₂L y₂R

Proof state:
x y₁ y₂ : PGame
⊢ x ∈ᵣ y₁ + y₂ ↔ (∃ z, z ∈ᵣ y₁ ∧ x ≡ z + y₂) ∨ ∃ z, z ∈ᵣ y₂ ∧ x ≡ y₁ + z

Tactic:
obtain ⟨y₁l, y₁r, y₁L, y₁R⟩ := y₁

Result:
case mk
x y₂ : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
⊢ x ∈ᵣ mk y₁l y₁r y₁L y₁R + y₂ ↔ (∃ z, z ∈ᵣ mk y₁l y₁r y₁L y₁R ∧ x ≡ z + y₂) ∨ ∃ z, z ∈ᵣ y₂ ∧ x ≡ mk y₁l y₁r y₁L y₁R + z

Proof state:
case mk.mk.mp
x : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
y₂l y₂r : Type u_1
y₂L : y₂l → PGame
y₂R : y₂r → PGame
⊢ x ∈ᵣ mk y₁l y₁r y₁L y₁R + mk y₂l y₂r y₂L y₂R →
    (∃ z, z ∈ᵣ mk y₁l y₁r y₁L y₁R ∧ x ≡ z + mk y₂l y₂r y₂L y₂R) ∨
      ∃ z, z ∈ᵣ mk y₂l y₂r y₂L y₂R ∧ x ≡ mk y₁l y₁r y₁L y₁R + z

Tactic:
rintro ⟨(i | i), hi⟩

Result:
case mk.mk.mp.intro.inl
x : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
y₂l y₂r : Type u_1
y₂L : y₂l → PGame
y₂R : y₂r → PGame
i : y₁r
hi : x ≡ (mk y₁l y₁r y₁L y₁R + mk y₂l y₂r y₂L y₂R).moveRight (Sum.inl i)
⊢ (∃ z, z ∈ᵣ mk y₁l y₁r y₁L y₁R ∧ x ≡ z + mk y₂l y₂r y₂L y₂R) ∨
    ∃ z, z ∈ᵣ mk y₂l y₂r y₂L y₂R ∧ x ≡ mk y₁l y₁r y₁L y₁R + z

case mk.mk.mp.intro.inr
x : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
y₂l y₂r : Type u_1
y₂L : y₂l → PGame
y₂R : y₂r → PGame
i : y₂r
hi : x ≡ (mk y₁l y₁r y₁L y₁R + mk y₂l y₂r y₂L y₂R).moveRight (Sum.inr i)
⊢ (∃ z, z ∈ᵣ mk y₁l y₁r y₁L y₁R ∧ x ≡ z + mk y₂l y₂r y₂L y₂R) ∨
    ∃ z, z ∈ᵣ mk y₂l y₂r y₂L y₂R ∧ x ≡ mk y₁l y₁r y₁L y₁R + z

Proof state:
case mk.mk.mpr
x : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
y₂l y₂r : Type u_1
y₂L : y₂l → PGame
y₂R : y₂r → PGame
⊢ ((∃ z, z ∈ᵣ mk y₁l y₁r y₁L y₁R ∧ x ≡ z + mk y₂l y₂r y₂L y₂R) ∨
      ∃ z, z ∈ᵣ mk y₂l y₂r y₂L y₂R ∧ x ≡ mk y₁l y₁r y₁L y₁R + z) →
    x ∈ᵣ mk y₁l y₁r y₁L y₁R + mk y₂l y₂r y₂L y₂R

Tactic:
rintro (⟨_, ⟨i, hi⟩, h⟩ | ⟨_, ⟨i, hi⟩, h⟩)

Result:
case mk.mk.mpr.inl.intro.intro.intro
x : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
y₂l y₂r : Type u_1
y₂L : y₂l → PGame
y₂R : y₂r → PGame
w✝ : PGame
h : x ≡ w✝ + mk y₂l y₂r y₂L y₂R
i : (mk y₁l y₁r y₁L y₁R).RightMoves
hi : w✝ ≡ (mk y₁l y₁r y₁L y₁R).moveRight i
⊢ x ∈ᵣ mk y₁l y₁r y₁L y₁R + mk y₂l y₂r y₂L y₂R

case mk.mk.mpr.inr.intro.intro.intro
x : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
y₂l y₂r : Type u_1
y₂L : y₂l → PGame
y₂R : y₂r → PGame
w✝ : PGame
h : x ≡ mk y₁l y₁r y₁L y₁R + w✝
i : (mk y₂l y₂r y₂L y₂R).RightMoves
hi : w✝ ≡ (mk y₂l y₂r y₂L y₂R).moveRight i
⊢ x ∈ᵣ mk y₁l y₁r y₁L y₁R + mk y₂l y₂r y₂L y₂R

Proof state:
case mk.mk.mpr.inl.intro.intro.intro
x : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
y₂l y₂r : Type u_1
y₂L : y₂l → PGame
y₂R : y₂r → PGame
w✝ : PGame
h : x ≡ w✝ + mk y₂l y₂r y₂L y₂R
i : (mk y₁l y₁r y₁L y₁R).RightMoves
hi : w✝ ≡ (mk y₁l y₁r y₁L y₁R).moveRight i
⊢ x ∈ᵣ mk y₁l y₁r y₁L y₁R + mk y₂l y₂r y₂L y₂R

case mk.mk.mpr.inr.intro.intro.intro
x : PGame
y₁l y₁r : Type u_1
y₁L : y₁l → PGame
y₁R : y₁r → PGame
y₂l y₂r : Type u_1
y₂L : y₂l → PGame
y₂R : y₂r → PGame
w✝ : PGame
h : x ≡ mk y₁l y₁r y₁L y₁R + w✝
i : (mk y₂l y₂r y₂L y₂R).RightMoves
hi : w✝ ≡ (mk y₂l y₂r y₂L y₂R).moveRight i
⊢ x ∈ᵣ mk y₁l y₁r y₁L y₁R + mk y₂l y₂r y₂L y₂R

Tactic:
exacts [⟨.inl i, h.trans hi.add_right⟩, ⟨.inr i, h.trans hi.add_left⟩]

Result:
no goals