[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ (m.fst - 1, m.snd) ∈ Finset.erase b m
[PROOFSTEP]
rw [mem_right] at h 
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.fst - 1, m.snd) ∈ b
⊢ (m.fst - 1, m.snd) ∈ Finset.erase b m
[PROOFSTEP]
apply Finset.mem_erase_of_ne_of_mem _ h.2
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.fst - 1, m.snd) ∈ b
⊢ (m.fst - 1, m.snd) ≠ m
[PROOFSTEP]
exact ne_of_apply_ne Prod.fst (pred_ne_self m.1)
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ (m.fst, m.snd - 1) ∈ Finset.erase b m
[PROOFSTEP]
rw [mem_left] at h 
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.fst, m.snd - 1) ∈ b
⊢ (m.fst, m.snd - 1) ∈ Finset.erase b m
[PROOFSTEP]
apply Finset.mem_erase_of_ne_of_mem _ h.2
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ b ∧ (m.fst, m.snd - 1) ∈ b
⊢ (m.fst, m.snd - 1) ≠ m
[PROOFSTEP]
exact ne_of_apply_ne Prod.snd (pred_ne_self m.2)
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have w₁ : m ∈ b := (Finset.mem_inter.1 h).1
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have w₂ : (m.1, m.2 - 1) ∈ b.erase m := snd_pred_mem_erase_of_mem_left h
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
w₂ : (m.fst, m.snd - 1) ∈ Finset.erase b m
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have i₁ := Finset.card_erase_lt_of_mem w₁
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
w₂ : (m.fst, m.snd - 1) ∈ Finset.erase b m
i₁ : Finset.card (Finset.erase b m) < Finset.card b
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have i₂ := Nat.lt_of_le_of_lt (Nat.zero_le _) (Finset.card_erase_lt_of_mem w₂)
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
w₂ : (m.fst, m.snd - 1) ∈ Finset.erase b m
i₁ : Finset.card (Finset.erase b m) < Finset.card b
i₂ : 0 < Finset.card (Finset.erase b m)
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
exact Nat.lt_of_le_of_lt i₂ i₁
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have w₁ : m ∈ b := (Finset.mem_inter.1 h).1
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have w₂ := fst_pred_mem_erase_of_mem_right h
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
w₂ : (m.fst - 1, m.snd) ∈ Finset.erase b m
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have i₁ := Finset.card_erase_lt_of_mem w₁
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
w₂ : (m.fst - 1, m.snd) ∈ Finset.erase b m
i₁ : Finset.card (Finset.erase b m) < Finset.card b
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
have i₂ := Nat.lt_of_le_of_lt (Nat.zero_le _) (Finset.card_erase_lt_of_mem w₂)
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
w₂ : (m.fst - 1, m.snd) ∈ Finset.erase b m
i₁ : Finset.card (Finset.erase b m) < Finset.card b
i₂ : 0 < Finset.card (Finset.erase b m)
⊢ 2 ≤ Finset.card b
[PROOFSTEP]
exact Nat.lt_of_le_of_lt i₂ i₁
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ Finset.card (moveLeft b m) + 2 = Finset.card b
[PROOFSTEP]
dsimp [moveLeft]
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ Finset.card (Finset.erase (Finset.erase b m) (m.fst, m.snd - 1)) + 2 = Finset.card b
[PROOFSTEP]
rw [Finset.card_erase_of_mem (snd_pred_mem_erase_of_mem_left h)]
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ Finset.card (Finset.erase b m) - 1 + 2 = Finset.card b
[PROOFSTEP]
rw [Finset.card_erase_of_mem (Finset.mem_of_mem_inter_left h)]
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ Finset.card b - 1 - 1 + 2 = Finset.card b
[PROOFSTEP]
exact tsub_add_cancel_of_le (card_of_mem_left h)
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ Finset.card (moveRight b m) + 2 = Finset.card b
[PROOFSTEP]
dsimp [moveRight]
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ Finset.card (Finset.erase (Finset.erase b m) (m.fst - 1, m.snd)) + 2 = Finset.card b
[PROOFSTEP]
rw [Finset.card_erase_of_mem (fst_pred_mem_erase_of_mem_right h)]
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ Finset.card (Finset.erase b m) - 1 + 2 = Finset.card b
[PROOFSTEP]
rw [Finset.card_erase_of_mem (Finset.mem_of_mem_inter_left h)]
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ Finset.card b - 1 - 1 + 2 = Finset.card b
[PROOFSTEP]
exact tsub_add_cancel_of_le (card_of_mem_right h)
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ Finset.card (moveLeft b m) / 2 < Finset.card b / 2
[PROOFSTEP]
simp [← moveLeft_card h, lt_add_one]
[GOAL]
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ Finset.card (moveRight b m) / 2 < Finset.card b / 2
[PROOFSTEP]
simp [← moveRight_card h, lt_add_one]
[GOAL]
s✝ t✝ : Board
m : t✝ ∈ (fun s => Finset.image (moveLeft s) (left s)) s✝
⊢ (fun s => Finset.card s / 2) t✝ < (fun s => Finset.card s / 2) s✝
[PROOFSTEP]
simp only [Finset.mem_image, Prod.exists] at m 
[GOAL]
s✝ t✝ : Board
m : ∃ a b, (a, b) ∈ left s✝ ∧ moveLeft s✝ (a, b) = t✝
⊢ (fun s => Finset.card s / 2) t✝ < (fun s => Finset.card s / 2) s✝
[PROOFSTEP]
rcases m with ⟨_, _, ⟨h, rfl⟩⟩
[GOAL]
case intro.intro.intro
s✝ : Board
w✝¹ w✝ : ℤ
h : (w✝¹, w✝) ∈ left s✝
⊢ (fun s => Finset.card s / 2) (moveLeft s✝ (w✝¹, w✝)) < (fun s => Finset.card s / 2) s✝
[PROOFSTEP]
exact moveLeft_smaller h
[GOAL]
s✝ t✝ : Board
m : t✝ ∈ (fun s => Finset.image (moveRight s) (right s)) s✝
⊢ (fun s => Finset.card s / 2) t✝ < (fun s => Finset.card s / 2) s✝
[PROOFSTEP]
simp only [Finset.mem_image, Prod.exists] at m 
[GOAL]
s✝ t✝ : Board
m : ∃ a b, (a, b) ∈ right s✝ ∧ moveRight s✝ (a, b) = t✝
⊢ (fun s => Finset.card s / 2) t✝ < (fun s => Finset.card s / 2) s✝
[PROOFSTEP]
rcases m with ⟨_, _, ⟨h, rfl⟩⟩
[GOAL]
case intro.intro.intro
s✝ : Board
w✝¹ w✝ : ℤ
h : (w✝¹, w✝) ∈ right s✝
⊢ (fun s => Finset.card s / 2) (moveRight s✝ (w✝¹, w✝)) < (fun s => Finset.card s / 2) s✝
[PROOFSTEP]
exact moveRight_smaller h
[GOAL]
b : Domineering.Board
⊢ Short (domineering b)
[PROOFSTEP]
dsimp [domineering]
[GOAL]
b : Domineering.Board
⊢ Short (ofState b)
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Short domineering.one
[PROOFSTEP]
dsimp [domineering.one]
[GOAL]
⊢ Short (domineering (List.toFinset [(0, 0), (0, 1)]))
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Short domineering.L
[PROOFSTEP]
dsimp [domineering.L]
[GOAL]
⊢ Short (domineering (List.toFinset [(0, 2), (0, 1), (0, 0), (1, 0)]))
[PROOFSTEP]
infer_instance
