Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h.refine_1
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ n - i ∈ Finset.range (n + 1)

case h.refine_2
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ 0 ≤ C_f * (1 + ‖x‖) ^ k_f

case h.refine_3
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ C_f * (1 + ‖x‖) ^ k_f * (C_g * (1 + ‖x‖) ^ k_g) ≤ C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g))
Tactic:
. simp
  exact Nat.sub_lt_succ n i
Proof state after:
case h.refine_2
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ 0 ≤ C_f * (1 + ‖x‖) ^ k_f

case h.refine_3
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ C_f * (1 + ‖x‖) ^ k_f * (C_g * (1 + ‖x‖) ^ k_g) ≤ C_f * (C_g * (1 + ‖x‖) ^ (k_f + k_g))