obtain ⟨⟨i, hi1, hi2⟩, ⟨j, hj1, hj2⟩, hij1, hij2, hc1, hc2⟩ := h
case h
h : coloring_is_good coloring_of_eight
⊢ False
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