awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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
⊢ 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
have calc : C₁ * (1 + ‖x‖) ^ k₁ ≤ (1 + C₁) * (1 + ‖x‖) ^ k₁
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
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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₁
⊢ 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
have calc₁ : (1 + C₁) * (1 + ‖x‖) ^ k₁ ≤ ((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
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
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₂)
⊢ 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)
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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₁) * (1 + ‖x‖) ^ k₁) ^ n =
    (↑n ! : ℝ) * C₃ * (1 + C₁) ^ n * (1 + ‖x‖) ^ (k₁ * k₂ + k₁ * n)
have 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))
Tactic: rw [mul_pow, ← pow_mul, pow_add]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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 + C₁) ^ n * (1 + ‖x‖) ^ (k₁ * k₂ + k₁ * n)
have calc : (↑n ! : ℝ) * (C₃ * (1 + ‖x‖) ^ (k₁ * k₂)) * ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ n =
  (↑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
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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
⊢ HasTemperateGrowth (g ∘ f)
have ht : Set.range f ⊆ Set.univ
Tactic: apply hf.comp' (t := Set.univ)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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
⊢ HasTemperateGrowth (g ∘ f)
have ht' : UniqueDiffOn.{0, u_5} ℝ (E := E) Set.univ
Tactic: apply hf.comp' (t := Set.univ)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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
⊢ HasTemperateGrowth (g ∘ f)
have hg₁ : ContDiffOn ℝ ∞ g Set.univ
Tactic: apply hf.comp' (t := Set.univ)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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
⊢ HasTemperateGrowth (g ∘ f)
have 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
Tactic: apply hf.comp' (t := Set.univ)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
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
⊢ ContDiffOn ℝ ∞ g Set.univ
have hg₁ : ContDiff ℝ ∞ g
Tactic: rw [contDiffOn_univ]
-- 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 : E → F
hf : HasTemperateGrowth f
⊢ HasTemperateGrowth (-f)
have 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
Tactic: refine ⟨hf.1.neg, fun n ↦ ?_⟩
-- 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 : E → F
hf : HasTemperateGrowth f
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
have obtain : ∀ (k : ℕ) (C : ℝ)
  (h :
    ∀ (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 ⟨k, C, h⟩ := hf.2 n
-- 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 rw : ∀
  (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),
  ContDiff ℝ ∞ (f + g) ∧
    ∀ (n : ℕ),
      ∃ (k : ℕ),
        IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
          (iteratedFDeriv ℝ n (f + g)) fun (x : E) ↦ (1 + ‖x‖) ^ k
Tactic: rw [hasTemperateGrowth_iff_isBigO] at *
Cleared hypotheses: hf, hg
-- 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
⊢ ContDiff ℝ ∞ (f + g) ∧
    ∀ (n : ℕ),
      ∃ (k : ℕ),
        IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
          (iteratedFDeriv ℝ n (f + g)) fun (x : E) ↦ (1 + ‖x‖) ^ k
have refine : ∀ (n : ℕ),
  ∃ (k : ℕ),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n (f + g)) fun (x : E) ↦ (1 + ‖x‖) ^ k
Tactic: refine ⟨hf.1.add hg.1, fun n ↦ ?_⟩
-- 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 : ℕ),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n (f + g)) fun (x : E) ↦ (1 + ‖x‖) ^ k
have obtain : ∀ (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 : ℕ),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n (f + g)) fun (x : E) ↦ (1 + ‖x‖) ^ k
Tactic: obtain ⟨k₁, h₁⟩ := hf.2 n
-- 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 : ℕ),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n (f + g)) fun (x : E) ↦ (1 + ‖x‖) ^ k
have obtain : ∀ (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₂),
  ∃ (k : ℕ),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n (f + g)) fun (x : E) ↦ (1 + ‖x‖) ^ k
Tactic: obtain ⟨k₂, h₂⟩ := hg.2 n
-- 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₂
⊢ ∃ (k : ℕ),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n (f + g)) fun (x : E) ↦ (1 + ‖x‖) ^ k
have h : IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
  (iteratedFDeriv ℝ n (f + g)) fun (x : E) ↦ (1 + ‖x‖) ^ max k₁ k₂
Tactic: use max k₁ k₂
-- 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₂
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
    (iteratedFDeriv ℝ n (f + g)) fun (x : E) ↦ (1 + ‖x‖) ^ max k₁ k₂
have h : 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₂
Tactic: rw [iteratedFDeriv_add (hf.1.of_le <| mod_cast le_top) (hg.1.of_le <| mod_cast le_top)]
-- 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₂
⊢ Filter.EventuallyLE (β := ℝ) ⊤ 1 fun (x : E) ↦ 1 + ‖x‖
have h : ∀ (a : E), Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ LE.le (α := ℝ) (1 x) ((fun (x : E) ↦ 1 + ‖x‖) x)) x} a
Tactic: filter_upwards with _ using (le_add_iff_nonneg_right _).mpr (by positivity)