rw [mul_comm, inv_mul_eq_div]
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 : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * ((1 + ‖x‖) ^ r)⁻¹
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 : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C / (1 + ‖x‖) ^ r