-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_nmul (a b : Ordinal) : (a ⨳ b).toPGame ≈ a.toPGame * b.toPGame

Proof state:
a b : Ordinal.{u_1}
i✝ : (a.toPGame * b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
j : b.toPGame.LeftMoves
⊢ (a.toPGame * b.toPGame).moveLeft (toLeftMovesMul (Sum.inl (i, j))) ⧏ (a ⨳ b).toPGame

Tactic:
rw [mul_moveLeft_inl, toPGame_moveLeft', toPGame_moveLeft', lf_iff_game_lf,
  quot_sub, quot_add, ← Game.not_le, le_sub_iff_add_le]

Result:
a b : Ordinal.{u_1}
i✝ : (a.toPGame * b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
j : b.toPGame.LeftMoves
⊢ ¬⟦(a ⨳ b).toPGame⟧ + ⟦(↑(toLeftMovesToPGame.symm i)).toPGame * (↑(toLeftMovesToPGame.symm j)).toPGame⟧ ≤
      ⟦(↑(toLeftMovesToPGame.symm i)).toPGame * b.toPGame⟧ + ⟦a.toPGame * (↑(toLeftMovesToPGame.symm j)).toPGame⟧

Proof state:
case refine_1.intro.intro.intro.intro
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
h : toGame ↑(toLeftMovesToPGame.symm i) ≤ toGame (c ⨳ b) + toGame (a ⨳ d) - toGame (c ⨳ d)
⊢ ⟦(c ⨳ b).toPGame⟧ + ⟦(a ⨳ d).toPGame⟧ - ⟦(c ⨳ d).toPGame⟧ = ⟦(c ⨳ b).toPGame⟧ + ⟦(a ⨳ d).toPGame⟧ + ⟦-(c ⨳ d).toPGame⟧

Tactic:
rfl

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
h : toGame ↑(toLeftMovesToPGame.symm i) ≤ toGame (c ⨳ b) + toGame (a ⨳ d) - toGame (c ⨳ d)
⊢ (a.toPGame * b.toPGame).moveLeft (toLeftMovesMul (Sum.inl (toLeftMovesToPGame ⟨c, hc⟩, toLeftMovesToPGame ⟨d, hd⟩))) ≈
    (c ⨳ b).toPGame + (a ⨳ d).toPGame + -(c ⨳ d).toPGame

Tactic:
simp only [mul_moveLeft_inl, toPGame_moveLeft', Equiv.symm_apply_apply, equiv_iff_game_eq,
  quot_sub, quot_add]

Result:
case refine_1.intro.intro.intro.intro
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
h : toGame ↑(toLeftMovesToPGame.symm i) ≤ toGame (c ⨳ b) + toGame (a ⨳ d) - toGame (c ⨳ d)
⊢ ⟦c.toPGame * b.toPGame⟧ + ⟦a.toPGame * d.toPGame⟧ - ⟦c.toPGame * d.toPGame⟧ =
    ⟦(c ⨳ b).toPGame⟧ + ⟦(a ⨳ d).toPGame⟧ + ⟦-(c ⨳ d).toPGame⟧

Proof state:
case refine_1.intro.intro.intro.intro
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
h : toGame ↑(toLeftMovesToPGame.symm i) ≤ toGame (c ⨳ b) + toGame (a ⨳ d) - toGame (c ⨳ d)
⊢ (↑(toLeftMovesToPGame.symm i)).toPGame ⧏ a.toPGame * b.toPGame

Tactic:
refine lf_of_le_of_lf h <| (lf_congr_left ?_).1 <| moveLeft_lf <| toLeftMovesMul <| Sum.inl
  ⟨toLeftMovesToPGame ⟨c, hc⟩, toLeftMovesToPGame ⟨d, hd⟩⟩

Result:
case refine_1.intro.intro.intro.intro
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
h : toGame ↑(toLeftMovesToPGame.symm i) ≤ toGame (c ⨳ b) + toGame (a ⨳ d) - toGame (c ⨳ d)
⊢ (a.toPGame * b.toPGame).moveLeft (toLeftMovesMul (Sum.inl (toLeftMovesToPGame ⟨c, hc⟩, toLeftMovesToPGame ⟨d, hd⟩))) ≈
    (c ⨳ b).toPGame + (a ⨳ d).toPGame + -(c ⨳ d).toPGame

Proof state:
case refine_1
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
⊢ (a ⨳ b).toPGame.moveLeft i ⧏ a.toPGame * b.toPGame

Tactic:
rw [toPGame_moveLeft']

Result:
case refine_1
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
⊢ (↑(toLeftMovesToPGame.symm i)).toPGame ⧏ a.toPGame * b.toPGame

Proof state:
a b : Ordinal.{u_1}
i✝ : (a.toPGame * b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
j : b.toPGame.LeftMoves
⊢ ¬⟦(a ⨳ b).toPGame⟧ + ⟦(↑(toLeftMovesToPGame.symm i)).toPGame * (↑(toLeftMovesToPGame.symm j)).toPGame⟧ ≤
      ⟦(↑(toLeftMovesToPGame.symm i)).toPGame * b.toPGame⟧ + ⟦a.toPGame * (↑(toLeftMovesToPGame.symm j)).toPGame⟧

Tactic:
repeat rw [← game_eq (toPGame_nmul _ _)]

Result:
a b : Ordinal.{u_1}
i✝ : (a.toPGame * b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
j : b.toPGame.LeftMoves
⊢ ¬⟦(a ⨳ b).toPGame⟧ + ⟦(↑(toLeftMovesToPGame.symm i) ⨳ ↑(toLeftMovesToPGame.symm j)).toPGame⟧ ≤
      ⟦(↑(toLeftMovesToPGame.symm i) ⨳ b).toPGame⟧ + ⟦(a ⨳ ↑(toLeftMovesToPGame.symm j)).toPGame⟧

Proof state:
case refine_1.intro.intro.intro.intro
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
h : toGame ↑(toLeftMovesToPGame.symm i) ≤ toGame (c ⨳ b) + toGame (a ⨳ d) - toGame (c ⨳ d)
⊢ ⟦(c ⨳ b).toPGame⟧ + ⟦(a ⨳ d).toPGame⟧ - ⟦c.toPGame * d.toPGame⟧ =
    ⟦(c ⨳ b).toPGame⟧ + ⟦(a ⨳ d).toPGame⟧ + ⟦-(c ⨳ d).toPGame⟧

Tactic:
rw [← game_eq (toPGame_nmul _ _)]

Result:
case refine_1.intro.intro.intro.intro
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
h : toGame ↑(toLeftMovesToPGame.symm i) ≤ toGame (c ⨳ b) + toGame (a ⨳ d) - toGame (c ⨳ d)
⊢ ⟦(c ⨳ b).toPGame⟧ + ⟦(a ⨳ d).toPGame⟧ - ⟦(c ⨳ d).toPGame⟧ = ⟦(c ⨳ b).toPGame⟧ + ⟦(a ⨳ d).toPGame⟧ + ⟦-(c ⨳ d).toPGame⟧

Proof state:
a b : Ordinal.{u_1}
i : (a.toPGame * b.toPGame).LeftMoves
⊢ ∀ (ix : a.toPGame.LeftMoves) (iy : b.toPGame.LeftMoves),
    (a.toPGame * b.toPGame).moveLeft (toLeftMovesMul (Sum.inl (ix, iy))) ⧏ (a ⨳ b).toPGame

Tactic:
intro i j

Result:
a b : Ordinal.{u_1}
i✝ : (a.toPGame * b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
j : b.toPGame.LeftMoves
⊢ (a.toPGame * b.toPGame).moveLeft (toLeftMovesMul (Sum.inl (i, j))) ⧏ (a ⨳ b).toPGame

Proof state:
a b : Ordinal.{u_1}
⊢ (a ⨳ b).toPGame ≈ a.toPGame * b.toPGame

Tactic:
refine ⟨le_of_forall_lf (fun i => ?_) isEmptyElim, le_of_forall_lf (fun i => ?_) isEmptyElim⟩

Result:
case refine_1
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
⊢ (a ⨳ b).toPGame.moveLeft i ⧏ a.toPGame * b.toPGame

case refine_2
a b : Ordinal.{u_1}
i : (a.toPGame * b.toPGame).LeftMoves
⊢ (a.toPGame * b.toPGame).moveLeft i ⧏ (a ⨳ b).toPGame

Proof state:
case refine_1.intro.intro.intro.intro
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
h : toGame ↑(toLeftMovesToPGame.symm i) ≤ toGame (c ⨳ b) + toGame (a ⨳ d) - toGame (c ⨳ d)
⊢ ⟦c.toPGame * b.toPGame⟧ + ⟦a.toPGame * d.toPGame⟧ - ⟦c.toPGame * d.toPGame⟧ =
    ⟦(c ⨳ b).toPGame⟧ + ⟦(a ⨳ d).toPGame⟧ + ⟦-(c ⨳ d).toPGame⟧

Tactic:
repeat rw [← game_eq (toPGame_nmul _ _)]

Result:
case refine_1.intro.intro.intro.intro
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
h : toGame ↑(toLeftMovesToPGame.symm i) ≤ toGame (c ⨳ b) + toGame (a ⨳ d) - toGame (c ⨳ d)
⊢ ⟦(c ⨳ b).toPGame⟧ + ⟦(a ⨳ d).toPGame⟧ - ⟦(c ⨳ d).toPGame⟧ = ⟦(c ⨳ b).toPGame⟧ + ⟦(a ⨳ d).toPGame⟧ + ⟦-(c ⨳ d).toPGame⟧

Proof state:
a b : Ordinal.{u_1}
i✝ : (a.toPGame * b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
j : b.toPGame.LeftMoves
⊢ ¬⟦(a ⨳ b).toPGame⟧ + ⟦(↑(toLeftMovesToPGame.symm i) ⨳ ↑(toLeftMovesToPGame.symm j)).toPGame⟧ ≤
      ⟦(↑(toLeftMovesToPGame.symm i) ⨳ b).toPGame⟧ + ⟦(a ⨳ ↑(toLeftMovesToPGame.symm j)).toPGame⟧

Tactic:
simp_rw [mk_toPGame, ← toGame_nadd]

Result:
a b : Ordinal.{u_1}
i✝ : (a.toPGame * b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
j : b.toPGame.LeftMoves
⊢ ¬toGame (a ⨳ b ♯ ↑(toLeftMovesToPGame.symm i) ⨳ ↑(toLeftMovesToPGame.symm j)) ≤
      toGame (↑(toLeftMovesToPGame.symm i) ⨳ b ♯ a ⨳ ↑(toLeftMovesToPGame.symm j))

Proof state:
case refine_1.intro.intro.intro.intro
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
h : ↑(toLeftMovesToPGame.symm i) ♯ c ⨳ d ≤ c ⨳ b ♯ a ⨳ d
⊢ (↑(toLeftMovesToPGame.symm i)).toPGame ⧏ a.toPGame * b.toPGame

Tactic:
rw [← toPGame_le_iff, le_iff_game_le, mk_toPGame, mk_toPGame, toGame_nadd _ _, toGame_nadd _ _,
  ← le_sub_iff_add_le] at h

Result:
case refine_1.intro.intro.intro.intro
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
h : toGame ↑(toLeftMovesToPGame.symm i) ≤ toGame (c ⨳ b) + toGame (a ⨳ d) - toGame (c ⨳ d)
⊢ (↑(toLeftMovesToPGame.symm i)).toPGame ⧏ a.toPGame * b.toPGame