A colouring argument in Lean 4

import Mathlib

open scoped BigOperators
open scoped Real
open scoped Nat
open scoped Classical
open scoped Pointwise

set_option maxHeartbeats 8000000
set_option maxRecDepth 4000
set_option synthInstance.maxHeartbeats 20000
set_option synthInstance.maxSize 128

set_option relaxedAutoImplicit false
set_option autoImplicit false

set_option pp.fullNames true
set_option pp.structureInstances true
set_option pp.coercions.types true
set_option pp.funBinderTypes true
set_option pp.letVarTypes true
set_option pp.piBinderTypes true

set_option grind.warning false

/-!
# Breaking a tile: a 2×2 tile and a 4×1 tile are never interchangeable

Suppose a floor (an arbitrary finite region of the square grid) has been tiled by
`4 × 1` tiles and `2 × 2` tiles, and that one tile breaks.  We show that the floor
cannot be retiled if the broken tile is replaced by a tile of the *other* shape.

The proof is the classical colouring argument: give the cell `(x, y)` the weight
`1 ∈ ZMod 2` when both coordinates are even and `0` otherwise.  Every `2 × 2` tile
carries total weight `1`, while every `4 × 1` tile carries total weight `0`.
Hence the parity of the number of `2 × 2` tiles is determined by the region alone,
and it changes when one `2 × 2` tile is traded for a `4 × 1` tile (or conversely).
-/

namespace BrokenTile

/-- The weight of a cell: `1` if both coordinates are even, `0` otherwise.
(Written multiplicatively in `ZMod 2`.) -/
def wt (c : ℤ × ℤ) : ZMod 2 := (1 + (c.1 : ZMod 2)) * (1 + (c.2 : ZMod 2))

/-- The total weight of a finite set of cells. -/
def wtSum (t : Finset (ℤ × ℤ)) : ZMod 2 := ∑ c ∈ t, wt c

/-- `t` is (the set of cells covered by) a `2 × 2` tile. -/
def IsSquareTile (t : Finset (ℤ × ℤ)) : Prop :=
  ∃ a b : ℤ, t = {(a, b), (a + 1, b), (a, b + 1), (a + 1, b + 1)}

/-- `t` is (the set of cells covered by) a `4 × 1` tile, in either orientation. -/
def IsBarTile (t : Finset (ℤ × ℤ)) : Prop :=
  (∃ a b : ℤ, t = {(a, b), (a + 1, b), (a + 2, b), (a + 3, b)}) ∨
  (∃ a b : ℤ, t = {(a, b), (a, b + 1), (a, b + 2), (a, b + 3)})

/-- `T` is a tiling of the region `S`: a family of pairwise disjoint tiles, each of
which is a `2 × 2` or a `4 × 1` tile, whose union is exactly `S`. -/
def IsTiling (S : Finset (ℤ × ℤ)) (T : Finset (Finset (ℤ × ℤ))) : Prop :=
  (∀ t ∈ T, IsSquareTile t ∨ IsBarTile t) ∧
  (T : Set (Finset (ℤ × ℤ))).PairwiseDisjoint id ∧
  S = T.biUnion id

/-- A `2 × 2` tile has odd weight. -/
theorem wtSum_of_isSquareTile {t : Finset (ℤ × ℤ)} (h : IsSquareTile t) : wtSum t = 1 := by
  obtain ⟨a, b, rfl⟩ := h
  rw [wtSum, Finset.sum_insert (by simp [Prod.ext_iff]), Finset.sum_insert (by simp [Prod.ext_iff]),
    Finset.sum_insert (by simp [Prod.ext_iff]), Finset.sum_singleton]
  simp only [wt]
  push_cast
  generalize ((a : ZMod 2)) = x
  generalize ((b : ZMod 2)) = y
  revert x y
  decide

/-- A `4 × 1` tile has even weight. -/
theorem wtSum_of_isBarTile {t : Finset (ℤ × ℤ)} (h : IsBarTile t) : wtSum t = 0 := by
  rcases h with ⟨a, b, rfl⟩ | ⟨a, b, rfl⟩ <;>
  · rw [wtSum, Finset.sum_insert (by simp [Prod.ext_iff]), Finset.sum_insert (by simp [Prod.ext_iff]),
      Finset.sum_insert (by simp [Prod.ext_iff]), Finset.sum_singleton]
    simp only [wt]
    push_cast
    generalize ((a : ZMod 2)) = x
    generalize ((b : ZMod 2)) = y
    revert x y
    decide

/-- The two tile shapes are genuinely different: no set of cells is both. -/
theorem not_isBarTile_of_isSquareTile {t : Finset (ℤ × ℤ)} (h : IsSquareTile t) :
    ¬ IsBarTile t := by
  intro hb
  have := wtSum_of_isBarTile hb
  rw [wtSum_of_isSquareTile h] at this
  exact one_ne_zero this

/-- The weight of the tiled region equals, mod 2, the number of `2 × 2` tiles used. -/
theorem wtSum_eq_card_squares {S : Finset (ℤ × ℤ)} {T : Finset (Finset (ℤ × ℤ))}
    (h : IsTiling S T) : wtSum S = ((T.filter IsSquareTile).card : ZMod 2) := by
  obtain ⟨hshape, hdisj, rfl⟩ := h
  rw [wtSum, Finset.sum_biUnion hdisj]
  simp only [id_eq]
  rw [← Finset.sum_filter_add_sum_filter_not T IsSquareTile]
  have h1 : ∑ t ∈ T.filter IsSquareTile, ∑ c ∈ t, wt c
      = ((T.filter IsSquareTile).card : ZMod 2) := by
    have key : ∀ t ∈ T.filter IsSquareTile, (∑ c ∈ t, wt c) = 1 := by
      intro t ht
      exact wtSum_of_isSquareTile (Finset.mem_filter.mp ht).2
    rw [Finset.sum_congr rfl key]
    simp
  have h2 : ∑ t ∈ T.filter (fun t => ¬ IsSquareTile t), ∑ c ∈ t, wt c = 0 := by
    refine Finset.sum_eq_zero (fun t ht => ?_)
    obtain ⟨htT, hns⟩ := Finset.mem_filter.mp ht
    exact wtSum_of_isBarTile ((hshape t htT).resolve_left hns)
  rw [h1, h2, add_zero]

/-- **Parity invariant.** Any two tilings of the same region use the same number of
`2 × 2` tiles modulo `2`. -/
theorem card_squares_modEq {S : Finset (ℤ × ℤ)} {T₁ T₂ : Finset (Finset (ℤ × ℤ))}
    (h₁ : IsTiling S T₁) (h₂ : IsTiling S T₂) :
    (T₁.filter IsSquareTile).card ≡ (T₂.filter IsSquareTile).card [MOD 2] := by
  have : (((T₁.filter IsSquareTile).card : ℕ) : ZMod 2)
      = (((T₂.filter IsSquareTile).card : ℕ) : ZMod 2) := by
    rw [← wtSum_eq_card_squares h₁, ← wtSum_eq_card_squares h₂]
  exact (ZMod.natCast_eq_natCast_iff _ _ _).mp this

/-- **The broken tile cannot be replaced by one of the other shape.**

If a region `S` is tiled by `T₁`, and `T₂` is another tiling of the same region using
one `2 × 2` tile fewer and one `4 × 1` tile more (or vice versa), we get a
contradiction: so after breaking a tile, no rearrangement using a tile of the other
shape can cover the floor. -/
theorem cannot_swap_tile_shapes {S : Finset (ℤ × ℤ)} {T₁ T₂ : Finset (Finset (ℤ × ℤ))}
    (h₁ : IsTiling S T₁) (h₂ : IsTiling S T₂)
    (hswap :
      ((T₂.filter IsSquareTile).card + 1 = (T₁.filter IsSquareTile).card ∧
        (T₁.filter IsBarTile).card + 1 = (T₂.filter IsBarTile).card) ∨
      ((T₁.filter IsSquareTile).card + 1 = (T₂.filter IsSquareTile).card ∧
        (T₂.filter IsBarTile).card + 1 = (T₁.filter IsBarTile).card)) :
    False := by
  have hpar := card_squares_modEq h₁ h₂
  unfold Nat.ModEq at hpar
  rcases hswap with ⟨h, -⟩ | ⟨h, -⟩ <;> omega

/-- Sanity check: the notion of tiling is not vacuous — a single `2 × 2` tile tiles
the `2 × 2` region, and it uses exactly one square tile. -/
example :
    IsTiling ({(0,0), (1,0), (0,1), (1,1)} : Finset (ℤ × ℤ))
      {({(0,0), (0+1,0), (0,0+1), (0+1,0+1)} : Finset (ℤ × ℤ))} ∧
    (({({(0,0), (0+1,0), (0,0+1), (0+1,0+1)} : Finset (ℤ × ℤ))} :
        Finset (Finset (ℤ × ℤ))).filter IsSquareTile).card = 1 := by
  refine ⟨⟨?_, ?_, ?_⟩, ?_⟩
  · intro t ht
    simp only [Finset.mem_singleton] at ht
    exact Or.inl ⟨0, 0, by rw [ht]⟩
  · simp
  · simp
  · rw [Finset.filter_singleton, if_pos ⟨0, 0, rfl⟩]
    simp

end BrokenTile