-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
lemma _root_.Function.HasTemperateGrowth.of_fderiv {f : E → F}
    (h'f : Function.HasTemperateGrowth (fderiv ℝ f)) (hf : Differentiable ℝ f) {k : ℕ} {C : ℝ}
    (h : ∀ x, ‖f x‖ ≤ C * (1 + ‖x‖) ^ k) :
    Function.HasTemperateGrowth f

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : Function.HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∞ = ω → AnalyticOnNhd ℝ f Set.univ

Tactic:
simp

Result:
no goals

Proof state:
case zero
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : Function.HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ 0 f x‖ ≤ C * (1 + ‖x‖) ^ k

Tactic:
exact ⟨k, C, fun x ↦ by simpa using h x⟩

Result:
no goals

Proof state:
case succ.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : Function.HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m k' : ℕ
C' : ℝ
h' : ∀ (x : E), ‖iteratedFDeriv ℝ m (fderiv ℝ f) x‖ ≤ C' * (1 + ‖x‖) ^ k'
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ (m + 1) f x‖ ≤ C * (1 + ‖x‖) ^ k

Tactic:
refine ⟨k', C', ?_⟩

Result:
case succ.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : Function.HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m k' : ℕ
C' : ℝ
h' : ∀ (x : E), ‖iteratedFDeriv ℝ m (fderiv ℝ f) x‖ ≤ C' * (1 + ‖x‖) ^ k'
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ (m + 1) f x‖ ≤ C' * (1 + ‖x‖) ^ k'

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : Function.HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ ‖iteratedFDeriv ℝ 0 f x‖ ≤ C * (1 + ‖x‖) ^ k

Tactic:
simpa using h x

Result:
no goals

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : Function.HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ Function.HasTemperateGrowth f

Tactic:
refine ⟨contDiff_succ_iff_fderiv.2 ⟨hf, by simp, h'f.1⟩ , fun n ↦ ?_⟩

Result:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : Function.HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C * (1 + ‖x‖) ^ k

Proof state:
case succ
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : Function.HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ (m + 1) f x‖ ≤ C * (1 + ‖x‖) ^ k

Tactic:
rcases h'f.2 m with ⟨k', C', h'⟩

Result:
case succ.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : Function.HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m k' : ℕ
C' : ℝ
h' : ∀ (x : E), ‖iteratedFDeriv ℝ m (fderiv ℝ f) x‖ ≤ C' * (1 + ‖x‖) ^ k'
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ (m + 1) f x‖ ≤ C * (1 + ‖x‖) ^ k

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : Function.HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C * (1 + ‖x‖) ^ k

Tactic:
rcases n with rfl|m

Result:
case zero
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : Function.HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ 0 f x‖ ≤ C * (1 + ‖x‖) ^ k

case succ
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : Function.HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ (m + 1) f x‖ ≤ C * (1 + ‖x‖) ^ k

Proof state:
case succ.intro.intro
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : Function.HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m k' : ℕ
C' : ℝ
h' : ∀ (x : E), ‖iteratedFDeriv ℝ m (fderiv ℝ f) x‖ ≤ C' * (1 + ‖x‖) ^ k'
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ (m + 1) f x‖ ≤ C' * (1 + ‖x‖) ^ k'

Tactic:
simpa [iteratedFDeriv_succ_eq_comp_right] using h'

Result:
no goals