-- Mathlib/SetTheory/Game/Basic.lean
theorem quot_left_distrib (x y z : PGame) : (⟦x * (y + z)⟧ : Game) = ⟦x * y⟧ + ⟦x * z⟧ :=
  match x, y, z with
  | mk xl xr xL xR, mk yl yr yL yR, mk zl zr zL zR => by
    let x := mk xl xr xL xR
    let y := mk yl yr yL yR
    let z := mk zl zr zL zR
    refine quot_eq_of_mk'_quot_eq ?_ ?_ ?_ ?_
    · fconstructor
      · rintro (⟨_, _ | _⟩ | ⟨_, _ | _⟩) <;>
          -- Porting note: we've increased `maxDepth` here from `5` to `6`.
          -- Likely this sort of off-by-one error is just a change in the implementation
          -- of `solve_by_elim`.
          solve_by_elim (config := { maxDepth := 6 }) [Sum.inl, Sum.inr, Prod.mk]
      · rintro (⟨⟨_, _⟩ | ⟨_, _⟩⟩ | ⟨_, _⟩ | ⟨_, _⟩) <;>
          solve_by_elim (config := { maxDepth := 6 }) [Sum.inl, Sum.inr, Prod.mk]
      · rintro (⟨_, _ | _⟩ | ⟨_, _ | _⟩) <;> rfl
      · rintro (⟨⟨_, _⟩ | ⟨_, _⟩⟩ | ⟨_, _⟩ | ⟨_, _⟩) <;> rfl
    · fconstructor
      · rintro (⟨_, _ | _⟩ | ⟨_, _ | _⟩) <;>
          solve_by_elim (config := { maxDepth := 6 }) [Sum.inl, Sum.inr, Prod.mk]
      · rintro (⟨⟨_, _⟩ | ⟨_, _⟩⟩ | ⟨_, _⟩ | ⟨_, _⟩) <;>
          solve_by_elim (config := { maxDepth := 6 }) [Sum.inl, Sum.inr, Prod.mk]
      · rintro (⟨_, _ | _⟩ | ⟨_, _ | _⟩) <;> rfl
      · rintro (⟨⟨_, _⟩ | ⟨_, _⟩⟩ | ⟨_, _⟩ | ⟨_, _⟩) <;> rfl
    -- Porting note: explicitly wrote out arguments to each recursive
    -- quot_left_distrib reference below, because otherwise the decreasing_by block
    -- failed. Previously, each branch ended with: `simp [quot_left_distrib]; abel`
    -- See https://github.com/leanprover/lean4/issues/2288
    · rintro (⟨i, j | k⟩ | ⟨i, j | k⟩)
      · change
          ⟦xL i * (y + z) + x * (yL j + z) - xL i * (yL j + z)⟧ =
            ⟦xL i * y + x * yL j - xL i * yL j + x * z⟧
        simp only [quot_sub, quot_add]
        rw [quot_left_distrib (xL i) (mk yl yr yL yR) (mk zl zr zL zR)]
        rw [quot_left_distrib (mk xl xr xL xR) (yL j) (mk zl zr zL zR)]
        rw [quot_left_distrib (xL i) (yL j) (mk zl zr zL zR)]
        abel
      · change
          ⟦xL i * (y + z) + x * (y + zL k) - xL i * (y + zL k)⟧ =
            ⟦x * y + (xL i * z + x * zL k - xL i * zL k)⟧
        simp only [quot_sub, quot_add]
        rw [quot_left_distrib (xL i) (mk yl yr yL yR) (mk zl zr zL zR)]
        rw [quot_left_distrib (mk xl xr xL xR) (mk yl yr yL yR) (zL k)]
        rw [quot_left_distrib (xL i) (mk yl yr yL yR) (zL k)]
        abel
      · change
          ⟦xR i * (y + z) + x * (yR j + z) - xR i * (yR j + z)⟧ =
            ⟦xR i * y + x * yR j - xR i * yR j + x * z⟧
        simp only [quot_sub, quot_add]
        rw [quot_left_distrib (xR i) (mk yl yr yL yR) (mk zl zr zL zR)]
        rw [quot_left_distrib (mk xl xr xL xR) (yR j) (mk zl zr zL zR)]
        rw [quot_left_distrib (xR i) (yR j) (mk zl zr zL zR)]
        abel
      · change
          ⟦xR i * (y + z) + x * (y + zR k) - xR i * (y + zR k)⟧ =
            ⟦x * y + (xR i * z + x * zR k - xR i * zR k)⟧
        simp only [quot_sub, quot_add]
        rw [quot_left_distrib (xR i) (mk yl yr yL yR) (mk zl zr zL zR)]
        rw [quot_left_distrib (mk xl xr xL xR) (mk yl yr yL yR) (zR k)]
        rw [quot_left_distrib (xR i) (mk yl yr yL yR) (zR k)]
        abel
    · rintro (⟨i, j | k⟩ | ⟨i, j | k⟩)
      · change
          ⟦xL i * (y + z) + x * (yR j + z) - xL i * (yR j + z)⟧ =
            ⟦xL i * y + x * yR j - xL i * yR j + x * z⟧
        simp only [quot_sub, quot_add]
        rw [quot_left_distrib (xL i) (mk yl yr yL yR) (mk zl zr zL zR)]
        rw [quot_left_distrib (mk xl xr xL xR) (yR j) (mk zl zr zL zR)]
        rw [quot_left_distrib (xL i) (yR j) (mk zl zr zL zR)]
        abel
      · change
          ⟦xL i * (y + z) + x * (y + zR k) - xL i * (y + zR k)⟧ =
            ⟦x * y + (xL i * z + x * zR k - xL i * zR k)⟧
        simp only [quot_sub, quot_add]
        rw [quot_left_distrib (xL i) (mk yl yr yL yR) (mk zl zr zL zR)]
        rw [quot_left_distrib (mk xl xr xL xR) (mk yl yr yL yR) (zR k)]
 

Proof state:
case refine_4.inr.mk.inr
x✝ y✝ z✝ : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
x : PGame := mk xl xr xL xR
y : PGame := mk yl yr yL yR
z : PGame := mk zl zr zL zR
i : xr
k : zl
⊢ ⟦xR i * (y + z)⟧ + ⟦x * (y + zL k)⟧ - ⟦xR i * (y + zL k)⟧ = ⟦x * y⟧ + (⟦xR i * z⟧ + ⟦x * zL k⟧ - ⟦xR i * zL k⟧)

Tactic:
rw [quot_left_distrib (xR i) (mk yl yr yL yR) (mk zl zr zL zR)]

Result:
case refine_4.inr.mk.inr
x✝ y✝ z✝ : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
x : PGame := mk xl xr xL xR
y : PGame := mk yl yr yL yR
z : PGame := mk zl zr zL zR
i : xr
k : zl
⊢ ⟦xR i * mk yl yr yL yR⟧ + ⟦xR i * mk zl zr zL zR⟧ + ⟦x * (y + zL k)⟧ - ⟦xR i * (y + zL k)⟧ =
    ⟦x * y⟧ + (⟦xR i * z⟧ + ⟦x * zL k⟧ - ⟦xR i * zL k⟧)

Proof state:
case refine_1
x✝ y✝ z✝ : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
x : PGame := mk xl xr xL xR
y : PGame := mk yl yr yL yR
z : PGame := mk zl zr zL zR
⊢ (mk xl xr xL xR * (mk yl yr yL yR + mk zl zr zL zR)).LeftMoves ≃
    (mk xl xr xL xR * mk yl yr yL yR + mk xl xr xL xR * mk zl zr zL zR).LeftMoves

Tactic:
fconstructor

Result:
case refine_1.toFun
x✝ y✝ z✝ : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
x : PGame := mk xl xr xL xR
y : PGame := mk yl yr yL yR
z : PGame := mk zl zr zL zR
⊢ (mk xl xr xL xR * (mk yl yr yL yR + mk zl zr zL zR)).LeftMoves →
    (mk xl xr xL xR * mk yl yr yL yR + mk xl xr xL xR * mk zl zr zL zR).LeftMoves

case refine_1.invFun
x✝ y✝ z✝ : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
x : PGame := mk xl xr xL xR
y : PGame := mk yl yr yL yR
z : PGame := mk zl zr zL zR
⊢ (mk xl xr xL xR * mk yl yr yL yR + mk xl xr xL xR * mk zl zr zL zR).LeftMoves →
    (mk xl xr xL xR * (mk yl yr yL yR + mk zl zr zL zR)).LeftMoves

case refine_1.left_inv
x✝ y✝ z✝ : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
x : PGame := mk xl xr xL xR
y : PGame := mk yl yr yL yR
z : PGame := mk zl zr zL zR
⊢ LeftInverse ?refine_1.invFun ?refine_1.toFun

case refine_1.right_inv
x✝ y✝ z✝ : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
x : PGame := mk xl xr xL xR
y : PGame := mk yl yr yL yR
z : PGame := mk zl zr zL zR
⊢ RightInverse ?refine_1.invFun ?refine_1.toFun

Proof state:
case refine_3.inr.mk.inr
x✝ y✝ z✝ : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
x : PGame := mk xl xr xL xR
y : PGame := mk yl yr yL yR
z : PGame := mk zl zr zL zR
i : xr
k : zr
⊢ ⟦xR i * mk yl yr yL yR⟧ + ⟦xR i * mk zl zr zL zR⟧ + (⟦mk xl xr xL xR * mk yl yr yL yR⟧ + ⟦mk xl xr xL xR * zR k⟧) -
      (⟦xR i * mk yl yr yL yR⟧ + ⟦xR i * zR k⟧) =
    ⟦x * y⟧ + (⟦xR i * z⟧ + ⟦x * zR k⟧ - ⟦xR i * zR k⟧)

Tactic:
abel

Result:
no goals

Proof state:
case refine_4.inl.mk.inl
x✝ y✝ z✝ : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
x : PGame := mk xl xr xL xR
y : PGame := mk yl yr yL yR
z : PGame := mk zl zr zL zR
i : xl
j : yr
⊢ ⟦xL i * mk yl yr yL yR⟧ + ⟦xL i * mk zl zr zL zR⟧ + (⟦mk xl xr xL xR * yR j⟧ + ⟦mk xl xr xL xR * mk zl zr zL zR⟧) -
      (⟦xL i * yR j⟧ + ⟦xL i * mk zl zr zL zR⟧) =
    ⟦xL i * y⟧ + ⟦x * yR j⟧ - ⟦xL i * yR j⟧ + ⟦x * z⟧

Tactic:
abel

Result:
no goals