Theorem: Function.HasTemperateGrowth.comp (ForML/HasTemperateGrowth.lean)

State before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
⊢ HasTemperateGrowth fun x => g (f x)
Tactic:
refine ⟨ContDiff.comp hg.1 hf.1, ?_⟩
State after:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro n
State after:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
have hg_bound := hg.bound_forall_range (n + 1)
State after:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n : ℕ
hg_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n : ℕ
hg_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
have hf_bound := hf.bound_forall_range (n + 1)
State after:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n : ℕ
hg_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C * (1 + ‖x‖) ^ k
hf_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n : ℕ
hg_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C * (1 + ‖x‖) ^ k
hf_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
simp [Nat.lt_succ] at hg_bound hf_bound
State after:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n : ℕ
hg_bound : ∃ k C, 0 ≤ C ∧ ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C * (1 + ‖x‖) ^ k
hf_bound : ∃ k C, 0 ≤ C ∧ ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n : ℕ
hg_bound : ∃ k C, 0 ≤ C ∧ ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C * (1 + ‖x‖) ^ k
hf_bound : ∃ k C, 0 ≤ C ∧ ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
rcases hg_bound with ⟨k_g, C_g, ⟨hC_g_nonneg, hC_g⟩⟩
State after:
case intro.intro.intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n : ℕ
hf_bound : ∃ k C, 0 ≤ C ∧ ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
case intro.intro.intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n : ℕ
hf_bound : ∃ k C, 0 ≤ C ∧ ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
rcases hf_bound with ⟨k_f, C_f, ⟨_, hC_f⟩⟩
State after:
case intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
case intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
have hf0 := hf.2 0
State after:
case intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
hf0 : ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ 0 f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
case intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
hf0 : ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ 0 f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
simp at hf0
State after:
case intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
hf0 : ∃ k C, ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
case intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
hf0 : ∃ k C, ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
rcases hf0 with ⟨k_f0, C_f0, hC_f0⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
use k_f0 * k_g + k_f * n
State after:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
⊢ ∃ C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)

State before:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
⊢ ∃ C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤ C * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)
Tactic:
use n.factorial * C_g * (2 * max 1 C_f0) ^ k_g * (max 1 C_f) ^ n
State after:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
⊢ ∀ (x : E),
    ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
      ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)

State before:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
⊢ ∀ (x : E),
    ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
      ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)
Tactic:
intro x
State after:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)

State before:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)
Tactic:
have hf0 : (1 + ‖f x‖) ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
State after:
case hf0
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0

case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)

State before:
case hf0
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0

case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)
Tactic:
. rw [mul_assoc, two_mul]
  refine add_le_add ?_ ?_
  . simp [one_le_mul_of_one_le_of_one_le]
  . exact le_trans (hC_f0 x) (by simp)
State after:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)

State before:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)
Tactic:
have hC : ∀ (i : ℕ), i ≤ n → ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
State after:
case hC
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
⊢ ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g

case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)

State before:
case hC
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
⊢ ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g

case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)
Tactic:
. intro i hi
  refine le_trans (hC_g i hi (f x)) ?_
  refine mul_le_mul_of_nonneg_left ?_ hC_g_nonneg
  exact pow_le_pow_left (by simp) hf0 k_g
State after:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)

State before:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)
Tactic:
have hD : ∀ i, 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i
State after:
case hD
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
⊢ ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i

case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)

State before:
case hD
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
⊢ ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i

case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)
Tactic:
. intro i _ hi
  refine le_trans (hC_f i hi x) ?_
  refine le_trans (mul_le_mul_of_nonneg_right (le_max_right 1 C_f) (by simp)) ?_
  refine le_self_pow ?_ (by linarith)
  exact one_le_mul_of_one_le_of_one_le (le_max_left 1 C_f) (by simp)
State after:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)

State before:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i
⊢ ‖iteratedFDeriv ℝ n (fun x => g (f x)) x‖ ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)
Tactic:
refine le_trans (norm_iteratedFDeriv_comp_le hg.1 hf.1 le_top x hC hD) ?_
State after:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i
⊢ ↑(Nat.factorial n) * (C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g) * (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ n ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)

State before:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i
⊢ ↑(Nat.factorial n) * (C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g) * (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ n ≤
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)
Tactic:
refine le_of_eq ?_
State after:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i
⊢ ↑(Nat.factorial n) * (C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g) * (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ n =
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)

State before:
case h
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i
⊢ ↑(Nat.factorial n) * (C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g) * (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ n =
    ↑(Nat.factorial n) * C_g * (2 * max 1 C_f0) ^ k_g * max 1 C_f ^ n * (1 + ‖x‖) ^ (k_f0 * k_g + k_f * n)
Tactic:
ring_nf
State after:
no goals

State before:
case hf0
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
Tactic:
rw [mul_assoc, two_mul]
State after:
case hf0
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ 1 + ‖f x‖ ≤ max 1 C_f0 * (1 + ‖x‖) ^ k_f0 + max 1 C_f0 * (1 + ‖x‖) ^ k_f0

State before:
case hf0
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ 1 + ‖f x‖ ≤ max 1 C_f0 * (1 + ‖x‖) ^ k_f0 + max 1 C_f0 * (1 + ‖x‖) ^ k_f0
Tactic:
refine add_le_add ?_ ?_
State after:
case hf0.refine_1
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ 1 ≤ max 1 C_f0 * (1 + ‖x‖) ^ k_f0

case hf0.refine_2
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ ‖f x‖ ≤ max 1 C_f0 * (1 + ‖x‖) ^ k_f0

State before:
case hf0.refine_1
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ 1 ≤ max 1 C_f0 * (1 + ‖x‖) ^ k_f0

case hf0.refine_2
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ ‖f x‖ ≤ max 1 C_f0 * (1 + ‖x‖) ^ k_f0
Tactic:
. simp [one_le_mul_of_one_le_of_one_le]
State after:
case hf0.refine_2
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ ‖f x‖ ≤ max 1 C_f0 * (1 + ‖x‖) ^ k_f0

State before:
case hf0.refine_2
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ ‖f x‖ ≤ max 1 C_f0 * (1 + ‖x‖) ^ k_f0
Tactic:
. exact le_trans (hC_f0 x) (by simp)
State after:
no goals

State before:
case hf0.refine_1
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ 1 ≤ max 1 C_f0 * (1 + ‖x‖) ^ k_f0
Tactic:
simp [one_le_mul_of_one_le_of_one_le]
State after:
no goals

State before:
case hf0.refine_2
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ ‖f x‖ ≤ max 1 C_f0 * (1 + ‖x‖) ^ k_f0
Tactic:
exact le_trans (hC_f0 x) (by simp)
State after:
no goals

State before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
⊢ C_f0 * (1 + ‖x‖) ^ k_f0 ≤ max 1 C_f0 * (1 + ‖x‖) ^ k_f0
Tactic:
simp
State after:
no goals

State before:
case hC
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
⊢ ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
Tactic:
intro i hi
State after:
case hC
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
i : ℕ
hi : i ≤ n
⊢ ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g

State before:
case hC
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
i : ℕ
hi : i ≤ n
⊢ ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
Tactic:
refine le_trans (hC_g i hi (f x)) ?_
State after:
case hC
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
i : ℕ
hi : i ≤ n
⊢ C_g * (1 + ‖f x‖) ^ k_g ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g

State before:
case hC
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
i : ℕ
hi : i ≤ n
⊢ C_g * (1 + ‖f x‖) ^ k_g ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
Tactic:
refine mul_le_mul_of_nonneg_left ?_ hC_g_nonneg
State after:
case hC
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
i : ℕ
hi : i ≤ n
⊢ (1 + ‖f x‖) ^ k_g ≤ (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g

State before:
case hC
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
i : ℕ
hi : i ≤ n
⊢ (1 + ‖f x‖) ^ k_g ≤ (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
Tactic:
exact pow_le_pow_left (by simp) hf0 k_g
State after:
no goals

State before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
i : ℕ
hi : i ≤ n
⊢ 0 ≤ 1 + ‖f x‖
Tactic:
simp
State after:
no goals

State before:
case hD
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
⊢ ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i
Tactic:
intro i _ hi
State after:
case hD
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
i : ℕ
a✝ : 1 ≤ i
hi : i ≤ n
⊢ ‖iteratedFDeriv ℝ i f x‖ ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i

State before:
case hD
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
i : ℕ
a✝ : 1 ≤ i
hi : i ≤ n
⊢ ‖iteratedFDeriv ℝ i f x‖ ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i
Tactic:
refine le_trans (hC_f i hi x) ?_
State after:
case hD
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
i : ℕ
a✝ : 1 ≤ i
hi : i ≤ n
⊢ C_f * (1 + ‖x‖) ^ k_f ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i

State before:
case hD
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
i : ℕ
a✝ : 1 ≤ i
hi : i ≤ n
⊢ C_f * (1 + ‖x‖) ^ k_f ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i
Tactic:
refine le_trans (mul_le_mul_of_nonneg_right (le_max_right 1 C_f) (by simp)) ?_
State after:
case hD
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
i : ℕ
a✝ : 1 ≤ i
hi : i ≤ n
⊢ max 1 C_f * (1 + ‖x‖) ^ k_f ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i

State before:
case hD
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
i : ℕ
a✝ : 1 ≤ i
hi : i ≤ n
⊢ max 1 C_f * (1 + ‖x‖) ^ k_f ≤ (max 1 C_f * (1 + ‖x‖) ^ k_f) ^ i
Tactic:
refine le_self_pow ?_ (by linarith)
State after:
case hD
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
i : ℕ
a✝ : 1 ≤ i
hi : i ≤ n
⊢ 1 ≤ max 1 C_f * (1 + ‖x‖) ^ k_f

State before:
case hD
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
i : ℕ
a✝ : 1 ≤ i
hi : i ≤ n
⊢ 1 ≤ max 1 C_f * (1 + ‖x‖) ^ k_f
Tactic:
exact one_le_mul_of_one_le_of_one_le (le_max_left 1 C_f) (by simp)
State after:
no goals

State before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
i : ℕ
a✝ : 1 ≤ i
hi : i ≤ n
⊢ 0 ≤ (1 + ‖x‖) ^ k_f
Tactic:
simp
State after:
no goals

State before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
i : ℕ
a✝ : 1 ≤ i
hi : i ≤ n
⊢ i ≠ 0
Tactic:
linarith
State after:
no goals

State before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : F → G
hg : HasTemperateGrowth g
f : E → F
hf : HasTemperateGrowth f
n k_g : ℕ
C_g : ℝ
hC_g_nonneg : 0 ≤ C_g
hC_g : ∀ i ≤ n, ∀ (x : F), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
k_f : ℕ
C_f : ℝ
left✝ : 0 ≤ C_f
hC_f : ∀ i ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_f0 : ℕ
C_f0 : ℝ
hC_f0 : ∀ (x : E), ‖f x‖ ≤ C_f0 * (1 + ‖x‖) ^ k_f0
x : E
hf0 : 1 + ‖f x‖ ≤ 2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0
hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i g (f x)‖ ≤ C_g * (2 * max 1 C_f0 * (1 + ‖x‖) ^ k_f0) ^ k_g
i : ℕ
a✝ : 1 ≤ i
hi : i ≤ n
⊢ 1 ≤ (1 + ‖x‖) ^ k_f
Tactic:
simp
State after:
no goals