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