awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
rw :
  (ContDiff.{0, u_4, u_7} ℝ (F := G) ∞ fun (x : D) ↦
      (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) ∧
    ∀ (n : ℕ),
      ∃ (k : ℕ),
        IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G) (F := ℝ) ⊤
          (iteratedFDeriv ℝ n fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x))
          fun (x : D) ↦ (1 + ‖x‖) ^ k
⊢ HasTemperateGrowth.{u_4, u_7} (F := G) fun (x : D) ↦
    (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)

Tactic:
rw [Function.hasTemperateGrowth_iff_isBigO]

Premises used: Function.hasTemperateGrowth_iff_isBigO
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
left :
  ContDiff.{0, u_4, u_7} ℝ (F := G) ∞ fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)
right :
  ∀ (n : ℕ),
    ∃ (k : ℕ),
      IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G) (F := ℝ) ⊤
        (iteratedFDeriv ℝ n fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x))
        fun (x : D) ↦ (1 + ‖x‖) ^ k
⊢ (ContDiff.{0, u_4, u_7} ℝ (F := G) ∞ fun (x : D) ↦
      (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) ∧
    ∀ (n : ℕ),
      ∃ (k : ℕ),
        IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G) (F := ℝ) ⊤
          (iteratedFDeriv ℝ n fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x))
          fun (x : D) ↦ (1 + ‖x‖) ^ k

Tactic:
constructor
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
⊢ ContDiff.{0, u_4, u_7} ℝ (F := G) ∞ fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)

Tactic:
apply (B.bilinearRestrictScalars ℝ).isBoundedBilinearMap.contDiff.comp (hf.1.prodMk hg.1)

Premises used: Real, ContDiff.prodMk, IsBoundedBilinearMap.contDiff, ContinuousLinearMap.isBoundedBilinearMap, ContDiff.comp, And.left, ContinuousLinearMap.bilinearRestrictScalars
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n : ℕ
right :
  ∀ (k1 : ℕ)
    (h1 :
      ∀ n_1 ≤ n,
        IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin n_1) ↦ D) E) (F := ℝ) ⊤
          (iteratedFDeriv ℝ n_1 f) fun (x : D) ↦ (1 + ‖x‖) ^ k1),
    ∃ (k : ℕ),
      IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G) (F := ℝ) ⊤
        (iteratedFDeriv ℝ n fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x))
        fun (x : D) ↦ (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x))
      fun (x : D) ↦ (1 + ‖x‖) ^ k

Tactic:
rcases hf.isBigO_uniform n with ⟨k1, h1⟩

Premises used: Function.HasTemperateGrowth.isBigO_uniform
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin n_1) ↦ D) E) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : D) ↦ (1 + ‖x‖) ^ k1
right :
  ∀ (k2 : ℕ)
    (h2 :
      ∀ n_1 ≤ n,
        IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n_1) ↦ D) F) (F := ℝ) ⊤
          (iteratedFDeriv ℝ n_1 g) fun (x : D) ↦ (1 + ‖x‖) ^ k2),
    ∃ (k : ℕ),
      IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G) (F := ℝ) ⊤
        (iteratedFDeriv ℝ n fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x))
        fun (x : D) ↦ (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x))
      fun (x : D) ↦ (1 + ‖x‖) ^ k

Tactic:
rcases hg.isBigO_uniform n with ⟨k2, h2⟩

Premises used: Function.HasTemperateGrowth.isBigO_uniform
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin n_1) ↦ D) E) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : D) ↦ (1 + ‖x‖) ^ k1
k2 : ℕ
h2 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n_1) ↦ D) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 g) fun (x : D) ↦ (1 + ‖x‖) ^ k2
h :
  IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G) (F := ℝ) ⊤
    (iteratedFDeriv ℝ n fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) fun (x : D) ↦
    (1 + ‖x‖) ^ (k1 + k2)
⊢ ∃ (k : ℕ),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x))
      fun (x : D) ↦ (1 + ‖x‖) ^ k

Tactic:
use k1 + k2
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin n_1) ↦ D) E) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : D) ↦ (1 + ‖x‖) ^ k1
k2 : ℕ
h2 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n_1) ↦ D) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 g) fun (x : D) ↦ (1 + ‖x‖) ^ k2
⊢ ∀ (x : D),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
        (iteratedFDeriv ℝ n (fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)

Tactic:
have estimate (x : D) : ‖iteratedFDeriv ℝ n (fun x ↦ B (f x) (g x)) x‖ ≤
      ‖B‖ * ∑ i ∈ Finset.range (n + 1), (n.choose i) *
        ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖ :=
    (B.bilinearRestrictScalars ℝ).norm_iteratedFDeriv_le_of_bilinear hf.1 hg.1 x (mod_cast le_top)
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin n_1) ↦ D) E) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : D) ↦ (1 + ‖x‖) ^ k1
k2 : ℕ
h2 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n_1) ↦ D) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 g) fun (x : D) ↦ (1 + ‖x‖) ^ k2
estimate :
  ∀ (x : D),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
        (iteratedFDeriv ℝ n (fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G) (F := ℝ) ⊤
    (iteratedFDeriv ℝ n fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) fun (x : D) ↦
    (1 + ‖x‖) ^ (k1 + k2)

Tactic:
(IsBigO.of_norm_le estimate).trans (.const_mul_left (.sum fun i hi ↦ ?_) _)

Premises used: Asymptotics.IsBigO.of_norm_le, Asymptotics.IsBigO.const_mul_left, Asymptotics.IsBigO.trans
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin n_1) ↦ D) E) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : D) ↦ (1 + ‖x‖) ^ k1
k2 : ℕ
h2 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n_1) ↦ D) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 g) fun (x : D) ↦ (1 + ‖x‖) ^ k2
estimate :
  ∀ (x : D),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
        (iteratedFDeriv ℝ n (fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)
h :
  ∀ (i : ℕ) (hi : i ∈ Finset.range (n + 1)),
    IsBigO (E := ℝ) (F := ℝ) ⊤
      (fun (x : D) ↦
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x))
      fun (x : D) ↦ (1 + ‖x‖) ^ (k1 + k2)
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G) (F := ℝ) ⊤
    (iteratedFDeriv ℝ n fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) fun (x : D) ↦
    (1 + ‖x‖) ^ (k1 + k2)

Tactic:
refine (IsBigO.of_norm_le estimate).trans (.const_mul_left (.sum fun i hi ↦ ?_) _)

Premises used: Asymptotics.IsBigO.of_norm_le, Asymptotics.IsBigO.const_mul_left, Asymptotics.IsBigO.trans
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin n_1) ↦ D) E) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : D) ↦ (1 + ‖x‖) ^ k1
k2 : ℕ
h2 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n_1) ↦ D) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 g) fun (x : D) ↦ (1 + ‖x‖) ^ k2
estimate :
  ∀ (x : D),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
        (iteratedFDeriv ℝ n (fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)
i : ℕ
hi : i ∈ Finset.range (n + 1)
h :
  IsBigO (E := ℝ) (F := ℝ) ⊤
    (fun (x : D) ↦
      (↑(n.choose i) : ℝ) *
        (norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)))
    fun (x : D) ↦ (1 + ‖x‖) ^ k1 * (1 + ‖x‖) ^ k2
⊢ IsBigO (E := ℝ) (F := ℝ) ⊤
    (fun (x : D) ↦
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
          (iteratedFDeriv ℝ (n - i) g x))
    fun (x : D) ↦ (1 + ‖x‖) ^ (k1 + k2)

Tactic:
simp_rw [mul_assoc, pow_add]

Premises used: mul_assoc, pow_add
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin n_1) ↦ D) E) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : D) ↦ (1 + ‖x‖) ^ k1
k2 : ℕ
h2 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n_1) ↦ D) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 g) fun (x : D) ↦ (1 + ‖x‖) ^ k2
estimate :
  ∀ (x : D),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
        (iteratedFDeriv ℝ n (fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ IsBigO (E := ℝ) (F := ℝ) ⊤
    (fun (x : D) ↦
      (↑(n.choose i) : ℝ) *
        (norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)))
    fun (x : D) ↦ (1 + ‖x‖) ^ k1 * (1 + ‖x‖) ^ k2

Tactic:
.const_mul_left (.mul (h1 i ?_).norm_left (h2 (n - i) ?_).norm_left) _

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.IsBigO.const_mul_left, HSub.hSub, Asymptotics.IsBigO.mul
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin n_1) ↦ D) E) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : D) ↦ (1 + ‖x‖) ^ k1
k2 : ℕ
h2 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n_1) ↦ D) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 g) fun (x : D) ↦ (1 + ‖x‖) ^ k2
estimate :
  ∀ (x : D),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
        (iteratedFDeriv ℝ n (fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)
i : ℕ
hi : i ∈ Finset.range (n + 1)
h : i ≤ n
h₁ : n - i ≤ n
⊢ IsBigO (E := ℝ) (F := ℝ) ⊤
    (fun (x : D) ↦
      (↑(n.choose i) : ℝ) *
        (norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)))
    fun (x : D) ↦ (1 + ‖x‖) ^ k1 * (1 + ‖x‖) ^ k2

Tactic:
refine .const_mul_left (.mul (h1 i ?_).norm_left (h2 (n - i) ?_).norm_left) _
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin n_1) ↦ D) E) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : D) ↦ (1 + ‖x‖) ^ k1
k2 : ℕ
h2 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n_1) ↦ D) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 g) fun (x : D) ↦ (1 + ‖x‖) ^ k2
estimate :
  ∀ (x : D),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
        (iteratedFDeriv ℝ n (fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ i ≤ n

Tactic:
grind
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin n_1) ↦ D) E) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : D) ↦ (1 + ‖x‖) ^ k1
k2 : ℕ
h2 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n_1) ↦ D) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 g) fun (x : D) ↦ (1 + ‖x‖) ^ k2
estimate :
  ∀ (x : D),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
        (iteratedFDeriv ℝ n (fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ n - i ≤ n

Tactic:
grind