internlm/Lean-Github huggingface dataset:
Theorem: Turanpartition.small_nonempty
Proof state before:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ P k = minP t P
Tactic:
rw [ha] at hk2
Proof state after:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = min' (image (fun i => P i) (range (t + 1))) nem
⊢ P k = minP t P
Theorem: Turanpartition.small_nonempty
Proof state before:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = min' (image (fun i => P i) (range (t + 1))) nem
⊢ P k = minP t P
Tactic:
exact hk2
Proof state after:
no goals
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
Tactic:
unfold Balanced at h
Proof state after:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
⊢ ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
⊢ ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
Tactic:
have nem : ((range (t + 1)).image fun i => P i).Nonempty :=
  (Nonempty.image_iff _).mpr nonempty_range_succ
Proof state after:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
⊢ ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
⊢ ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
Tactic:
set a : ℕ := min' ((range (t + 1)).image fun i => P i) nem with ha
Proof state after:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
⊢ ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
⊢ ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
Tactic:
set b : ℕ := max' ((range (t + 1)).image fun i => P i) nem with hb
Proof state after:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
⊢ ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
⊢ ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
Tactic:
intro i hi
Proof state after:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
⊢ P i = minP t P ∨ P i = minP t P + 1
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
⊢ P i = minP t P ∨ P i = minP t P + 1
Tactic:
have ale : a ≤ P i := min'_le ((range (t + 1)).image fun i => P i) (P i) (mem_image_of_mem P hi)
Proof state after:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
⊢ P i = minP t P ∨ P i = minP t P + 1
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
⊢ P i = minP t P ∨ P i = minP t P + 1
Tactic:
have leb : P i ≤ b := le_max' ((range (t + 1)).image fun i => P i) (P i) (mem_image_of_mem P hi)
Proof state after:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
⊢ P i = minP t P ∨ P i = minP t P + 1
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
⊢ P i = minP t P ∨ P i = minP t P + 1
Tactic:
have ain := min'_mem ((range (t + 1)).image fun i => P i) nem
Proof state after:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : min' (image (fun i => P i) (range (t + 1))) nem ∈ image (fun i => P i) (range (t + 1))
⊢ P i = minP t P ∨ P i = minP t P + 1
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : min' (image (fun i => P i) (range (t + 1))) nem ∈ image (fun i => P i) (range (t + 1))
⊢ P i = minP t P ∨ P i = minP t P + 1
Tactic:
rw [← ha] at ain
Proof state after:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
⊢ P i = minP t P ∨ P i = minP t P + 1
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
⊢ P i = minP t P ∨ P i = minP t P + 1
Tactic:
have bin := max'_mem ((range (t + 1)).image fun i => P i) nem
Proof state after:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : max' (image (fun i => P i) (range (t + 1))) nem ∈ image (fun i => P i) (range (t + 1))
⊢ P i = minP t P ∨ P i = minP t P + 1
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : max' (image (fun i => P i) (range (t + 1))) nem ∈ image (fun i => P i) (range (t + 1))
⊢ P i = minP t P ∨ P i = minP t P + 1
Tactic:
rw [← hb] at bin
Proof state after:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
⊢ P i = minP t P ∨ P i = minP t P + 1
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
⊢ P i = minP t P ∨ P i = minP t P + 1
Tactic:
have blea : b ≤ a + 1 := by
  rw [mem_image] at *
  obtain ⟨k, hk, hak⟩ := ain; obtain ⟨l, hl, hbl⟩ := bin
  rw [← hak, ← hbl]; exact h l hl k hk
Proof state after:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
blea : b ≤ a + 1
⊢ P i = minP t P ∨ P i = minP t P + 1
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
blea : b ≤ a + 1
⊢ P i = minP t P ∨ P i = minP t P + 1
Tactic:
have ple := le_trans leb blea
Proof state after:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
blea : b ≤ a + 1
ple : P i ≤ a + 1
⊢ P i = minP t P ∨ P i = minP t P + 1
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
blea : b ≤ a + 1
ple : P i ≤ a + 1
⊢ P i = minP t P ∨ P i = minP t P + 1
Tactic:
by_contra h
Proof state after:
t : ℕ
P : ℕ → ℕ
h✝ : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
blea : b ≤ a + 1
ple : P i ≤ a + 1
h : ¬(P i = minP t P ∨ P i = minP t P + 1)
⊢ False
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h✝ : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
blea : b ≤ a + 1
ple : P i ≤ a + 1
h : ¬(P i = minP t P ∨ P i = minP t P + 1)
⊢ False
Tactic:
push_neg at h
Proof state after:
t : ℕ
P : ℕ → ℕ
h✝ : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
blea : b ≤ a + 1
ple : P i ≤ a + 1
h : P i ≠ minP t P ∧ P i ≠ minP t P + 1
⊢ False
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h✝ : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
blea : b ≤ a + 1
ple : P i ≤ a + 1
h : P i ≠ minP t P ∧ P i ≠ minP t P + 1
⊢ False
Tactic:
have h1 := lt_of_le_of_ne ale h.1.symm
Proof state after:
t : ℕ
P : ℕ → ℕ
h✝ : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
blea : b ≤ a + 1
ple : P i ≤ a + 1
h : P i ≠ minP t P ∧ P i ≠ minP t P + 1
h1 : a < P i
⊢ False
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h✝ : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
blea : b ≤ a + 1
ple : P i ≤ a + 1
h : P i ≠ minP t P ∧ P i ≠ minP t P + 1
h1 : a < P i
⊢ False
Tactic:
have h2 := lt_of_le_of_ne ple h.2
Proof state after:
t : ℕ
P : ℕ → ℕ
h✝ : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
blea : b ≤ a + 1
ple : P i ≤ a + 1
h : P i ≠ minP t P ∧ P i ≠ minP t P + 1
h1 : a < P i
h2 : P i < a + 1
⊢ False
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h✝ : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
blea : b ≤ a + 1
ple : P i ≤ a + 1
h : P i ≠ minP t P ∧ P i ≠ minP t P + 1
h1 : a < P i
h2 : P i < a + 1
⊢ False
Tactic:
apply lt_irrefl (a+1)
Proof state after:
t : ℕ
P : ℕ → ℕ
h✝ : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
blea : b ≤ a + 1
ple : P i ≤ a + 1
h : P i ≠ minP t P ∧ P i ≠ minP t P + 1
h1 : a < P i
h2 : P i < a + 1
⊢ a + 1 < a + 1
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h✝ : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
blea : b ≤ a + 1
ple : P i ≤ a + 1
h : P i ≠ minP t P ∧ P i ≠ minP t P + 1
h1 : a < P i
h2 : P i < a + 1
⊢ a + 1 < a + 1
Tactic:
exact lt_of_le_of_lt h1 h2
Proof state after:
no goals
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : a ∈ image (fun i => P i) (range (t + 1))
bin : b ∈ image (fun i => P i) (range (t + 1))
⊢ b ≤ a + 1
Tactic:
rw [mem_image] at *
Proof state after:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : ∃ a_1, a_1 ∈ range (t + 1) ∧ P a_1 = a
bin : ∃ a, a ∈ range (t + 1) ∧ P a = b
⊢ b ≤ a + 1