Theorem: Bulgaria1998P1.lemma2 (Compfiles/Bulgaria1998P1.lean)

State before:
⊢ ∃ f, ¬coloring_is_good f
Tactic:
use coloring_of_eight
State after:
case h

⊢ ¬coloring_is_good coloring_of_eight

State before:
case h

⊢ ¬coloring_is_good coloring_of_eight
Tactic:
intro h
State after:
case h
h : coloring_is_good coloring_of_eight
⊢ False

State before:
case h
h : coloring_is_good coloring_of_eight
⊢ False
Tactic:
obtain ⟨⟨i, hi1, hi2⟩, ⟨j, hj1, hj2⟩, hij1, hij2, hc1, hc2⟩ := h
State after:
case h.intro.mk.intro.intro.mk.intro.intro.intro.intro
i : ℕ
hi1 : 1 ≤ i
hi2 : i ≤ 8
j : ℕ
hj1 : 1 ≤ j
hj2 : j ≤ 8
hij1 : ⟨i, ⋯⟩ < ⟨j, ⋯⟩
hij2 : 2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩ ∈ Set.Icc 1 8
hc1 : coloring_of_eight ⟨i, ⋯⟩ = coloring_of_eight ⟨j, ⋯⟩
hc2 : coloring_of_eight ⟨i, ⋯⟩ = coloring_of_eight ⟨2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩, hij2⟩
⊢ False

State before:
case h.intro.mk.intro.intro.mk.intro.intro.intro.intro
i : ℕ
hi1 : 1 ≤ i
hi2 : i ≤ 8
j : ℕ
hj1 : 1 ≤ j
hj2 : j ≤ 8
hij1 : ⟨i, ⋯⟩ < ⟨j, ⋯⟩
hij2 : 2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩ ∈ Set.Icc 1 8
hc1 : coloring_of_eight ⟨i, ⋯⟩ = coloring_of_eight ⟨j, ⋯⟩
hc2 : coloring_of_eight ⟨i, ⋯⟩ = coloring_of_eight ⟨2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩, hij2⟩
⊢ False
Tactic:
dsimp [coloring_of_eight] at *
State after:
case h.intro.mk.intro.intro.mk.intro.intro.intro.intro
i : ℕ
hi1 : 1 ≤ i
hi2 : i ≤ 8
j : ℕ
hj1 : 1 ≤ j
hj2 : j ≤ 8
hij1 : ⟨i, ⋯⟩ < ⟨j, ⋯⟩
hij2 : 2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩ ∈ Set.Icc 1 8
hc1 :
  (match ⟨i, ⋯⟩ with
    | ⟨1, property⟩ => 0
    | ⟨2, property⟩ => 1
    | ⟨3, property⟩ => 0
    | ⟨4, property⟩ => 1
    | ⟨5, property⟩ => 1
    | ⟨6, property⟩ => 0
    | ⟨7, property⟩ => 1
    | ⟨8, property⟩ => 0
    | x => 0) =
    match ⟨j, ⋯⟩ with
    | ⟨1, property⟩ => 0
    | ⟨2, property⟩ => 1
    | ⟨3, property⟩ => 0
    | ⟨4, property⟩ => 1
    | ⟨5, property⟩ => 1
    | ⟨6, property⟩ => 0
    | ⟨7, property⟩ => 1
    | ⟨8, property⟩ => 0
    | x => 0
hc2 :
  (match ⟨i, ⋯⟩ with
    | ⟨1, property⟩ => 0
    | ⟨2, property⟩ => 1
    | ⟨3, property⟩ => 0
    | ⟨4, property⟩ => 1
    | ⟨5, property⟩ => 1
    | ⟨6, property⟩ => 0
    | ⟨7, property⟩ => 1
    | ⟨8, property⟩ => 0
    | x => 0) =
    match ⟨2 * j - i, hij2⟩ with
    | ⟨1, property⟩ => 0
    | ⟨2, property⟩ => 1
    | ⟨3, property⟩ => 0
    | ⟨4, property⟩ => 1
    | ⟨5, property⟩ => 1
    | ⟨6, property⟩ => 0
    | ⟨7, property⟩ => 1
    | ⟨8, property⟩ => 0
    | x => 0
⊢ False

State before:
case h.intro.mk.intro.intro.mk.intro.intro.intro.intro
i : ℕ
hi1 : 1 ≤ i
hi2 : i ≤ 8
j : ℕ
hj1 : 1 ≤ j
hj2 : j ≤ 8
hij1 : ⟨i, ⋯⟩ < ⟨j, ⋯⟩
hij2 : 2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩ ∈ Set.Icc 1 8
hc1 :
  (match ⟨i, ⋯⟩ with
    | ⟨1, property⟩ => 0
    | ⟨2, property⟩ => 1
    | ⟨3, property⟩ => 0
    | ⟨4, property⟩ => 1
    | ⟨5, property⟩ => 1
    | ⟨6, property⟩ => 0
    | ⟨7, property⟩ => 1
    | ⟨8, property⟩ => 0
    | x => 0) =
    match ⟨j, ⋯⟩ with
    | ⟨1, property⟩ => 0
    | ⟨2, property⟩ => 1
    | ⟨3, property⟩ => 0
    | ⟨4, property⟩ => 1
    | ⟨5, property⟩ => 1
    | ⟨6, property⟩ => 0
    | ⟨7, property⟩ => 1
    | ⟨8, property⟩ => 0
    | x => 0
hc2 :
  (match ⟨i, ⋯⟩ with
    | ⟨1, property⟩ => 0
    | ⟨2, property⟩ => 1
    | ⟨3, property⟩ => 0
    | ⟨4, property⟩ => 1
    | ⟨5, property⟩ => 1
    | ⟨6, property⟩ => 0
    | ⟨7, property⟩ => 1
    | ⟨8, property⟩ => 0
    | x => 0) =
    match ⟨2 * j - i, hij2⟩ with
    | ⟨1, property⟩ => 0
    | ⟨2, property⟩ => 1
    | ⟨3, property⟩ => 0
    | ⟨4, property⟩ => 1
    | ⟨5, property⟩ => 1
    | ⟨6, property⟩ => 0
    | ⟨7, property⟩ => 1
    | ⟨8, property⟩ => 0
    | x => 0
⊢ False
Tactic:
interval_cases i <;> interval_cases j <;> aesop (simp_config := {decide := true})
State after:
no goals