Theorem: Bulgaria1998P1.lemma1 (Compfiles/Bulgaria1998P1.lean)

State before:
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
⊢ all_colorings_are_good n
Tactic:
constructor
State after:
case left
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
⊢ 3 ≤ n

case right
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
⊢ ∀ (color : ↑(Set.Icc 1 n) → Fin 2), coloring_is_good color

State before:
case left
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
⊢ 3 ≤ n
Tactic:
exact hm.1.trans hmn
State after:
no goals

State before:
case right
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
⊢ ∀ (color : ↑(Set.Icc 1 n) → Fin 2), coloring_is_good color
Tactic:
intro c
State after:
case right
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
c : ↑(Set.Icc 1 n) → Fin 2
⊢ coloring_is_good c

State before:
case right
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
c : ↑(Set.Icc 1 n) → Fin 2
⊢ coloring_is_good c
Tactic:
let c' : Set.Icc 1 m → Fin 2 :=
  fun x ↦ c ⟨x.val, by rw [Set.mem_Icc]; exact ⟨x.prop.1, x.prop.2.trans hmn⟩⟩
State after:
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

State before:
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
Tactic:
obtain ⟨⟨i, hi1, hi2⟩, ⟨j, hj1, hj2⟩, hij1, hij2, hc1, hc2⟩ := hm.2 c'
State after:
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

State before:
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
Tactic:
use ⟨i, hi1, hi2.trans hmn⟩
State after:
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⟩
⊢ ∃ j, ⟨i, ⋯⟩ < j ∧ ∃ (h3 : 2 * ↑j - ↑⟨i, ⋯⟩ ∈ Set.Icc 1 n), c ⟨i, ⋯⟩ = c j ∧ c ⟨i, ⋯⟩ = c ⟨2 * ↑j - ↑⟨i, ⋯⟩, h3⟩

State before:
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⟩
⊢ ∃ j, ⟨i, ⋯⟩ < j ∧ ∃ (h3 : 2 * ↑j - ↑⟨i, ⋯⟩ ∈ Set.Icc 1 n), c ⟨i, ⋯⟩ = c j ∧ c ⟨i, ⋯⟩ = c ⟨2 * ↑j - ↑⟨i, ⋯⟩, h3⟩
Tactic:
use ⟨j, hj1, hj2.trans hmn⟩
State after:
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⟩

State before:
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⟩
Tactic:
simp only [Subtype.mk_lt_mk, Nat.lt_one_iff, Set.mem_Icc,
           tsub_le_iff_right, exists_and_left]
State after:
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, ⋯⟩

State before:
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, ⋯⟩
Tactic:
simp only [Subtype.mk_lt_mk] at hij1
State after:
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
⊢ i < j ∧ c ⟨i, ⋯⟩ = c ⟨j, ⋯⟩ ∧ ∃ (x : 1 ≤ 2 * j - i ∧ 2 * j ≤ n + i), c ⟨i, ⋯⟩ = c ⟨2 * j - i, ⋯⟩

State before:
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
⊢ i < j ∧ c ⟨i, ⋯⟩ = c ⟨j, ⋯⟩ ∧ ∃ (x : 1 ≤ 2 * j - i ∧ 2 * j ≤ n + i), c ⟨i, ⋯⟩ = c ⟨2 * j - i, ⋯⟩
Tactic:
refine ⟨hij1, ?_⟩
State after:
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
⊢ c ⟨i, ⋯⟩ = c ⟨j, ⋯⟩ ∧ ∃ (x : 1 ≤ 2 * j - i ∧ 2 * j ≤ n + i), c ⟨i, ⋯⟩ = c ⟨2 * j - i, ⋯⟩

State before:
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
⊢ c ⟨i, ⋯⟩ = c ⟨j, ⋯⟩ ∧ ∃ (x : 1 ≤ 2 * j - i ∧ 2 * j ≤ n + i), c ⟨i, ⋯⟩ = c ⟨2 * j - i, ⋯⟩
Tactic:
simp only [Nat.lt_one_iff, Set.mem_Icc, tsub_le_iff_right] at hij2
State after:
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, ⋯⟩

State before:
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, ⋯⟩
Tactic:
unfold_let c' at hc1
State after:
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 : (fun x => c ⟨↑x, ⋯⟩) ⟨i, ⋯⟩ = (fun x => c ⟨↑x, ⋯⟩) ⟨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, ⋯⟩

State before:
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 : (fun x => c ⟨↑x, ⋯⟩) ⟨i, ⋯⟩ = (fun x => c ⟨↑x, ⋯⟩) ⟨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, ⋯⟩
Tactic:
simp only at hc1
State after:
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, ⋯⟩

State before:
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, ⋯⟩
Tactic:
refine ⟨hc1, ?_⟩
State after:
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, ⋯⟩

State before:
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, ⋯⟩
Tactic:
have hij2' : 1 ≤ 2 * j - i ∧ 2 * j ≤ n + i :=
   ⟨hij2.1, le_add_of_le_add_right hij2.2 hmn⟩
State after:
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
hij2' : 1 ≤ 2 * j - i ∧ 2 * j ≤ n + i
⊢ ∃ (x : 1 ≤ 2 * j - i ∧ 2 * j ≤ n + i), c ⟨i, ⋯⟩ = c ⟨2 * j - i, ⋯⟩

State before:
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
hij2' : 1 ≤ 2 * j - i ∧ 2 * j ≤ n + i
⊢ ∃ (x : 1 ≤ 2 * j - i ∧ 2 * j ≤ n + i), c ⟨i, ⋯⟩ = c ⟨2 * j - i, ⋯⟩
Tactic:
use hij2'
State after:
no goals

State before:
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
c : ↑(Set.Icc 1 n) → Fin 2
x : ↑(Set.Icc 1 m)
⊢ ↑x ∈ Set.Icc 1 n
Tactic:
rw [Set.mem_Icc]
State after:
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
c : ↑(Set.Icc 1 n) → Fin 2
x : ↑(Set.Icc 1 m)
⊢ 1 ≤ ↑x ∧ ↑x ≤ n

State before:
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
c : ↑(Set.Icc 1 n) → Fin 2
x : ↑(Set.Icc 1 m)
⊢ 1 ≤ ↑x ∧ ↑x ≤ n
Tactic:
exact ⟨x.prop.1, x.prop.2.trans hmn⟩
State after:
no goals