. intro x
  specialize hC x
  have h_pos : 0 < 1 + ‖x‖ := add_pos_of_pos_of_nonneg zero_lt_one (norm_nonneg _)
  rw [Real.rpow_neg h_pos.le]
  rw [mul_comm, inv_mul_eq_div]
  rw [le_div_iff' (Real.rpow_pos_of_pos h_pos _)]
  refine le_trans ?_ hC
  refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
  rw [← Real.rpow_nat_cast]
  refine Real.rpow_le_rpow_of_exponent_le (by simp) ?_
  simp [← hk]
  exact Nat.le_ceil _
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
no goals