awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
hg' :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin ℝ i g t (f x)) ≤
      C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
i : ℕ
hi : 1 ≤ i
hi' : i ≤ n
hbc : C₁ ≤ 1 + C₁
⊢ C₁ * (1 + ‖x‖) ^ k₁ ≤ (1 + C₁) * (1 + ‖x‖) ^ k₁

Tactic:
gcongr
-- 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₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
hg' :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin ℝ i g t (f x)) ≤
      C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
i : ℕ
hi : 1 ≤ i
hi' : i ≤ n
⊢ C₁ ≤ 1 + C₁

Tactic:
simp
-- 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₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
hg' :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin ℝ i g t (f x)) ≤
      C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
i : ℕ
hi : 1 ≤ i
hi' : i ≤ n
⊢ 1 ≤ 1 + C₁

Tactic:
simp [hC₁]
-- 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₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
hg' :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin ℝ i g t (f x)) ≤
      C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
i : ℕ
hi : 1 ≤ i
hi' : i ≤ n
⊢ 1 ≤ (1 + ‖x‖) ^ k₁

Tactic:
simp [one_le_pow₀]

Premises used: one_le_pow₀
-- 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₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
hg' :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin ℝ i g t (f x)) ≤
      C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
i : ℕ
hi : 1 ≤ i
hi' : i ≤ n
apply : i ≠ 0
⊢ (1 + C₁) * (1 + ‖x‖) ^ k₁ ≤ ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i

Tactic:
apply le_self_pow₀ (one_le_mul_of_one_le_of_one_le (by simp [hC₁]) (by simp [one_le_pow₀]))

Premises used: le_self_pow₀, one_le_mul_of_one_le_of_one_le
-- 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₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
hg' :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin ℝ i g t (f x)) ≤
      C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
i : ℕ
hi : 1 ≤ i
hi' : i ≤ n
⊢ i ≠ 0

Tactic:
grind
-- 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₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
hg' :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin ℝ i g t (f x)) ≤
      C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
i : ℕ
hi : 1 ≤ i
hi' : i ≤ n
calc : C₁ * (1 + ‖x‖) ^ k₁ ≤ (1 + C₁) * (1 + ‖x‖) ^ k₁
calc₁ : (1 + C₁) * (1 + ‖x‖) ^ k₁ ≤ ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) ≤
    ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i

Tactic:
calc _ ≤ C₁ * (1 + ‖x‖) ^ k₁ := h₁ i hi' x
      _ ≤ (1 + C₁) * (1 + ‖x‖) ^ k₁ := by gcongr; simp
      _ ≤ _ := by
        apply le_self_pow₀ (one_le_mul_of_one_le_of_one_le (by simp [hC₁]) (by simp [one_le_pow₀]))
        grind

Premises used: Norm.norm, HAdd.hAdd, 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₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
hg' :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin ℝ i g t (f x)) ≤
      C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
⊢ ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) ≤
          ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i

Tactic:
have hf' : ∀ i, 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i := by
    intro i hi hi'
    calc _ ≤ C₁ * (1 + ‖x‖) ^ k₁ := h₁ i hi' x
      _ ≤ (1 + C₁) * (1 + ‖x‖) ^ k₁ := by gcongr; simp
      _ ≤ _ := by
        apply le_self_pow₀ (one_le_mul_of_one_le_of_one_le (by simp [hC₁]) (by simp [one_le_pow₀]))
        grind
-- 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₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
hg' :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin ℝ i g t (f x)) ≤
      C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
hf' :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) ≤
          ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
    (↑n ! : ℝ) * (C₃ * (1 + ‖x‖) ^ (k₁ * k₂)) * ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ n

Tactic:
norm_iteratedFDeriv_comp_le' ht ht' hg₁ hf.1 (mod_cast le_top) x hg' hf'

Premises used: norm_iteratedFDeriv_comp_le', And.left
-- 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₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
hg' :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin ℝ i g t (f x)) ≤
      C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
hf' :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) ≤
          ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i
rw :
  (↑n ! : ℝ) * (C₃ * (1 + ‖x‖) ^ (k₁ * k₂)) * ((1 + C₁) ^ n * (1 + ‖x‖) ^ (k₁ * n)) =
    (↑n ! : ℝ) * C₃ * (1 + C₁) ^ n * ((1 + ‖x‖) ^ (k₁ * k₂) * (1 + ‖x‖) ^ (k₁ * n))
⊢ (↑n ! : ℝ) * (C₃ * (1 + ‖x‖) ^ (k₁ * k₂)) * ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ n =
    (↑n ! : ℝ) * C₃ * (1 + C₁) ^ n * (1 + ‖x‖) ^ (k₁ * k₂ + k₁ * n)

Tactic:
rw [mul_pow, ← pow_mul, pow_add]

Premises used: pow_add, pow_mul, mul_pow
-- 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₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
hg' :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin ℝ i g t (f x)) ≤
      C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
hf' :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) ≤
          ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i
⊢ (↑n ! : ℝ) * (C₃ * (1 + ‖x‖) ^ (k₁ * k₂)) * ((1 + C₁) ^ n * (1 + ‖x‖) ^ (k₁ * n)) =
    (↑n ! : ℝ) * C₃ * (1 + C₁) ^ n * ((1 + ‖x‖) ^ (k₁ * k₂) * (1 + ‖x‖) ^ (k₁ * n))

Tactic:
ring
-- 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₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
hg' :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin ℝ i g t (f x)) ≤
      C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
hf' :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n →
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) ≤
          ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i
calc :
  (↑n ! : ℝ) * (C₃ * (1 + ‖x‖) ^ (k₁ * k₂)) * ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ n =
    (↑n ! : ℝ) * C₃ * (1 + C₁) ^ n * (1 + ‖x‖) ^ (k₁ * k₂ + k₁ * n)
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
    (↑n ! : ℝ) * C₃ * (1 + C₁) ^ n * (1 + ‖x‖) ^ (k₁ * k₂ + k₁ * n)

Tactic:
calc _ ≤ n ! * (C₃ * (1 + ‖x‖) ^ (k₁ * k₂)) * ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ n :=
      norm_iteratedFDeriv_comp_le' ht ht' hg₁ hf.1 (mod_cast le_top) x hg' hf'
    _ = _ := by rw [mul_pow, ← pow_mul, pow_add]; ring

Premises used: Norm.norm, norm_iteratedFDeriv_comp_le', HMul.hMul, HPow.hPow, And.left, HAdd.hAdd, 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
hg : HasTemperateGrowth g
hf : HasTemperateGrowth f
ht : Set.range f ⊆ Set.univ
ht' : UniqueDiffOn.{0, u_5} ℝ (E := E) Set.univ
hg₁ : ContDiffOn ℝ ∞ g Set.univ
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ (x : E),
          Membership.mem (γ := Set E) Set.univ x →
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
                (iteratedFDerivWithin ℝ n g Set.univ x) ≤
              C * (1 + ‖x‖) ^ k
⊢ HasTemperateGrowth (g ∘ f)

Tactic:
apply hf.comp' (t := Set.univ)

Premises used: Function.HasTemperateGrowth.comp'
-- 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
hg : HasTemperateGrowth g
hf : HasTemperateGrowth f
⊢ Set.range f ⊆ Set.univ

Tactic:
simp
-- 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
hg : HasTemperateGrowth g
hf : HasTemperateGrowth f
⊢ UniqueDiffOn.{0, u_5} ℝ (E := E) Set.univ

Tactic:
simp
-- 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
hg : HasTemperateGrowth g
hf : HasTemperateGrowth f
hg₁ : ContDiff ℝ ∞ g
⊢ ContDiffOn ℝ ∞ g Set.univ

Tactic:
rw [contDiffOn_univ]

Premises used: contDiffOn_univ
-- 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
hg : HasTemperateGrowth g
hf : HasTemperateGrowth f
⊢ ContDiff ℝ ∞ g

Tactic:
hg.1

Premises used: And.left
-- 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
hg : HasTemperateGrowth g
hf : HasTemperateGrowth f
⊢ ContDiff ℝ ∞ g

Tactic:
exact hg.1

Premises used: And.left
-- 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
hg : HasTemperateGrowth g
hf : HasTemperateGrowth f
⊢ ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ (x : E),
          Membership.mem (γ := Set E) Set.univ x →
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
                (iteratedFDerivWithin ℝ n g Set.univ x) ≤
              C * (1 + ‖x‖) ^ k

Tactic:
simpa [iteratedFDerivWithin_univ] using hg.norm_iteratedFDeriv_le_uniform

Premises used: Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform, iteratedFDerivWithin_univ