lean_workbook_plus_48042
ProvedLet's number the board from the top leftmost cell to the bottom rightmost cell with numbers from to . The number in cell will be equal to . Each domino will now cover 3 squares that the sum of the numbers in them is divisible by . Since the sum of all the numbers is also divisible by , the number in the leftover cell must be divisible by . Now, each rotation with turn the number in cell from to . If the cell is leftover in the first configuration, then it is still a leftover cell after the rotation. Thus, we have and , or and . Since , so . There are such pairs, account for cells.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48042 (x y : ℕ)
(h₀ : 0 ≤ x ∧ x ≤ 9)
(h₁ : 0 ≤ y ∧ y ≤ 9)
(h₂ : 3 ∣ (10 * x + y))
(h₃ : 3 ∣ (10 * y + (9 - x))) :
x ∈ ({0, 3, 6, 9} : Finset ℕ) ∧ y ∈ ({0, 3, 6, 9} : Finset ℕ) := by sorrySource