Base-5 6D No-Carry Rigidity

import Mathlib

theorem base5_projection_no_carry_6d (x y z : Fin 6 → ℕ) (hx : ∀ i, x i ≤ 2) (hy : ∀ i, y i ≤ 2) (hz : ∀ i, z i ≤ 2) (h_proj : (x 0 + x 1 * 5 + x 2 * 25 + x 3 * 125 + x 4 * 625 + x 5 * 3125) + (z 0 + z 1 * 5 + z 2 * 25 + z 3 * 125 + z 4 * 625 + z 5 * 3125) = 2 * (y 0 + y 1 * 5 + y 2 * 25 + y 3 * 125 + y 4 * 625 + y 5 * 3125)) : ∀ i : Fin 6, x i + z i = 2 * y i := by sorry