awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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 g : E → F
hf :
  ContDiff ℝ ∞ f ∧
    ∀ (n : ℕ),
      ∃ (k : ℕ),
        IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
          (iteratedFDeriv ℝ n f) fun (x : E) ↦ (1 + ‖x‖) ^ k
hg :
  ContDiff ℝ ∞ g ∧
    ∀ (n : ℕ),
      ∃ (k : ℕ),
        IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
          (iteratedFDeriv ℝ n g) fun (x : E) ↦ (1 + ‖x‖) ^ k
n k₁ : ℕ
h₁ :
  IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤ (iteratedFDeriv ℝ n f)
    fun (x : E) ↦ (1 + ‖x‖) ^ k₁
k₂ : ℕ
h₂ :
  IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤ (iteratedFDeriv ℝ n g)
    fun (x : E) ↦ (1 + ‖x‖) ^ k₂
h :
  ∀ (a : E), Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ LE.le (α := ℝ) (1 x) ((fun (x : E) ↦ 1 + ‖x‖) x)) x} a
⊢ Filter.EventuallyLE (β := ℝ) ⊤ 1 fun (x : E) ↦ 1 + ‖x‖
have h₃ : ∀ (a : E), 1 a ≤ 1 + ‖a‖
Tactic: filter_upwards with _ using (le_add_iff_nonneg_right _).mpr (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
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 g : E → F
hf :
  ContDiff ℝ ∞ f ∧
    ∀ (n : ℕ),
      ∃ (k : ℕ),
        IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
          (iteratedFDeriv ℝ n f) fun (x : E) ↦ (1 + ‖x‖) ^ k
hg :
  ContDiff ℝ ∞ g ∧
    ∀ (n : ℕ),
      ∃ (k : ℕ),
        IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
          (iteratedFDeriv ℝ n g) fun (x : E) ↦ (1 + ‖x‖) ^ k
n k₁ : ℕ
h₁ :
  IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤ (iteratedFDeriv ℝ n f)
    fun (x : E) ↦ (1 + ‖x‖) ^ k₁
k₂ : ℕ
h₂ :
  IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤ (iteratedFDeriv ℝ n g)
    fun (x : E) ↦ (1 + ‖x‖) ^ k₂
⊢ IsBigO (F := ℝ) ⊤
    (HAdd.hAdd (α := E → ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f)
      (iteratedFDeriv ℝ n g))
    fun (x : E) ↦ (1 + ‖x‖) ^ max k₁ k₂
have this : Filter.EventuallyLE (β := ℝ) ⊤ 1 fun (x : E) ↦ 1 + ‖x‖
Tactic: have : 1 ≤ᶠ[⊤] fun (x : E) ↦ 1 + ‖x‖ := by
    filter_upwards with _ using (le_add_iff_nonneg_right _).mpr (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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 g : E → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
⊢ HasTemperateGrowth (f - g)
have h : f - g = f + -g
Tactic: convert! hf.add hg.neg using 1
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
ι : Type u_1
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
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (hf : ∀ i ∈ s, HasTemperateGrowth (f i)), HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ s, f i x
hf : ∀ i ∈ insert a s, HasTemperateGrowth (f i)
⊢ HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ insert a s, f i x
have hf₁ : HasTemperateGrowth (f a)
Tactic: obtain ⟨hf, h⟩ := by simpa using hf
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
ι : Type u_1
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
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (hf : ∀ i ∈ s, HasTemperateGrowth (f i)), HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ s, f i x
hf : ∀ i ∈ insert a s, HasTemperateGrowth (f i)
hf₁ : HasTemperateGrowth (f a)
⊢ HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ insert a s, f i x
have h : ∀ a ∈ s, HasTemperateGrowth (f a)
Tactic: obtain ⟨hf, h⟩ := by simpa using hf
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
ι : Type u_1
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
s : Finset ι
hf : ∀ i ∈ s, HasTemperateGrowth (f i)
⊢ HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ s, f i x
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasTemperateGrowth (f i)),
  HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ ∅, f i x
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert a s has ih =>
    obtain ⟨hf, h⟩ := by simpa using hf
    simpa [has] using hf.add (ih h)
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
ι : Type u_1
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
s : Finset ι
hf : ∀ i ∈ s, HasTemperateGrowth (f i)
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasTemperateGrowth (f i)),
    HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ ∅, f i x
⊢ HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ s, f i x
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (ih : ∀ (hf : ∀ i ∈ s, HasTemperateGrowth (f i)), HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ s, f i x)
  (hf : ∀ i ∈ insert a s, HasTemperateGrowth (f i)),
  HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ insert a s, f i x
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert a s has ih =>
    obtain ⟨hf, h⟩ := by simpa using hf
    simpa [has] using hf.add (ih h)
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
ι : Type u_1
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
s : Finset ι
hf : ∀ i ∈ s, HasTemperateGrowth (f i)
⊢ HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ s, f i x
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasTemperateGrowth (f i)),
  HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ ∅, f i x
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s has ih =>
    obtain ⟨hf, h⟩ := by simpa using hf
    simpa [has] using hf.add (ih h)
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
ι : Type u_1
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
s : Finset ι
hf : ∀ i ∈ s, HasTemperateGrowth (f i)
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasTemperateGrowth (f i)),
    HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ ∅, f i x
⊢ HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ s, f i x
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (ih : ∀ (hf : ∀ i ∈ s, HasTemperateGrowth (f i)), HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ s, f i x)
  (hf : ∀ i ∈ insert a s, HasTemperateGrowth (f i)),
  HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ insert a s, f i x
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s has ih =>
    obtain ⟨hf, h⟩ := by simpa using hf
    simpa [has] using hf.add (ih h)
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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
⊢ 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)
have 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
Tactic: rw [Function.hasTemperateGrowth_iff_isBigO]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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)) ∧
    ∀ (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
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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)
⊢ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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 : ℕ
⊢ ∃ (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
have 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
Tactic: rcases hf.isBigO_uniform n with ⟨k1, h1⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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
⊢ ∃ (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
have 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
Tactic: rcases hg.isBigO_uniform n with ⟨k2, h2⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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
⊢ ∃ (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
have 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)
Tactic: use k1 + k2
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
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
⊢ 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)
have 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)
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)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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)
have 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)
Tactic: refine (IsBigO.of_norm_le estimate).trans (.const_mul_left (.sum fun i hi ↦ ?_) _)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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 + k2)
have 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
Tactic: simp_rw [mul_assoc, pow_add]