Theorem: Turanpartition.con_sum (Turan4/Turanpartition.lean)

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
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

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
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

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
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

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
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

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
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

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)
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

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)
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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)
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

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
State after:
no goals

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 *
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

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_1, a_1 ∈ range (t + 1) ∧ P a_1 = a
bin : ∃ a, a ∈ range (t + 1) ∧ P a = b
⊢ b ≤ a + 1
Tactic:
obtain ⟨k, hk, hak⟩ := ain
State after:
case intro.intro
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
bin : ∃ a, a ∈ range (t + 1) ∧ P a = b
k : ℕ
hk : k ∈ range (t + 1)
hak : P k = a
⊢ b ≤ a + 1

State before:
case intro.intro
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
bin : ∃ a, a ∈ range (t + 1) ∧ P a = b
k : ℕ
hk : k ∈ range (t + 1)
hak : P k = a
⊢ b ≤ a + 1
Tactic:
obtain ⟨l, hl, hbl⟩ := bin
State after:
case intro.intro.intro.intro
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
k : ℕ
hk : k ∈ range (t + 1)
hak : P k = a
l : ℕ
hl : l ∈ range (t + 1)
hbl : P l = b
⊢ b ≤ a + 1

State before:
case intro.intro.intro.intro
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
k : ℕ
hk : k ∈ range (t + 1)
hak : P k = a
l : ℕ
hl : l ∈ range (t + 1)
hbl : P l = b
⊢ b ≤ a + 1
Tactic:
rw [← hak, ← hbl]
State after:
case intro.intro.intro.intro
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
k : ℕ
hk : k ∈ range (t + 1)
hak : P k = a
l : ℕ
hl : l ∈ range (t + 1)
hbl : P l = b
⊢ P l ≤ P k + 1

State before:
case intro.intro.intro.intro
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
k : ℕ
hk : k ∈ range (t + 1)
hak : P k = a
l : ℕ
hl : l ∈ range (t + 1)
hbl : P l = b
⊢ P l ≤ P k + 1
Tactic:
exact h l hl k hk
State after:
no goals