-- Mathlib/SetTheory/Game/PGame.lean
lemma identical_zero_iff : ∀ (x : PGame),
    x ≡ 0 ↔ IsEmpty x.LeftMoves ∧ IsEmpty x.RightMoves
  | mk xl xr xL xR => by
    constructor
    · rintro ⟨h₁, h₂⟩
      dsimp [Relator.BiTotal, Relator.LeftTotal, Relator.RightTotal] at h₁ h₂
      simp_rw [IsEmpty.forall_iff, and_true, IsEmpty.exists_iff] at h₁ h₂
      exact ⟨⟨h₁⟩, ⟨h₂⟩⟩
    · rintro ⟨h₁, h₂⟩
      exact identical_of_isEmpty _ _

Proof state:
case mp.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h₁ : (∀ (a : xl), ∃ b, xL a ≡ b.elim) ∧ ∀ (b : PEmpty.{u_1 + 1}), ∃ a, xL a ≡ b.elim
h₂ : (∀ (a : xr), ∃ b, xR a ≡ b.elim) ∧ ∀ (b : PEmpty.{u_1 + 1}), ∃ a, xR a ≡ b.elim
⊢ IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk xl xr xL xR).RightMoves

Tactic:
simp_rw [IsEmpty.forall_iff, and_true, IsEmpty.exists_iff] at h₁ h₂

Result:
case mp.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h₁ : xl → False
h₂ : xr → False
⊢ IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk xl xr xL xR).RightMoves

Proof state:
case mpr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk xl xr xL xR).RightMoves → mk xl xr xL xR ≡ 0

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case mpr.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h₁ : IsEmpty (mk xl xr xL xR).LeftMoves
h₂ : IsEmpty (mk xl xr xL xR).RightMoves
⊢ mk xl xr xL xR ≡ 0

Proof state:
case mp
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ mk xl xr xL xR ≡ 0 → IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk xl xr xL xR).RightMoves

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case mp.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h₁ : Relator.BiTotal fun i j => xL i ≡ j.elim
h₂ : Relator.BiTotal fun i j => xR i ≡ j.elim
⊢ IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk xl xr xL xR).RightMoves

Proof state:
case mp.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h₁ : Relator.BiTotal fun i j => xL i ≡ j.elim
h₂ : Relator.BiTotal fun i j => xR i ≡ j.elim
⊢ IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk xl xr xL xR).RightMoves

Tactic:
dsimp [Relator.BiTotal, Relator.LeftTotal, Relator.RightTotal] at h₁ h₂

Result:
case mp.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h₁ : (∀ (a : xl), ∃ b, xL a ≡ b.elim) ∧ ∀ (b : PEmpty.{u_1 + 1}), ∃ a, xL a ≡ b.elim
h₂ : (∀ (a : xr), ∃ b, xR a ≡ b.elim) ∧ ∀ (b : PEmpty.{u_1 + 1}), ∃ a, xR a ≡ b.elim
⊢ IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk xl xr xL xR).RightMoves

Proof state:
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ mk xl xr xL xR ≡ 0 ↔ IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk xl xr xL xR).RightMoves

Tactic:
constructor

Result:
case mp
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ mk xl xr xL xR ≡ 0 → IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk xl xr xL xR).RightMoves

case mpr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk xl xr xL xR).RightMoves → mk xl xr xL xR ≡ 0

Proof state:
case mpr.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h₁ : IsEmpty (mk xl xr xL xR).LeftMoves
h₂ : IsEmpty (mk xl xr xL xR).RightMoves
⊢ mk xl xr xL xR ≡ 0

Tactic:
exact identical_of_isEmpty _ _

Result:
no goals

Proof state:
case mp.intro
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
h₁ : xl → False
h₂ : xr → False
⊢ IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk xl xr xL xR).RightMoves

Tactic:
exact ⟨⟨h₁⟩, ⟨h₂⟩⟩

Result:
no goals