obtain ⟨⟨i, hi1, hi2⟩, ⟨j, hj1, hj2⟩, hij1, hij2, hc1, hc2⟩ := hm.2 c'
case right
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, ⋯⟩
⊢ coloring_is_good c
case right.intro.mk.intro.intro.mk.intro.intro.intro.intro
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⟩
⊢ coloring_is_good c