refine ⟨hc1, ?_⟩
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
hij2✝ : 2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩ ∈ Set.Icc 1 m
hc1 : c ⟨i, ⋯⟩ = c ⟨j, ⋯⟩
hc2 : c' ⟨i, ⋯⟩ = c' ⟨2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩, hij2✝⟩
hij1 : i < j
hij2 : 1 ≤ 2 * j - i ∧ 2 * j ≤ m + i
⊢ c ⟨i, ⋯⟩ = c ⟨j, ⋯⟩ ∧ ∃ (x : 1 ≤ 2 * j - i ∧ 2 * j ≤ n + i), c ⟨i, ⋯⟩ = c ⟨2 * j - i, ⋯⟩
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
hij2✝ : 2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩ ∈ Set.Icc 1 m
hc1 : c ⟨i, ⋯⟩ = c ⟨j, ⋯⟩
hc2 : c' ⟨i, ⋯⟩ = c' ⟨2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩, hij2✝⟩
hij1 : i < j
hij2 : 1 ≤ 2 * j - i ∧ 2 * j ≤ m + i
⊢ ∃ (x : 1 ≤ 2 * j - i ∧ 2 * j ≤ n + i), c ⟨i, ⋯⟩ = c ⟨2 * j - i, ⋯⟩