Lean4
theorem quot_mul_assoc (x y z : PGame) : (⟦x * y * z⟧ : Game) = ⟦x * (y * 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: as above, increased the `maxDepth` here by 1.
solve_by_elim (maxDepth := 8) [Sum.inl, Sum.inr, Prod.mk]
·
rintro (⟨_, ⟨_, _⟩ | ⟨_, _⟩⟩ | ⟨_, ⟨_, _⟩ | ⟨_, _⟩⟩) <;>
solve_by_elim (maxDepth := 8) [Sum.inl, Sum.inr, Prod.mk]
· rintro (⟨⟨_, _⟩ | ⟨_, _⟩, _⟩ | ⟨⟨_, _⟩ | ⟨_, _⟩, _⟩) <;> rfl
· rintro (⟨_, ⟨_, _⟩ | ⟨_, _⟩⟩ | ⟨_, ⟨_, _⟩ | ⟨_, _⟩⟩) <;> rfl
· fconstructor
·
rintro (⟨⟨_, _⟩ | ⟨_, _⟩, _⟩ | ⟨⟨_, _⟩ | ⟨_, _⟩, _⟩) <;>
solve_by_elim (maxDepth := 8) [Sum.inl, Sum.inr, Prod.mk]
·
rintro (⟨_, ⟨_, _⟩ | ⟨_, _⟩⟩ | ⟨_, ⟨_, _⟩ | ⟨_, _⟩⟩) <;>
solve_by_elim (maxDepth := 8) [Sum.inl, Sum.inr, Prod.mk]
· rintro (⟨⟨_, _⟩ | ⟨_, _⟩, _⟩ | ⟨⟨_, _⟩ | ⟨_, _⟩, _⟩) <;> rfl
·
rintro (⟨_, ⟨_, _⟩ | ⟨_, _⟩⟩ | ⟨_, ⟨_, _⟩ | ⟨_, _⟩⟩) <;>
rfl
-- Porting note: explicitly wrote out arguments to each recursive
-- quot_mul_assoc reference below, because otherwise the decreasing_by block
-- failed. Each branch previously ended with: `simp [quot_mul_assoc]; abel`
-- See https://github.com/leanprover/lean4/issues/2288
· rintro (⟨⟨i, j⟩ | ⟨i, j⟩, k⟩ | ⟨⟨i, j⟩ | ⟨i, j⟩, k⟩)
· change
⟦(xL i * y + x * yL j - xL i * yL j) * z + x * y * zL k - (xL i * y + x * yL j - xL i * yL j) * zL k⟧ =
⟦xL i * (y * z) + x * (yL j * z + y * zL k - yL j * zL k) - xL i * (yL j * z + y * zL k - yL j * zL k)⟧
simp only [quot_sub, quot_add, quot_right_distrib_sub, quot_right_distrib, quot_left_distrib_sub,
quot_left_distrib]
rw [quot_mul_assoc (xL i) (mk yl yr yL yR) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (yL j) (mk zl zr zL zR)]
rw [quot_mul_assoc (xL i) (yL j) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (mk yl yr yL yR) (zL k)]
rw [quot_mul_assoc (xL i) (mk yl yr yL yR) (zL k)]
rw [quot_mul_assoc (mk xl xr xL xR) (yL j) (zL k)]
rw [quot_mul_assoc (xL i) (yL j) (zL k)]
abel
· change
⟦(xR i * y + x * yR j - xR i * yR j) * z + x * y * zL k - (xR i * y + x * yR j - xR i * yR j) * zL k⟧ =
⟦xR i * (y * z) + x * (yR j * z + y * zL k - yR j * zL k) - xR i * (yR j * z + y * zL k - yR j * zL k)⟧
simp only [quot_sub, quot_add, quot_right_distrib_sub, quot_right_distrib, quot_left_distrib_sub,
quot_left_distrib]
rw [quot_mul_assoc (xR i) (mk yl yr yL yR) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (yR j) (mk zl zr zL zR)]
rw [quot_mul_assoc (xR i) (yR j) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (mk yl yr yL yR) (zL k)]
rw [quot_mul_assoc (xR i) (mk yl yr yL yR) (zL k)]
rw [quot_mul_assoc (mk xl xr xL xR) (yR j) (zL k)]
rw [quot_mul_assoc (xR i) (yR j) (zL k)]
abel
· change
⟦(xL i * y + x * yR j - xL i * yR j) * z + x * y * zR k - (xL i * y + x * yR j - xL i * yR j) * zR k⟧ =
⟦xL i * (y * z) + x * (yR j * z + y * zR k - yR j * zR k) - xL i * (yR j * z + y * zR k - yR j * zR k)⟧
simp only [quot_sub, quot_add, quot_right_distrib_sub, quot_right_distrib, quot_left_distrib_sub,
quot_left_distrib]
rw [quot_mul_assoc (xL i) (mk yl yr yL yR) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (yR j) (mk zl zr zL zR)]
rw [quot_mul_assoc (xL i) (yR j) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (mk yl yr yL yR) (zR k)]
rw [quot_mul_assoc (xL i) (mk yl yr yL yR) (zR k)]
rw [quot_mul_assoc (mk xl xr xL xR) (yR j) (zR k)]
rw [quot_mul_assoc (xL i) (yR j) (zR k)]
abel
· change
⟦(xR i * y + x * yL j - xR i * yL j) * z + x * y * zR k - (xR i * y + x * yL j - xR i * yL j) * zR k⟧ =
⟦xR i * (y * z) + x * (yL j * z + y * zR k - yL j * zR k) - xR i * (yL j * z + y * zR k - yL j * zR k)⟧
simp only [quot_sub, quot_add, quot_right_distrib_sub, quot_right_distrib, quot_left_distrib_sub,
quot_left_distrib]
rw [quot_mul_assoc (xR i) (mk yl yr yL yR) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (yL j) (mk zl zr zL zR)]
rw [quot_mul_assoc (xR i) (yL j) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (mk yl yr yL yR) (zR k)]
rw [quot_mul_assoc (xR i) (mk yl yr yL yR) (zR k)]
rw [quot_mul_assoc (mk xl xr xL xR) (yL j) (zR k)]
rw [quot_mul_assoc (xR i) (yL j) (zR k)]
abel
· rintro (⟨⟨i, j⟩ | ⟨i, j⟩, k⟩ | ⟨⟨i, j⟩ | ⟨i, j⟩, k⟩)
· change
⟦(xL i * y + x * yL j - xL i * yL j) * z + x * y * zR k - (xL i * y + x * yL j - xL i * yL j) * zR k⟧ =
⟦xL i * (y * z) + x * (yL j * z + y * zR k - yL j * zR k) - xL i * (yL j * z + y * zR k - yL j * zR k)⟧
simp only [quot_sub, quot_add, quot_right_distrib_sub, quot_right_distrib, quot_left_distrib_sub,
quot_left_distrib]
rw [quot_mul_assoc (xL i) (mk yl yr yL yR) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (yL j) (mk zl zr zL zR)]
rw [quot_mul_assoc (xL i) (yL j) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (mk yl yr yL yR) (zR k)]
rw [quot_mul_assoc (xL i) (mk yl yr yL yR) (zR k)]
rw [quot_mul_assoc (mk xl xr xL xR) (yL j) (zR k)]
rw [quot_mul_assoc (xL i) (yL j) (zR k)]
abel
· change
⟦(xR i * y + x * yR j - xR i * yR j) * z + x * y * zR k - (xR i * y + x * yR j - xR i * yR j) * zR k⟧ =
⟦xR i * (y * z) + x * (yR j * z + y * zR k - yR j * zR k) - xR i * (yR j * z + y * zR k - yR j * zR k)⟧
simp only [quot_sub, quot_add, quot_right_distrib_sub, quot_right_distrib, quot_left_distrib_sub,
quot_left_distrib]
rw [quot_mul_assoc (xR i) (mk yl yr yL yR) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (yR j) (mk zl zr zL zR)]
rw [quot_mul_assoc (xR i) (yR j) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (mk yl yr yL yR) (zR k)]
rw [quot_mul_assoc (xR i) (mk yl yr yL yR) (zR k)]
rw [quot_mul_assoc (mk xl xr xL xR) (yR j) (zR k)]
rw [quot_mul_assoc (xR i) (yR j) (zR k)]
abel
· change
⟦(xL i * y + x * yR j - xL i * yR j) * z + x * y * zL k - (xL i * y + x * yR j - xL i * yR j) * zL k⟧ =
⟦xL i * (y * z) + x * (yR j * z + y * zL k - yR j * zL k) - xL i * (yR j * z + y * zL k - yR j * zL k)⟧
simp only [quot_sub, quot_add, quot_right_distrib_sub, quot_right_distrib, quot_left_distrib_sub,
quot_left_distrib]
rw [quot_mul_assoc (xL i) (mk yl yr yL yR) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (yR j) (mk zl zr zL zR)]
rw [quot_mul_assoc (xL i) (yR j) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (mk yl yr yL yR) (zL k)]
rw [quot_mul_assoc (xL i) (mk yl yr yL yR) (zL k)]
rw [quot_mul_assoc (mk xl xr xL xR) (yR j) (zL k)]
rw [quot_mul_assoc (xL i) (yR j) (zL k)]
abel
· change
⟦(xR i * y + x * yL j - xR i * yL j) * z + x * y * zL k - (xR i * y + x * yL j - xR i * yL j) * zL k⟧ =
⟦xR i * (y * z) + x * (yL j * z + y * zL k - yL j * zL k) - xR i * (yL j * z + y * zL k - yL j * zL k)⟧
simp only [quot_sub, quot_add, quot_right_distrib_sub, quot_right_distrib, quot_left_distrib_sub,
quot_left_distrib]
rw [quot_mul_assoc (xR i) (mk yl yr yL yR) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (yL j) (mk zl zr zL zR)]
rw [quot_mul_assoc (xR i) (yL j) (mk zl zr zL zR)]
rw [quot_mul_assoc (mk xl xr xL xR) (mk yl yr yL yR) (zL k)]
rw [quot_mul_assoc (xR i) (mk yl yr yL yR) (zL k)]
rw [quot_mul_assoc (mk xl xr xL xR) (yL j) (zL k)]
rw [quot_mul_assoc (xR i) (yL j) (zL k)]
abel
termination_by (x, y, z)
