awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h'f : HasTemperateGrowth.{u_5, u_5} (E := E) (F := E →L[ℝ] E) (fderiv ℝ _root_.id)
hf : Differentiable.{0, u_5, u_5} ℝ (E := E) _root_.id
h : ∀ (x : E), ‖_root_.id x‖ ≤ 1 * HPow.hPow (β := ℕ) (1 + ‖x‖) 1
⊢ HasTemperateGrowth.{u_5, u_5} (E := E) _root_.id

Tactic:
apply Function.HasTemperateGrowth.of_fderiv (k := 1) (C := 1)

Premises used: Function.HasTemperateGrowth.of_fderiv
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ HasTemperateGrowth (F := E →L[ℝ] E) fun (x : E) ↦ ContinuousLinearMap.id ℝ E

Tactic:
Function.HasTemperateGrowth.const (ContinuousLinearMap.id ℝ E)

Premises used: Real, Function.HasTemperateGrowth.const, ContinuousLinearMap.id
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x : E), Eq (α := E →L[ℝ] E) (fderiv ℝ _root_.id x) (ContinuousLinearMap.id ℝ E)
⊢ HasTemperateGrowth.{u_5, u_5} (E := E) (F := E →L[ℝ] E) (fderiv ℝ _root_.id)

Tactic:
convert Function.HasTemperateGrowth.const (ContinuousLinearMap.id ℝ E)

Premises used: Real, Function.HasTemperateGrowth.const, ContinuousLinearMap.id
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
⊢ Eq (α := E →L[ℝ] E) (fderiv ℝ _root_.id x) (ContinuousLinearMap.id ℝ E)

Tactic:
fderiv_fun_id

Premises used: fderiv_fun_id
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
⊢ Eq (α := E →L[ℝ] E) (fderiv ℝ _root_.id x) (ContinuousLinearMap.id ℝ E)

Tactic:
exact fderiv_fun_id

Premises used: fderiv_fun_id
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ Differentiable.{0, u_5, u_5} ℝ (E := E) _root_.id

Tactic:
apply differentiable_id

Premises used: differentiable_id
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ ∀ (x : E), ‖_root_.id x‖ ≤ 1 * HPow.hPow (β := ℕ) (1 + ‖x‖) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ HasTemperateGrowth (F := E) fun (x : E) ↦ x

Tactic:
Function.HasTemperateGrowth.id

Premises used: Function.HasTemperateGrowth.id
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
f : E → 𝕜
g : E → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
⊢ HasTemperateGrowth (f • g)

Tactic:
(ContinuousLinearMap.lsmul ℝ 𝕜).bilinear_hasTemperateGrowth hf hg

Premises used: Real, ContinuousLinearMap.bilinear_hasTemperateGrowth, ContinuousLinearMap.lsmul
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
R : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing R
inst_3 : NormedAlgebra ℝ R
f g : E → R
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
⊢ HasTemperateGrowth (f * g)

Tactic:
(ContinuousLinearMap.mul ℝ R).bilinear_hasTemperateGrowth hf hg

Premises used: Real, ContinuousLinearMap.bilinear_hasTemperateGrowth, ContinuousLinearMap.mul
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
R : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing R
inst_3 : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
⊢ HasTemperateGrowth (HPow.hPow (β := ℕ) f 0)

Tactic:
simpa only [pow_zero] using HasTemperateGrowth.const 1

Premises used: Function.HasTemperateGrowth.const, pow_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
R : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing R
inst_3 : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
k : ℕ
IH : HasTemperateGrowth (f ^ k)
succ : HasTemperateGrowth (f ^ k * f)
⊢ HasTemperateGrowth (f ^ (k + 1))

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
R : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing R
inst_3 : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
k : ℕ
IH : HasTemperateGrowth (f ^ k)
⊢ HasTemperateGrowth (f ^ k * f)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
R : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing R
inst_3 : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
k : ℕ
zero : HasTemperateGrowth (HPow.hPow (β := ℕ) f 0)
succ : ∀ (k : ℕ) (IH : HasTemperateGrowth (f ^ k)), HasTemperateGrowth (f ^ (k + 1))
⊢ HasTemperateGrowth (f ^ k)

Tactic:
induction k with
  | zero => simpa only [pow_zero] using HasTemperateGrowth.const 1
  | succ k IH => rw [pow_succ]; fun_prop

Premises used: Function.HasTemperateGrowth.const, pow_succ, Function.HasTemperateGrowth.zero, pow_zero, 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 →L[ℝ] F
apply : HasTemperateGrowth (E := E) (F := E →L[ℝ] F) (fderiv ℝ (⇑f : (a : E) → F))
apply₁ : ∀ (x : E), norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ ‖f‖ * HPow.hPow (β := ℕ) (1 + ‖x‖) 1
⊢ HasTemperateGrowth.{u_5, u_6} (E := E) (F := F) (⇑f : (a : E) → F)

Tactic:
apply Function.HasTemperateGrowth.of_fderiv ?_ f.differentiable (k := 1) (C := ‖f‖) (fun x ↦ ?_)

Premises used: Function.HasTemperateGrowth.of_fderiv, ContinuousLinearMap.differentiable
-- 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 →L[ℝ] F
h : ∀ (v : E), fderiv ℝ (⇑f : (a : E) → F) v = f
⊢ Eq (α := (x : E) → E →L[ℝ] F) (fderiv ℝ (⇑f : (a : E) → F)) fun (x : E) ↦ f

Tactic:
ext1 v
-- 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 →L[ℝ] F
v : E
⊢ fderiv ℝ (⇑f : (a : E) → F) v = f

Tactic:
simp only [ContinuousLinearMap.fderiv]

Premises used: ContinuousLinearMap.fderiv
-- 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 →L[ℝ] F
⊢ Eq (α := (x : E) → E →L[ℝ] F) (fderiv ℝ (⇑f : (a : E) → F)) fun (x : E) ↦ f

Tactic:
have : fderiv ℝ f = fun _ ↦ f := by ext1 v; simp only [ContinuousLinearMap.fderiv]
-- 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 →L[ℝ] F
this : Eq (α := (x : E) → E →L[ℝ] F) (fderiv ℝ (⇑f : (a : E) → F)) fun (x : E) ↦ f
⊢ HasTemperateGrowth (E := E) (F := E →L[ℝ] F) (fderiv ℝ (⇑f : (a : E) → F))

Tactic:
simp [this]
-- 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 →L[ℝ] F
x : E
⊢ ‖f‖ * ‖x‖ ≤ ‖f‖ * HPow.hPow (β := ℕ) (1 + ‖x‖) 1

Tactic:
simp [mul_add]

Premises used: mul_add
-- 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 →L[ℝ] F
x : E
⊢ norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ ‖f‖ * HPow.hPow (β := ℕ) (1 + ‖x‖) 1

Tactic:
exact (f.le_opNorm x).trans (by simp [mul_add])

Premises used: ContinuousLinearMap.le_opNorm, LE.le.trans
-- 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 ≃L[ℝ] F
⊢ HasTemperateGrowth.{u_5, u_6} (E := E) (F := F) (⇑f : (a : E) → F)

Tactic:
f.toContinuousLinearMap.hasTemperateGrowth

Premises used: ContinuousLinearMap.hasTemperateGrowth, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
⊢ HasTemperateGrowth Complex.ofReal

Tactic:
(Complex.ofRealCLM).hasTemperateGrowth

Premises used: Complex.ofRealCLM, ContinuousLinearMap.hasTemperateGrowth
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
⊢ HasTemperateGrowth.{0, u_2} (F := 𝕜) RCLike.ofReal

Tactic:
(RCLike.ofRealCLM (K := 𝕜)).hasTemperateGrowth

Premises used: RCLike.ofRealCLM, ContinuousLinearMap.hasTemperateGrowth
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
c : H
⊢ HasTemperateGrowth (F := ℝ) fun (x : H) ↦ inner ℝ x c

Tactic:
((innerSL ℝ).flip c).hasTemperateGrowth

Premises used: Real, innerSL, ContinuousLinearMap.hasTemperateGrowth, ContinuousLinearMap.flip, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
c : H
⊢ HasTemperateGrowth (F := ℝ) fun (x : H) ↦ inner ℝ c x

Tactic:
(innerSL ℝ c).hasTemperateGrowth

Premises used: Real, innerSL, ContinuousLinearMap.hasTemperateGrowth, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
h'f : HasTemperateGrowth.{u_8, u_8} (E := H) (F := H →L[ℝ] ℝ) (fderiv ℝ fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2)
hf : Differentiable ℝ (F := ℝ) fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2
h : ∀ (x : H), ‖HPow.hPow (β := ℕ) ‖x‖ 2‖ ≤ 1 * HPow.hPow (β := ℕ) (1 + ‖x‖) 2
⊢ HasTemperateGrowth (F := ℝ) fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
apply _root_.Function.HasTemperateGrowth.of_fderiv (C := 1) (k := 2)

Premises used: Function.HasTemperateGrowth.of_fderiv
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
h'f : HasTemperateGrowth (HSMul.hSMul (α := ℕ) (β := (a : H) → H →L[ℝ] ℝ) 2 (⇑(innerSL ℝ) : (a : H) → H →L[ℝ] ℝ))
⊢ HasTemperateGrowth.{u_8, u_8} (E := H) (F := H →L[ℝ] ℝ) (fderiv ℝ fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2)

Tactic:
rw [fderiv_norm_sq]

Premises used: fderiv_norm_sq
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
⊢ HasTemperateGrowth (E := H) (F := H →L[ℝ] ℝ)
    (⇑(HSMul.hSMul (α := ℕ) (β := H →L⋆[ℝ] H →L[ℝ] ℝ) 2 (innerSL ℝ)) : (a : H) → H →L[ℝ] ℝ)

Tactic:
(2 • innerSL ℝ).hasTemperateGrowth

Premises used: Real, innerSL, ContinuousLinearMap.hasTemperateGrowth, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
⊢ HasTemperateGrowth (HSMul.hSMul (α := ℕ) (β := (a : H) → H →L[ℝ] ℝ) 2 (⇑(innerSL ℝ) : (a : H) → H →L[ℝ] ℝ))

Tactic:
convert! (2 • innerSL ℝ).hasTemperateGrowth

Premises used: Real, innerSL, ContinuousLinearMap.hasTemperateGrowth, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
⊢ Differentiable ℝ (F := ℝ) fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
.norm_sq ℝ differentiable_id

Premises used: Real, Differentiable.norm_sq, differentiable_id
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
⊢ Differentiable ℝ (F := ℝ) fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
exact .norm_sq ℝ differentiable_id
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
x : H
h : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 1 2 + HMul.hMul (α := ℝ) 2 1 * ‖x‖ + HPow.hPow (β := ℕ) ‖x‖ 2
⊢ ‖HPow.hPow (β := ℕ) ‖x‖ 2‖ ≤ 1 * HPow.hPow (β := ℕ) (1 + ‖x‖) 2

Tactic:
rw [norm_pow, norm_norm, one_mul, add_pow_two]

Premises used: norm_pow, add_pow_two, norm_norm, one_mul
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
x : H
⊢ 0 ≤ HPow.hPow (α := ℝ) (β := ℕ) 1 2 + HMul.hMul (α := ℝ) 2 1 * ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
x : H
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 1 2 + HMul.hMul (α := ℝ) 2 1 * ‖x‖ + HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
exact le_add_of_nonneg_left (by positivity)

Premises used: le_add_of_nonneg_left
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
y : H
simp : 1 / 2 < 1 + HPow.hPow (β := ℕ) ‖y‖ 2
⊢ (fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) y ∈ t

Tactic:
simp only [Set.mem_setOf_eq, t]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
y : H
⊢ 1 / 2 < HAdd.hAdd (α := ℝ) 1 0

Tactic:
norm_num
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
y : H
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
y : H
⊢ 1 / 2 < 1 + HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
exact lt_add_of_lt_add_left (c := 0) (by norm_num) (by positivity)

Premises used: lt_add_of_lt_add_left
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
⊢ (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t

Tactic:
have ht : Set.range (fun (x : H) ↦ (1 + ‖x‖ ^ 2)) ⊆ t := by
    rintro - ⟨y, rfl⟩
    simp only [Set.mem_setOf_eq, t]
    exact lt_add_of_lt_add_left (c := 0) (by norm_num) (by positivity)
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
x : ℝ
hx : x ∈ t
⊢ 0 < 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t

Tactic:
have hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t :=
    contDiffOn_fun_id.rpow_const_of_ne fun x hx ↦ (lt_trans (by norm_num) hx).ne'
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
⊢ UniqueDiffOn ℝ t

Tactic:
have hunique : UniqueDiffOn ℝ t := (isOpen_lt' (1 / 2)).uniqueDiffOn
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
⊢ HasTemperateGrowth (F := ℝ) fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
apply :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ)
              (iteratedFDerivWithin ℝ n (fun (x : ℝ) ↦ x ^ r) t x) ≤
            C * (1 + ‖x‖) ^ k
⊢ HasTemperateGrowth (F := ℝ) fun (x : H) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ r

Tactic:
apply HasTemperateGrowth.comp' ht hunique hdiff _ (by fun_prop)

Premises used: Function.HasTemperateGrowth.comp'
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N : ℕ
obtain :
  ∀ (k : ℕ) (hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ)
              (iteratedFDerivWithin ℝ n (fun (x : ℝ) ↦ x ^ r) t x) ≤
            C * (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
    ∀ n ≤ N,
      ∀ x ∈ t,
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ)
            (iteratedFDerivWithin ℝ n (fun (x : ℝ) ↦ x ^ r) t x) ≤
          C * (1 + ‖x‖) ^ k

Tactic:
obtain ⟨k, hk⟩ := exists_nat_ge (max r <| (N - r) * Real.log 2 / (Real.log (3 / 2)))

Premises used: HMul.hMul, HSub.hSub, exists_nat_ge, HDiv.hDiv, Nat.cast, Real.log, Max.max, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
⊢ r ≤ (↑k : ℝ)

Tactic:
have hk₁ : r ≤ k := le_sup_left.trans hk
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
⊢ ((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2) ≤ (↑k : ℝ)

Tactic:
have := le_sup_right.trans hk
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
this : ((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2) ≤ (↑k : ℝ)
⊢ ((↑N : ℝ) - r) * Real.log 2 ≤ Real.log (3 / 2) * (↑k : ℝ)

Tactic:
field_simp at this
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
this : ((↑N : ℝ) - r) * Real.log 2 ≤ Real.log (3 / 2) * (↑k : ℝ)
⊢ Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)

Tactic:
grind
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
⊢ Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)

Tactic:
have hk₂ : Real.log 2 * (N - r) ≤ (Real.log (3 / 2)) * k := by
    have := le_sup_right.trans hk
    field_simp at this
    grind
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
hk₂ : Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
⊢ LE.le (α := ℝ) 0 (∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖)

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
hk₂ : Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
h :
  ∀ n ≤ N,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ)
          (iteratedFDerivWithin ℝ n (fun (x : ℝ) ↦ x ^ r) t x) ≤
        (∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖) * (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
    ∀ n ≤ N,
      ∀ x ∈ t,
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ)
            (iteratedFDerivWithin ℝ n (fun (x : ℝ) ↦ x ^ r) t x) ≤
          C * (1 + ‖x‖) ^ k

Tactic:
use k, ∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖, by positivity

Premises used: Polynomial.eval, Real, descPochhammer, Finset.range, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
hk₂ : Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
⊢ 0 < 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
hk₂ : Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
⊢ ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x

Tactic:
have : ContDiffAt ℝ n (fun x ↦ x ^ r) x :=
    Real.contDiffAt_rpow_const <| Or.inl (lt_trans (by norm_num) hx).ne'