English
Quotient of x times (y+z) equals quotient of x*y plus quotient of x*z.
Русский
Часть x*(y+z) равна части x*y плюс части x*z.
LaTeX
$$$[ x \cdot (y+z) ] = [ x \cdot y ] + [ x \cdot z ]$$$
Lean4
@[simp]
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 (maxDepth := 6) [Sum.inl, Sum.inr, Prod.mk]
· rintro (⟨⟨_, _⟩ | ⟨_, _⟩⟩ | ⟨_, _⟩ | ⟨_, _⟩) <;> solve_by_elim (maxDepth := 6) [Sum.inl, Sum.inr, Prod.mk]
· rintro (⟨_, _ | _⟩ | ⟨_, _ | _⟩) <;> rfl
· rintro (⟨⟨_, _⟩ | ⟨_, _⟩⟩ | ⟨_, _⟩ | ⟨_, _⟩) <;> rfl
· fconstructor
· rintro (⟨_, _ | _⟩ | ⟨_, _ | _⟩) <;> solve_by_elim (maxDepth := 6) [Sum.inl, Sum.inr, Prod.mk]
· rintro (⟨⟨_, _⟩ | ⟨_, _⟩⟩ | ⟨_, _⟩ | ⟨_, _⟩) <;> solve_by_elim (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)]
rw [quot_left_distrib (xL i) (mk yl yr yL yR) (zR k)]
abel
· change ⟦xR i * (y + z) + x * (yL j + z) - xR i * (yL j + z)⟧ = ⟦xR i * y + x * yL j - xR i * yL 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) (yL j) (mk zl zr zL zR)]
rw [quot_left_distrib (xR i) (yL j) (mk zl zr zL zR)]
abel
· change ⟦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)⟧
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) (zL k)]
rw [quot_left_distrib (xR i) (mk yl yr yL yR) (zL k)]
abel
termination_by (x, y, z)
