interval_cases i <;> interval_cases j <;> aesop (simp_config := {decide := true})
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
no goals