awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.Support
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x x' : E
hx' :
  Membership.mem (γ := Set E)
    (dsupport (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ)) x'
⊢ ∀ (s : Set E),
    IsVanishingOn (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ) sᶜ →
      IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → x' ∈ s

Tactic:
rw [mem_dsupport_iff] at hx'

Premises used: Distribution.mem_dsupport_iff
-- Module: Mathlib.Analysis.Distribution.Support
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x x' : E
hx' :
  ∀ (s : Set E),
    IsVanishingOn (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ) sᶜ →
      IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → x' ∈ s
⊢ Membership.mem (γ := Set E) {x} x'

Tactic:
hx' {x} (isVanishingOn_delta x) (T1Space.t1 x)

Premises used: T1Space.t1, TemperedDistribution.isVanishingOn_delta, Singleton.singleton
-- Module: Mathlib.Analysis.Distribution.Support
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x x' : E
hx' :
  ∀ (s : Set E),
    IsVanishingOn (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ) sᶜ →
      IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → x' ∈ s
⊢ Membership.mem (γ := Set E) {x} x'

Tactic:
exact hx' {x} (isVanishingOn_delta x) (T1Space.t1 x)

Premises used: T1Space.t1, TemperedDistribution.isVanishingOn_delta, Singleton.singleton
-- Module: Mathlib.Analysis.Distribution.Support
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
a :
  ∀ (s : Set E),
    x ∈ s →
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s →
        ∃ (u : 𝓢(E, ℂ)),
          tsupport (α := ℂ) (⇑u : (a : E) → ℂ) ⊆ s ∧
            Ne (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) u : ℂ) (0 : ℂ)
⊢ Membership.mem (γ := Set E)
    (dsupport (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ)) x

Tactic:
rw [mem_dsupport_iff_forall_exists_ne]

Premises used: Distribution.mem_dsupport_iff_forall_exists_ne
-- Module: Mathlib.Analysis.Distribution.Support
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
a :
  ∀ (u : E → ℝ) (h₁ : tsupport u ⊆ s) (h₂ : HasCompactSupport u) (h₃ : ContDiff ℝ (↑⊤ : WithTop ℕ∞) u) (h₄ : u x = 1),
    ∃ (u : 𝓢(E, ℂ)),
      tsupport (α := ℂ) (⇑u : (a : E) → ℂ) ⊆ s ∧
        Ne (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) u : ℂ) (0 : ℂ)
⊢ ∃ (u : 𝓢(E, ℂ)),
    tsupport (α := ℂ) (⇑u : (a : E) → ℂ) ⊆ s ∧
      Ne (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) u : ℂ) (0 : ℂ)

Tactic:
obtain ⟨u, h₁, h₂, h₃, -, h₄⟩ :=
    exists_contDiff_tsupport_subset (n := ⊤) ((IsOpen.mem_nhds_iff hs).mpr hx)

Premises used: Iff.mpr, IsOpen.mem_nhds_iff, exists_contDiff_tsupport_subset
-- Module: Mathlib.Analysis.Distribution.Support
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
u : E → ℝ
h₁ : tsupport u ⊆ s
h₂ : HasCompactSupport u
h₃ : ContDiff ℝ (↑⊤ : WithTop ℕ∞) u
h₄ : u x = 1
⊢ tsupport (α := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ u) ⊆ s

Tactic:
have h₁' : tsupport (Complex.ofRealCLM ∘ u) ⊆ s := (tsupport_comp_subset rfl _).trans h₁
-- Module: Mathlib.Analysis.Distribution.Support
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
u : E → ℝ
h₁ : tsupport u ⊆ s
h₂ : HasCompactSupport u
h₃ : ContDiff ℝ (↑⊤ : WithTop ℕ∞) u
h₄ : u x = 1
h₁' : tsupport (α := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ u) ⊆ s
⊢ HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ u)

Tactic:
have h₂' : HasCompactSupport (Complex.ofRealCLM ∘ u) := h₂.comp_left rfl
-- Module: Mathlib.Analysis.Distribution.Support
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
u : E → ℝ
h₁ : tsupport u ⊆ s
h₂ : HasCompactSupport u
h₃ : ContDiff ℝ (↑⊤ : WithTop ℕ∞) u
h₄ : u x = 1
h₁' : tsupport (α := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ u) ⊆ s
h₂' : HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ u)
h :
  tsupport (α := ℂ) (⇑(h₂'.toSchwartzMap ⋯) : (a : E) → ℂ) ⊆ s ∧
    Ne (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) (h₂'.toSchwartzMap ⋯) : ℂ) (0 : ℂ)
⊢ ∃ (u : 𝓢(E, ℂ)),
    tsupport (α := ℂ) (⇑u : (a : E) → ℂ) ⊆ s ∧
      Ne (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) u : ℂ) (0 : ℂ)

Tactic:
use h₂'.toSchwartzMap (Complex.ofRealCLM.contDiff.comp h₃)

Premises used: Complex.ofRealCLM, ContDiff.comp, ContinuousLinearMap.contDiff, HasCompactSupport.toSchwartzMap
-- Module: Mathlib.Analysis.Distribution.Support
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
u : E → ℝ
h₁ : tsupport u ⊆ s
h₂ : HasCompactSupport u
h₃ : ContDiff ℝ (↑⊤ : WithTop ℕ∞) u
h₄ : u x = 1
h₁' : tsupport (α := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ u) ⊆ s
h₂' : HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ u)
⊢ Ne (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) (h₂'.toSchwartzMap ⋯) : ℂ) (0 : ℂ)

Tactic:
simp [h₄]
-- Module: Mathlib.Analysis.Distribution.Support
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
u : E → ℝ
h₁ : tsupport u ⊆ s
h₂ : HasCompactSupport u
h₃ : ContDiff ℝ (↑⊤ : WithTop ℕ∞) u
h₄ : u x = 1
h₁' : tsupport (α := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ u) ⊆ s
h₂' : HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ u)
⊢ tsupport (α := ℂ) (⇑(h₂'.toSchwartzMap ⋯) : (a : E) → ℂ) ⊆ s ∧
    Ne (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) (h₂'.toSchwartzMap ⋯) : ℂ) (0 : ℂ)

Tactic:
exact ⟨h₁', by simp [h₄]⟩
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
simp_rw :
  HasTemperateGrowth f ↔
    ContDiff ℝ ∞ 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‖
⊢ HasTemperateGrowth f ↔
    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

Tactic:
simp_rw [Asymptotics.isBigO_top]

Premises used: Asymptotics.isBigO_top
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : ∀ (n k : ℕ) (C : ℝ) (x : E), (1 + ‖x‖) ^ k = ‖(1 + ‖x‖) ^ k‖
⊢ HasTemperateGrowth f ↔
    ContDiff ℝ ∞ 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‖

Tactic:
congrm ContDiff ℝ ∞ f ∧ (∀ n, ∃ k C, ∀ x, _ ≤ C * ?_)

Premises used: Real, ContDiff, WithTop.some, Top.top
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
n k : ℕ
C : ℝ
x : E
⊢ 0 ≤ 1 + ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
n k : ℕ
C : ℝ
x : E
a : (1 + ‖x‖) ^ k = ‖1 + ‖x‖‖ ^ k
a₁ a₂ : (1 + ‖x‖) ^ k = (1 + ‖x‖) ^ k
⊢ (1 + ‖x‖) ^ k = ‖(1 + ‖x‖) ^ k‖

Tactic:
rw [norm_pow, Real.norm_of_nonneg (by positivity)]

Premises used: norm_pow, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth 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

Tactic:
Function.hasTemperateGrowth_iff_isBigO.mp hf_temperate |>.2 n

Premises used: Function.hasTemperateGrowth_iff_isBigO, And.right, Iff.mp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
choose :
  ∀ (k : (n : ℕ) → ℕ)
    (hk :
      ∀ (n : ℕ),
        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 n),
    ∃ (k : ℕ),
      ∀ n ≤ N,
        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 : ℕ),
    ∀ n ≤ N,
      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

Tactic:
choose k hk using hf_temperate.isBigO

Premises used: Function.HasTemperateGrowth.isBigO
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    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 n
h :
  ∀ n ≤ N,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤ (iteratedFDeriv ℝ n f)
      fun (x : E) ↦ (1 + ‖x‖) ^ (Finset.range (N + 1)).sup k
⊢ ∃ (k : ℕ),
    ∀ n ≤ N,
      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

Tactic:
use (Finset.range (N + 1)).sup k

Premises used: Finset.range, HAdd.hAdd, Finset.sup, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    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 n
n : ℕ
hn : n ≤ N
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤ (iteratedFDeriv ℝ n f)
    fun (x : E) ↦ (1 + ‖x‖) ^ (Finset.range (N + 1)).sup k

Tactic:
(hk n).trans (isBigO_of_le _ fun x ↦ ?_)

Premises used: Asymptotics.IsBigO.trans, Asymptotics.isBigO_of_le
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    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 n
n : ℕ
hn : n ≤ N
h : ∀ (x : E), ‖(1 + ‖x‖) ^ k n‖ ≤ ‖(1 + ‖x‖) ^ (Finset.range (N + 1)).sup 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‖) ^ (Finset.range (N + 1)).sup k

Tactic:
refine (hk n).trans (isBigO_of_le _ fun x ↦ ?_)

Premises used: Asymptotics.IsBigO.trans, Asymptotics.isBigO_of_le
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    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 n
n : ℕ
hn : n ≤ N
x : E
⊢ 0 ≤ (1 + ‖x‖) ^ k n

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    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 n
n : ℕ
hn : n ≤ N
x : E
⊢ 0 ≤ (1 + ‖x‖) ^ (Finset.range (N + 1)).sup k

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    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 n
n : ℕ
hn : n ≤ N
x : E
h : (1 + ‖x‖) ^ k n ≤ (1 + ‖x‖) ^ (Finset.range (N + 1)).sup k
⊢ ‖(1 + ‖x‖) ^ k n‖ ≤ ‖(1 + ‖x‖) ^ (Finset.range (N + 1)).sup k‖

Tactic:
rw [Real.norm_of_nonneg (by positivity), Real.norm_of_nonneg (by positivity)]

Premises used: Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    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 n
n : ℕ
hn : n ≤ N
x : E
h : 1 ≤ 1 + ‖x‖
h₁ : k n ≤ (Finset.range (N + 1)).sup k
⊢ (1 + ‖x‖) ^ k n ≤ (1 + ‖x‖) ^ (Finset.range (N + 1)).sup k

Tactic:
gcongr
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    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 n
n : ℕ
hn : n ≤ N
x : E
⊢ 1 ≤ 1 + ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    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 n
n : ℕ
hn : n ≤ N
x : E
⊢ n ∈ Finset.range (N + 1)

Tactic:
simpa using hn
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    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 n
n : ℕ
hn : n ≤ N
x : E
⊢ k n ≤ (Finset.range (N + 1)).sup k

Tactic:
exact Finset.le_sup (by simpa using hn)

Premises used: Finset.le_sup
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
n : ℕ
rcases :
  ∀ (k : ℕ)
    (hk :
      ∀ n_1 ≤ n,
        IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F) (F := ℝ) ⊤
          (iteratedFDeriv ℝ n_1 f) fun (x : E) ↦ (1 + ‖x‖) ^ k),
    ∃ (k : ℕ) (C : ℝ),
      0 ≤ C ∧
        ∀ N ≤ n,
          ∀ (x : E),
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin N) ↦ E) F) (iteratedFDeriv ℝ N f x) ≤
              C * (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    0 ≤ C ∧
      ∀ N ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin N) ↦ E) F) (iteratedFDeriv ℝ N f x) ≤
            C * (1 + ‖x‖) ^ k

Tactic:
rcases hf_temperate.isBigO_uniform n with ⟨k, hk⟩

Premises used: Function.HasTemperateGrowth.isBigO_uniform
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F_1 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F_1
inst_3 : NormedSpace ℝ F_1
f : E → F_1
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F_1) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : E) ↦ (1 + ‖x‖) ^ k
F : (x : E) → (N : Fin (n + 1)) → ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (↑N : ℕ)) ↦ E) F_1 :=
  fun (x : E) (N : Fin (n + 1)) ↦ iteratedFDeriv ℝ (↑N : ℕ) f x
simp_rw :
  ∀ (i : ℕ) (h : i ≤ n),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F_1) (F := ℝ) ⊤
      (fun (x : E) ↦ iteratedFDeriv ℝ i f x) fun (x : E) ↦ (1 + ‖x‖) ^ k
⊢ IsBigO (F := ℝ) ⊤ F fun (x : E) ↦ (1 + ‖x‖) ^ k

Tactic:
simp_rw [F, isBigO_pi, Fin.forall_iff, Nat.lt_succ_iff]

Premises used: Asymptotics.isBigO_pi, Fin.forall_iff, Nat.lt_succ_iff
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F_1 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F_1
inst_3 : NormedSpace ℝ F_1
f : E → F_1
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F_1) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : E) ↦ (1 + ‖x‖) ^ k
F : (x : E) → (N : Fin (n + 1)) → ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (↑N : ℕ)) ↦ E) F_1 :=
  fun (x : E) (N : Fin (n + 1)) ↦ iteratedFDeriv ℝ (↑N : ℕ) f x
⊢ ∀ (i : ℕ) (h : i ≤ n),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F_1) (F := ℝ) ⊤
      (fun (x : E) ↦ iteratedFDeriv ℝ i f x) fun (x : E) ↦ (1 + ‖x‖) ^ k

Tactic:
hk
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F_1 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F_1
inst_3 : NormedSpace ℝ F_1
f : E → F_1
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F_1) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : E) ↦ (1 + ‖x‖) ^ k
F : (x : E) → (N : Fin (n + 1)) → ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (↑N : ℕ)) ↦ E) F_1 :=
  fun (x : E) (N : Fin (n + 1)) ↦ iteratedFDeriv ℝ (↑N : ℕ) f x
⊢ ∀ (i : ℕ) (h : i ≤ n),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F_1) (F := ℝ) ⊤
      (fun (x : E) ↦ iteratedFDeriv ℝ i f x) fun (x : E) ↦ (1 + ‖x‖) ^ k

Tactic:
exact hk
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F_1 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F_1
inst_3 : NormedSpace ℝ F_1
f : E → F_1
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F_1) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : E) ↦ (1 + ‖x‖) ^ k
F : (x : E) → (N : Fin (n + 1)) → ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (↑N : ℕ)) ↦ E) F_1 :=
  fun (x : E) (N : Fin (n + 1)) ↦ iteratedFDeriv ℝ (↑N : ℕ) f x
⊢ IsBigO (F := ℝ) ⊤ F fun (x : E) ↦ (1 + ‖x‖) ^ k

Tactic:
have : F =O[⊤] (fun x ↦ (1 + ‖x‖) ^ k) := by
    simp_rw [F, isBigO_pi, Fin.forall_iff, Nat.lt_succ_iff]
    exact hk
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
F_1 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F_1
inst_3 : NormedSpace ℝ F_1
f : E → F_1
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F_1) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : E) ↦ (1 + ‖x‖) ^ k
F : (x : E) → (N : Fin (n + 1)) → ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (↑N : ℕ)) ↦ E) F_1 :=
  fun (x : E) (N : Fin (n + 1)) ↦ iteratedFDeriv ℝ (↑N : ℕ) f x
this : IsBigO (F := ℝ) ⊤ F fun (x : E) ↦ (1 + ‖x‖) ^ k
rcases :
  ∀ (C : ℝ) (C_nonneg : C ≥ 0) (hC : IsBigOWith (F := ℝ) C ⊤ F fun (x : E) ↦ (1 + ‖x‖) ^ k),
    ∃ (k : ℕ) (C : ℝ),
      0 ≤ C ∧
        ∀ N ≤ n,
          ∀ (x : E),
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin N) ↦ E) F_1) (iteratedFDeriv ℝ N f x) ≤
              C * (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    0 ≤ C ∧
      ∀ N ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin N) ↦ E) F_1) (iteratedFDeriv ℝ N f x) ≤
            C * (1 + ‖x‖) ^ k

Tactic:
rcases this.exists_nonneg with ⟨C, C_nonneg, hC⟩

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

Tactic:
simp (discharger := positivity) only [isBigOWith_top, Real.norm_of_nonneg,
    pi_norm_le_iff_of_nonneg, Fin.forall_iff, Nat.lt_succ_iff] at hC

Premises used: pi_norm_le_iff_of_nonneg, Asymptotics.isBigOWith_top, Fin.forall_iff, Nat.lt_succ_iff, Real.norm_of_nonneg