obtain ⟨k, hk, hak⟩ := ain
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
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