internlm/Lean-Github huggingface dataset:
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case a
n : ℕ
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x✝ : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x✝ ∉ M
y : ℤ
hy1 : x✝ < y
hy2 : y ∈ M
M' : Finset ℤ := Finset.filter (fun z => z ≤ x✝) M
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card > 0
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
x : Fin n
⊢ x ∈ Finset.filter (fun x => x ≤ i) Finset.univ ↔ x ∈ Finset.univ
Tactic:
rw [Finset.mem_filter]
Proof state after:
case a
n : ℕ
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x✝ : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x✝ ∉ M
y : ℤ
hy1 : x✝ < y
hy2 : y ∈ M
M' : Finset ℤ := Finset.filter (fun z => z ≤ x✝) M
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card > 0
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
x : Fin n
⊢ x ∈ Finset.univ ∧ x ≤ i ↔ x ∈ Finset.univ
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case a
n : ℕ
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x✝ : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x✝ ∉ M
y : ℤ
hy1 : x✝ < y
hy2 : y ∈ M
M' : Finset ℤ := Finset.filter (fun z => z ≤ x✝) M
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card > 0
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
x : Fin n
⊢ x ∈ Finset.univ ∧ x ≤ i ↔ x ∈ Finset.univ
Tactic:
suffices x ≤ i from and_iff_left_of_imp fun a ↦ this
Proof state after:
case a
n : ℕ
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x✝ : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x✝ ∉ M
y : ℤ
hy1 : x✝ < y
hy2 : y ∈ M
M' : Finset ℤ := Finset.filter (fun z => z ≤ x✝) M
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card > 0
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
x : Fin n
⊢ x ≤ i
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case a
n : ℕ
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x✝ : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x✝ ∉ M
y : ℤ
hy1 : x✝ < y
hy2 : y ∈ M
M' : Finset ℤ := Finset.filter (fun z => z ≤ x✝) M
hyM' : y ∉ M'
h3 : M'.card ≤ n - 2
hM : ∑ i : Fin n, a i ∉ M
h7 : M'.card > 0
n' : ℕ := n - 1
a' : Fin n' → ℤ := fun i => a ⟨↑i, ⋯⟩
ainj' : Function.Injective a'
apos' : ∀ (i : Fin n'), 0 < a' i
asorted' : ∀ (i j : Fin n'), i < j → a' i < a' j
Mpos' : ∀ m ∈ M', 0 < m
hM' : ∑ i : Fin n', a' i ∉ M'
p' : Equiv.Perm (Fin n')
hp : ∀ (i : Fin n'), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a' (p' j) ∉ M'
p : Equiv.Perm (Fin n) := extendPerm p' ⋯
i : Fin n
h30 : ¬↑i < n'
h31 : ↑i = n'
pb : Function.Bijective p.toFun
h33 : ↑i + 1 = n
x : Fin n
⊢ x ≤ i
Tactic:
omega
Proof state after:
no goals
Theorem: Imo2009P6.imo2009_p6_aux1
Proof state before:
case ind.inr.inr
n : ℕ
ih :
  ∀ m < n,
    0 < m →
      ∀ (a : Fin m → ℤ),
        Function.Injective a →
          (∀ (i : Fin m), 0 < a i) →
            (∀ (i j : Fin m), i < j → a i < a j) →
              ∀ (M : Finset ℤ),
                (∀ m ∈ M, 0 < m) →
                  M.card ≤ m - 1 →
                    ∑ i : Fin m, a i ∉ M →
                      ∃ p, ∀ (i : Fin m), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card ≤ n - 1
x : ℤ := ∑ i ∈ Finset.filter (fun x => ↑x < n - 1) Finset.univ, a i
h1 : x ∉ M
h2 : ¬∃ y, x < y ∧ y ∈ M
⊢ ∑ i : Fin n, a i ∉ M → ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
sorry
Proof state after:
no goals
Theorem: Imo2009P6.imo2009_p6_aux2
Proof state before:
n : ℕ
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card = n - 1
hM : ∑ i : Fin n, a i ∉ M
⊢ ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
have Mcard' := Mcard.le
Proof state after:
n : ℕ
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card = n - 1
hM : ∑ i : Fin n, a i ∉ M
Mcard' : M.card ≤ n - 1
⊢ ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Theorem: Imo2009P6.imo2009_p6_aux2
Proof state before:
n : ℕ
hn : 0 < n
a : Fin n → ℤ
ainj : Function.Injective a
apos : ∀ (i : Fin n), 0 < a i
asorted : ∀ (i j : Fin n), i < j → a i < a j
M : Finset ℤ
Mpos : ∀ m ∈ M, 0 < m
Mcard : M.card = n - 1
hM : ∑ i : Fin n, a i ∉ M
Mcard' : M.card ≤ n - 1
⊢ ∃ p, ∀ (i : Fin n), ∑ j ∈ Finset.filter (fun x => x ≤ i) Finset.univ, a (p j) ∉ M
Tactic:
exact imo2009_p6_aux1 n hn a ainj apos asorted M Mpos Mcard' hM
Proof state after:
no goals
Theorem: Bulgaria1998P1.lemma1
Proof state before:
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
⊢ all_colorings_are_good n
Tactic:
constructor
Proof 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
Theorem: Bulgaria1998P1.lemma1
Proof state before:
case left
m n : ℕ
hmn : m ≤ n
hm : all_colorings_are_good m
⊢ 3 ≤ n
Tactic:
exact hm.1.trans hmn
Proof state after:
no goals
Theorem: Bulgaria1998P1.lemma1
Proof 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
Proof 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
Theorem: Bulgaria1998P1.lemma1
Proof 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⟩⟩
Proof 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
Theorem: Bulgaria1998P1.lemma1
Proof 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'
Proof 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
Theorem: Bulgaria1998P1.lemma1
Proof 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⟩
Proof 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⟩
Theorem: Bulgaria1998P1.lemma1
Proof 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⟩
Proof 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⟩
Theorem: Bulgaria1998P1.lemma1
Proof 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]
Proof 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, ⋯⟩
Theorem: Bulgaria1998P1.lemma1
Proof 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
Proof 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, ⋯⟩
Theorem: Bulgaria1998P1.lemma1
Proof 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, ?_⟩
Proof 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, ⋯⟩
Theorem: Bulgaria1998P1.lemma1
Proof 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
Proof 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, ⋯⟩
Theorem: Bulgaria1998P1.lemma1
Proof 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
Proof 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, ⋯⟩
Theorem: Bulgaria1998P1.lemma1
Proof 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
Proof 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, ⋯⟩
Theorem: Bulgaria1998P1.lemma1
Proof 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, ?_⟩
Proof 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, ⋯⟩
Theorem: Bulgaria1998P1.lemma1
Proof 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⟩
Proof 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, ⋯⟩
Theorem: Bulgaria1998P1.lemma1
Proof 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'
Proof state after:
no goals
Theorem: Bulgaria1998P1.lemma1
Proof 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]
Proof 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
Theorem: Bulgaria1998P1.lemma1
Proof 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⟩
Proof state after:
no goals
Theorem: Bulgaria1998P1.lemma2
Proof state before:
⊢ ∃ f, ¬coloring_is_good f
Tactic:
use coloring_of_eight
Proof state after:
case h

⊢ ¬coloring_is_good coloring_of_eight
Theorem: Bulgaria1998P1.lemma2
Proof state before:
case h

⊢ ¬coloring_is_good coloring_of_eight
Tactic:
intro h
Proof state after:
case h
h : coloring_is_good coloring_of_eight
⊢ False
Theorem: Bulgaria1998P1.lemma2
Proof state before:
case h
h : coloring_is_good coloring_of_eight
⊢ False
Tactic:
obtain ⟨⟨i, hi1, hi2⟩, ⟨j, hj1, hj2⟩, hij1, hij2, hc1, hc2⟩ := h
Proof state after:
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 : coloring_of_eight ⟨i, ⋯⟩ = coloring_of_eight ⟨j, ⋯⟩
hc2 : coloring_of_eight ⟨i, ⋯⟩ = coloring_of_eight ⟨2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩, hij2⟩
⊢ False
Theorem: Bulgaria1998P1.lemma2
Proof state before:
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 : coloring_of_eight ⟨i, ⋯⟩ = coloring_of_eight ⟨j, ⋯⟩
hc2 : coloring_of_eight ⟨i, ⋯⟩ = coloring_of_eight ⟨2 * ↑⟨j, ⋯⟩ - ↑⟨i, ⋯⟩, hij2⟩
⊢ False
Tactic:
dsimp [coloring_of_eight] at *
Proof state after:
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
Theorem: Bulgaria1998P1.lemma2
Proof state before:
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
Tactic:
interval_cases i <;> interval_cases j <;> aesop (simp_config := {decide := true})
Proof state after:
no goals