awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F_1 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F_1
inst_3 : NormedSpace ℝ F_1
f : E → F_1
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F_1) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : E) ↦ (1 + ‖x‖) ^ k
F : (x : E) → (N : Fin (n + 1)) → ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (↑N : ℕ)) ↦ E) F_1 :=
  fun (x : E) (N : Fin (n + 1)) ↦ iteratedFDeriv ℝ (↑N : ℕ) f x
this : IsBigO (F := ℝ) ⊤ F fun (x : E) ↦ (1 + ‖x‖) ^ k
C : ℝ
C_nonneg : C ≥ 0
hC :
  ∀ (x : E) (i : ℕ) (h : i ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F_1) (F x (⟨i, ⋯⟩ : Fin (n + 1))) ≤
      C * (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    0 ≤ C ∧
      ∀ N ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin N) ↦ E) F_1) (iteratedFDeriv ℝ N f x) ≤
            C * (1 + ‖x‖) ^ k

Tactic:
⟨k, C, C_nonneg, fun N hN x ↦ hC x N hN⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F_1 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F_1
inst_3 : NormedSpace ℝ F_1
f : E → F_1
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F_1) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : E) ↦ (1 + ‖x‖) ^ k
F : (x : E) → (N : Fin (n + 1)) → ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (↑N : ℕ)) ↦ E) F_1 :=
  fun (x : E) (N : Fin (n + 1)) ↦ iteratedFDeriv ℝ (↑N : ℕ) f x
this : IsBigO (F := ℝ) ⊤ F fun (x : E) ↦ (1 + ‖x‖) ^ k
C : ℝ
C_nonneg : C ≥ 0
hC :
  ∀ (x : E) (i : ℕ) (h : i ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F_1) (F x (⟨i, ⋯⟩ : Fin (n + 1))) ≤
      C * (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    0 ≤ C ∧
      ∀ N ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin N) ↦ E) F_1) (iteratedFDeriv ℝ N f x) ≤
            C * (1 + ‖x‖) ^ k

Tactic:
exact ⟨k, C, C_nonneg, fun N hN x ↦ hC x N hN⟩
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ Eq (α := ℕ∞ω) ∞ ω → AnalyticOnNhd ℝ f Set.univ

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
refine :
  ∀ (n : ℕ),
    ∃ (k : ℕ) (C : ℝ),
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
          C * (1 + ‖x‖) ^ k
⊢ HasTemperateGrowth f

Tactic:
refine ⟨contDiff_succ_iff_fderiv.2 ⟨hf, by simp, h'f.1⟩, fun n ↦ ?_⟩
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
n : ℕ
zero :
  ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv ℝ 0 f x) ≤
        C * (1 + ‖x‖) ^ k
succ :
  ∀ (m : ℕ),
    ∃ (k : ℕ) (C : ℝ),
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F)
            (iteratedFDeriv ℝ (m + 1) f x) ≤
          C * (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C * (1 + ‖x‖) ^ k

Tactic:
rcases n with rfl | m

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv ℝ 0 f x) ≤
    C * (1 + ‖x‖) ^ k

Tactic:
simpa using h x
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv ℝ 0 f x) ≤
        C * (1 + ‖x‖) ^ k

Tactic:
exact ⟨k, C, fun x ↦ by simpa using h x⟩
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m : ℕ
succ :
  ∀ (k' : ℕ) (C' : ℝ)
    (h' :
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ E) (E →L[ℝ] F)) (iteratedFDeriv ℝ m (fderiv ℝ f) x) ≤
          C' * (1 + ‖x‖) ^ k'),
    ∃ (k : ℕ) (C : ℝ),
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F)
            (iteratedFDeriv ℝ (m + 1) f x) ≤
          C * (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F)
          (iteratedFDeriv ℝ (m + 1) f x) ≤
        C * (1 + ‖x‖) ^ k

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

Premises used: And.right
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m k' : ℕ
C' : ℝ
h' :
  ∀ (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ E) (E →L[ℝ] F)) (iteratedFDeriv ℝ m (fderiv ℝ f) x) ≤
      C' * (1 + ‖x‖) ^ k'
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F)
          (iteratedFDeriv ℝ (m + 1) f x) ≤
        C * (1 + ‖x‖) ^ k

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

Premises used: Exists.intro
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m k' : ℕ
C' : ℝ
h' :
  ∀ (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ E) (E →L[ℝ] F)) (iteratedFDeriv ℝ m (fderiv ℝ f) x) ≤
      C' * (1 + ‖x‖) ^ k'
succ :
  ∀ (x : E),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F)
        (iteratedFDeriv ℝ (m + 1) f x) ≤
      C' * (1 + ‖x‖) ^ k'
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F)
          (iteratedFDeriv ℝ (m + 1) f x) ≤
        C * (1 + ‖x‖) ^ k

Tactic:
refine ⟨k', C', ?_⟩
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m k' : ℕ
C' : ℝ
h' :
  ∀ (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ E) (E →L[ℝ] F)) (iteratedFDeriv ℝ m (fderiv ℝ f) x) ≤
      C' * (1 + ‖x‖) ^ k'
succ :
  ∀ (x : E),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F)
        ((LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' ℝ m E F) :
              (a : ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ E) (E →L[ℝ] F)) →
                ContinuousMultilinearMap ℝ (fun (i : Fin (m + 1)) ↦ E) F)
            (iteratedFDeriv ℝ m (fun (y : E) ↦ fderiv ℝ f y) x) :
          ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F) ≤
      C' * (1 + ‖x‖) ^ k'
⊢ ∀ (x : E),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F)
        (iteratedFDeriv ℝ (m + 1) f x) ≤
      C' * (1 + ‖x‖) ^ k'

Tactic:
simpa [iteratedFDeriv_succ_eq_comp_right] using h'

Premises used: iteratedFDeriv_succ_eq_comp_right
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
⊢ HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ 0

Tactic:
⟨contDiff_const, fun n ↦ ⟨0, 0, fun x ↦ ?_⟩⟩

Premises used: Function.HasTemperateGrowth, contDiff_const, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
refine :
  ∀ (n : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (fun (x : E) ↦ 0) x) ≤
      0 * HPow.hPow (β := ℕ) (1 + ‖x‖) 0
⊢ HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ 0

Tactic:
refine ⟨contDiff_const, fun n ↦ ⟨0, 0, fun x ↦ ?_⟩⟩
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ
x : E
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (fun (x : E) ↦ 0) x) ≤
    0 * HPow.hPow (β := ℕ) (1 + ‖x‖) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
c : F
⊢ HasTemperateGrowth (E := E) (F := E →L[ℝ] F) (fderiv ℝ fun (x : E) ↦ c)

Tactic:
simpa using .zero
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
c : F
x : E
⊢ ‖c‖ ≤ ‖c‖ * HPow.hPow (β := ℕ) (1 + ‖x‖) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
⊢ HasTemperateGrowth f

Tactic:
⟨h₂, fun n ↦ ?_⟩

Premises used: Function.HasTemperateGrowth, And.intro
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
refine :
  ∀ (n : ℕ),
    ∃ (k : ℕ) (C : ℝ),
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
          C * (1 + ‖x‖) ^ k
⊢ HasTemperateGrowth f

Tactic:
refine ⟨h₂, fun n ↦ ?_⟩
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
⊢ Continuous g

Tactic:
have hg : Continuous g := (h₂.continuous_iteratedFDeriv <| mod_cast le_top).norm
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
hg : Continuous g
obtain :
  ∀ (x₀ : E) (hx₀ : ∀ (y : E), g y ≤ g x₀),
    ∃ (k : ℕ) (C : ℝ),
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
          C * (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C * (1 + ‖x‖) ^ k

Tactic:
obtain ⟨x₀, hx₀⟩ := hg.exists_forall_ge_of_hasCompactSupport ((h₁.iteratedFDeriv _).norm)

Premises used: Continuous.exists_forall_ge_of_hasCompactSupport, HasCompactSupport.iteratedFDeriv, HasCompactSupport.norm
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
hg : Continuous g
x₀ : E
hx₀ : ∀ (y : E), g y ≤ g x₀
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C * (1 + ‖x‖) ^ k

Tactic:
⟨0, g x₀, fun x ↦ ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
hg : Continuous g
x₀ : E
hx₀ : ∀ (y : E), g y ≤ g x₀
refine :
  ∀ (x : E),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
      g x₀ * HPow.hPow (β := ℕ) (1 + ‖x‖) 0
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C * (1 + ‖x‖) ^ k

Tactic:
refine ⟨0, g x₀, fun x ↦ ?_⟩
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
hg : Continuous g
x₀ : E
hx₀ : ∀ (y : E), g y ≤ g x₀
x : E
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
    g x₀ * HPow.hPow (β := ℕ) (1 + ‖x‖) 0

Tactic:
simpa using hx₀ x
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
⊢ HasTemperateGrowth (g ∘ f)

Tactic:
⟨hg₁.comp_contDiff hf.1 (ht ⟨·, rfl⟩), fun n ↦ ?_⟩

Premises used: ContDiffOn.comp_contDiff, Function.HasTemperateGrowth, And.left, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
refine :
  ∀ (n : ℕ),
    ∃ (k : ℕ) (C : ℝ),
      ∀ (x : D),
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
          C * (1 + ‖x‖) ^ k
⊢ HasTemperateGrowth (g ∘ f)

Tactic:
refine ⟨hg₁.comp_contDiff hf.1 (ht ⟨·, rfl⟩), fun n ↦ ?_⟩
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n : ℕ
obtain :
  ∀ (k₁ : ℕ) (C₁ : ℝ) (hC₁ : 0 ≤ C₁)
    (h₁ :
      ∀ N ≤ n,
        ∀ (x : D),
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
            C₁ * (1 + ‖x‖) ^ k₁),
    ∃ (k : ℕ) (C : ℝ),
      ∀ (x : D),
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
          C * (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
        C * (1 + ‖x‖) ^ k

Tactic:
obtain ⟨k₁, C₁, hC₁, h₁⟩ := hf.norm_iteratedFDeriv_le_uniform n

Premises used: Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
obtain :
  ∀ (k₂ : ℕ) (C₂ : ℝ) (hC₂ : 0 ≤ C₂)
    (h₂ :
      ∀ n_1 ≤ n,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
              (iteratedFDerivWithin ℝ n_1 g t x) ≤
            C₂ * (1 + ‖x‖) ^ k₂),
    ∃ (k : ℕ) (C : ℝ),
      ∀ (x : D),
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
          C * (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
        C * (1 + ‖x‖) ^ k

Tactic:
obtain ⟨k₂, C₂, hC₂, h₂⟩ := hg₂ n
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
⊢ ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁

Tactic:
simpa using h₁ 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
⊢ ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁

Tactic:
have h₁' : ∀ x, ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁ := by simpa using h₁ 0