-- Mathlib/SetTheory/Game/Birthday.lean
theorem Relabelling.birthday_congr : ∀ {x y : PGame.{u}}, x ≡r y → birthday x = birthday y
  | ⟨xl, xr, xL, xR⟩, ⟨yl, yr, yL, yR⟩, r => by
    unfold birthday
    congr 1
    all_goals
      apply lsub_eq_of_range_eq.{u, u, u}
      ext i; constructor
    all_goals rintro ⟨j, rfl⟩
    · exact ⟨_, (r.moveLeft j).birthday_congr.symm⟩
    · exact ⟨_, (r.moveLeftSymm j).birthday_congr⟩
    · exact ⟨_, (r.moveRight j).birthday_congr.symm⟩
    · exact ⟨_, (r.moveRightSymm j).birthday_congr⟩

Proof state:
case e_a.h
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => (xR i).birthday) ↔ i ∈ Set.range fun i => (yR i).birthday

Tactic:
constructor

Result:
case e_a.h.mp
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => (xR i).birthday) → i ∈ Set.range fun i => (yR i).birthday

case e_a.h.mpr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => (yR i).birthday) → i ∈ Set.range fun i => (xR i).birthday

Proof state:
case e_a.h.mpr.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : yr
⊢ (fun i => (yR i).birthday) j ∈ Set.range fun i => (xR i).birthday

Tactic:
exact ⟨_, (r.moveRightSymm j).birthday_congr⟩

Result:
no goals

Proof state:
case e_a.h.mp
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => (xL i).birthday) → i ∈ Set.range fun i => (yL i).birthday

case e_a.h.mpr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => (yL i).birthday) → i ∈ Set.range fun i => (xL i).birthday

case e_a.h.mp
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => (xR i).birthday) → i ∈ Set.range fun i => (yR i).birthday

case e_a.h.mpr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => (yR i).birthday) → i ∈ Set.range fun i => (xR i).birthday

Tactic:
all_goals rintro ⟨j, rfl⟩

Result:
case e_a.h.mp.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : xl
⊢ (fun i => (xL i).birthday) j ∈ Set.range fun i => (yL i).birthday

case e_a.h.mpr.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : yl
⊢ (fun i => (yL i).birthday) j ∈ Set.range fun i => (xL i).birthday

case e_a.h.mp.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : xr
⊢ (fun i => (xR i).birthday) j ∈ Set.range fun i => (yR i).birthday

case e_a.h.mpr.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : yr
⊢ (fun i => (yR i).birthday) j ∈ Set.range fun i => (xR i).birthday

Proof state:
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (PGame.mk xl xr xL xR).birthday = (PGame.mk yl yr yL yR).birthday

Tactic:
unfold birthday

Result:
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ ((lsub fun i => (xL i).birthday) ⊔ lsub fun i => (xR i).birthday) =
    (lsub fun i => (yL i).birthday) ⊔ lsub fun i => (yR i).birthday

Proof state:
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (lsub fun i => (xR i).birthday) = lsub fun i => (yR i).birthday

Tactic:
apply lsub_eq_of_range_eq.{u, u, u}

Result:
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (Set.range fun i => (xR i).birthday) = Set.range fun i => (yR i).birthday

Proof state:
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (lsub fun i => (xL i).birthday) = lsub fun i => (yL i).birthday

case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (lsub fun i => (xR i).birthday) = lsub fun i => (yR i).birthday

Tactic:
all_goals
  apply lsub_eq_of_range_eq.{u, u, u}
  ext i; constructor

Result:
case e_a.h.mp
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => (xL i).birthday) → i ∈ Set.range fun i => (yL i).birthday

case e_a.h.mpr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => (yL i).birthday) → i ∈ Set.range fun i => (xL i).birthday

case e_a.h.mp
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => (xR i).birthday) → i ∈ Set.range fun i => (yR i).birthday

case e_a.h.mpr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => (yR i).birthday) → i ∈ Set.range fun i => (xR i).birthday

Proof state:
case e_a.h.mpr.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : yl
⊢ (fun i => (yL i).birthday) j ∈ Set.range fun i => (xL i).birthday

Tactic:
exact ⟨_, (r.moveLeftSymm j).birthday_congr⟩

Result:
no goals

Proof state:
case e_a.h.mpr
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => (yR i).birthday) → i ∈ Set.range fun i => (xR i).birthday

Tactic:
rintro ⟨j, rfl⟩

Result:
case e_a.h.mpr.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : yr
⊢ (fun i => (yR i).birthday) j ∈ Set.range fun i => (xR i).birthday

Proof state:
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ ((lsub fun i => (xL i).birthday) ⊔ lsub fun i => (xR i).birthday) =
    (lsub fun i => (yL i).birthday) ⊔ lsub fun i => (yR i).birthday

Tactic:
congr 1

Result:
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (lsub fun i => (xL i).birthday) = lsub fun i => (yL i).birthday

case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (lsub fun i => (xR i).birthday) = lsub fun i => (yR i).birthday