simp only [Subtype.mk_lt_mk, Nat.lt_one_iff, Set.mem_Icc,
           tsub_le_iff_right, exists_and_left]
case h
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
c : ↑(Set.Icc 1 n) → Fin 2
c' : ↑(Set.Icc 1 m) → Fin 2 := fun x => c ⟨↑x, ⋯⟩
i : ℕ
hi1 : 1 ≤ i
hi2 : i ≤ m
j : ℕ
hj1 : 1 ≤ j
hj2 : j ≤ m
hij1 : ⟨i, ⋯⟩ < ⟨j, ⋯⟩
hij2 : 2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩ ∈ Set.Icc 1 m
hc1 : c' ⟨i, ⋯⟩ = c' ⟨j, ⋯⟩
hc2 : c' ⟨i, ⋯⟩ = c' ⟨2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩, hij2⟩
⊢ ⟨i, ⋯⟩ < ⟨j, ⋯⟩ ∧
    ∃ (h3 : 2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩ ∈ Set.Icc 1 n), c ⟨i, ⋯⟩ = c ⟨j, ⋯⟩ ∧ c ⟨i, ⋯⟩ = c ⟨2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩, h3⟩
case h
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
c : ↑(Set.Icc 1 n) → Fin 2
c' : ↑(Set.Icc 1 m) → Fin 2 := fun x => c ⟨↑x, ⋯⟩
i : ℕ
hi1 : 1 ≤ i
hi2 : i ≤ m
j : ℕ
hj1 : 1 ≤ j
hj2 : j ≤ m
hij1 : ⟨i, ⋯⟩ < ⟨j, ⋯⟩
hij2 : 2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩ ∈ Set.Icc 1 m
hc1 : c' ⟨i, ⋯⟩ = c' ⟨j, ⋯⟩
hc2 : c' ⟨i, ⋯⟩ = c' ⟨2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩, hij2⟩
⊢ i < j ∧ c ⟨i, ⋯⟩ = c ⟨j, ⋯⟩ ∧ ∃ (x : 1 ≤ 2 * j - i ∧ 2 * j ≤ n + i), c ⟨i, ⋯⟩ = c ⟨2 * j - i, ⋯⟩