awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : HasTemperateGrowth f
⊢ HasTemperateGrowth (-f)

Tactic:
⟨hf.1.neg, fun n ↦ ?_⟩

Premises used: Function.HasTemperateGrowth, And.left, And.intro, ContDiff.neg
-- 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 : HasTemperateGrowth f
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
⊢ HasTemperateGrowth (-f)

Tactic:
refine ⟨hf.1.neg, fun n ↦ ?_⟩
-- 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 : HasTemperateGrowth f
n : ℕ
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
⊢ ∃ (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

Premises used: And.right
-- 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 : HasTemperateGrowth f
n 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
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:
simpa [iteratedFDeriv_neg_apply] using h x

Premises used: iteratedFDeriv_neg_apply
-- 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 : HasTemperateGrowth f
n 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:
exact ⟨k, C, fun x ↦ by simpa [iteratedFDeriv_neg_apply] using h x⟩
-- 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 g : E → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
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
⊢ HasTemperateGrowth (f + g)

Tactic:
rw [hasTemperateGrowth_iff_isBigO] at *

Premises used: Function.hasTemperateGrowth_iff_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 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

Tactic:
⟨hf.1.add hg.1, fun n ↦ ?_⟩

Premises used: ContDiff.add, And.left, And.intro
-- 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 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
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
⊢ 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:
refine ⟨hf.1.add hg.1, fun n ↦ ?_⟩
-- 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 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 : ℕ
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
⊢ ∃ (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

Premises used: And.right
-- 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 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₁
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
⊢ ∃ (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

Premises used: And.right
-- 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 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 :
  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₂
⊢ ∃ (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:
use max k₁ k₂

Premises used: Max.max
-- 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 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 :
  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₂
⊢ 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:
rw [iteratedFDeriv_add (hf.1.of_le <| mod_cast le_top) (hg.1.of_le <| mod_cast le_top)]

Premises used: iteratedFDeriv_add, ContDiff.of_le, And.left
-- 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 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₂
a : E
⊢ 0 ≤ ‖a‖

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 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
h₃ h₄ : ∀ (a : E), 1 a ≤ 1 + ‖a‖
⊢ Filter.EventuallyLE (β := ℝ) ⊤ 1 fun (x : E) ↦ 1 + ‖x‖

Tactic:
filter_upwards with _ using (le_add_iff_nonneg_right _).mpr (by positivity)

Premises used: Iff.mpr, le_add_iff_nonneg_right
-- 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 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‖

Tactic:
have : 1 ≤ᶠ[⊤] fun (x : E) ↦ 1 + ‖x‖ := by
    filter_upwards with _ using (le_add_iff_nonneg_right _).mpr (by 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 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₂
this : Filter.EventuallyLE (β := ℝ) ⊤ 1 fun (x : E) ↦ 1 + ‖x‖
⊢ 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:
(h₁.trans (IsBigO.pow_of_le_right this (k₁.le_max_left k₂))).add
    (h₂.trans (IsBigO.pow_of_le_right this (k₁.le_max_right k₂)))

Premises used: Nat.le_max_right, Nat.le_max_left, Asymptotics.IsBigO.trans, Asymptotics.IsBigO.add, Asymptotics.IsBigO.pow_of_le_right
-- 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 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₂
this : Filter.EventuallyLE (β := ℝ) ⊤ 1 fun (x : E) ↦ 1 + ‖x‖
⊢ 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:
exact (h₁.trans (IsBigO.pow_of_le_right this (k₁.le_max_left k₂))).add
    (h₂.trans (IsBigO.pow_of_le_right this (k₁.le_max_right k₂)))

Premises used: Nat.le_max_right, Nat.le_max_left, Asymptotics.IsBigO.trans, Asymptotics.IsBigO.add, Asymptotics.IsBigO.pow_of_le_right
-- 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 g : E → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
⊢ HasTemperateGrowth (f + -g)

Tactic:
hf.add hg.neg

Premises used: Function.HasTemperateGrowth.neg, Function.HasTemperateGrowth.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 g : E → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
h : f - g = f + -g
⊢ HasTemperateGrowth (f - g)

Tactic:
convert! hf.add hg.neg using 1

Premises used: Function.HasTemperateGrowth.neg, Function.HasTemperateGrowth.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 g : E → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
⊢ f - g = f + -g

Tactic:
grind
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasTemperateGrowth (f i)
⊢ HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ ∅, f i x

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 (f a) ∧ ∀ a ∈ s, HasTemperateGrowth (f a)

Tactic:
simpa using hf
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 (f a)

Tactic:
obtain ⟨hf, h⟩ := by simpa using hf
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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)
⊢ ∀ a ∈ s, HasTemperateGrowth (f a)

Tactic:
obtain ⟨hf, h⟩ := by simpa using hf
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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_1 : ∀ i ∈ insert a s, HasTemperateGrowth (f i)
hf : HasTemperateGrowth (f a)
h : ∀ a ∈ s, HasTemperateGrowth (f a)
⊢ HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ insert a s, f i x

Tactic:
simpa [has] using hf.add (ih h)

Premises used: Function.HasTemperateGrowth.add
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
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.insert a s, HasTemperateGrowth (f i)),
    HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ Insert.insert a s, f i x
⊢ HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ 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)

Premises used: Insert.insert
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
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.insert a s, HasTemperateGrowth (f i)),
    HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ Insert.insert a s, f i x
⊢ HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ ∑ i ∈ 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)

Premises used: Insert.insert