exact Finset.self_mem_range_succ (n + 1)
case this
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ n + 1 ∈ Finset.range (n + 2)
no goals