awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this :
  ∀ (i : Fin (Module.finrank ℝ E)) (hi : Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i),
    Function.HasTemperateGrowth (F := ℂ) fun (x : E) ↦
      HPow.hPow (β := ℕ) (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ) 2
i : Fin (Module.finrank ℝ E)
x : 𝓢(E, ℂ)
⊢ 2 * (↑π : ℂ) * Complex.I * (2 * (↑π : ℂ) * Complex.I) = (↑(-HPow.hPow (β := ℕ) (2 * π) 2) : ℂ)
have e_f : HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) Complex.I 2 * 4 = (↑(-(HPow.hPow (β := ℕ) π 2 * 4)) : ℂ)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f g : 𝓢(E, F)
h : Eq (α := (a : E) → F) ((fun (f : 𝓢(E, F)) ↦ f.toFun) f) ((fun (f : 𝓢(E, F)) ↦ f.toFun) g)
⊢ f = g
have mk : ∀ (toFun : E → F) (smooth' : ContDiff ℝ ∞ toFun)
  (decay' :
    ∀ (k n : ℕ),
      ∃ (C : ℝ),
        ∀ (x : E),
          ‖x‖ ^ k *
              norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
                (iteratedFDeriv ℝ n toFun x) ≤
            C)
  (h :
    Eq (α := (a : E) → F) ((fun (f : 𝓢(E, F)) ↦ f.toFun) { toFun := toFun, smooth' := smooth', decay' := decay' })
      ((fun (f : 𝓢(E, F)) ↦ f.toFun) g)),
  { toFun := toFun, smooth' := smooth', decay' := decay' : 𝓢(E, F) } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
g : 𝓢(E, F)
toFun : E → F
smooth' : ContDiff ℝ ∞ toFun
decay' :
  ∀ (k n : ℕ),
    ∃ (C : ℝ),
      ∀ (x : E),
        ‖x‖ ^ k *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDeriv ℝ n toFun x) ≤
          C
h :
  Eq (α := (a : E) → F) ((fun (f : 𝓢(E, F)) ↦ f.toFun) { toFun := toFun, smooth' := smooth', decay' := decay' })
    ((fun (f : 𝓢(E, F)) ↦ f.toFun) g)
⊢ { toFun := toFun, smooth' := smooth', decay' := decay' : 𝓢(E, F) } = g
have mk : ∀ (toFun_1 : E → F) (smooth'_1 : ContDiff ℝ ∞ toFun_1)
  (decay'_1 :
    ∀ (k n : ℕ),
      ∃ (C : ℝ),
        ∀ (x : E),
          ‖x‖ ^ k *
              norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
                (iteratedFDeriv ℝ n toFun_1 x) ≤
            C)
  (h :
    Eq (α := (a : E) → F) ((fun (f : 𝓢(E, F)) ↦ f.toFun) { toFun := toFun, smooth' := smooth', decay' := decay' })
      ((fun (f : 𝓢(E, F)) ↦ f.toFun) { toFun := toFun_1, smooth' := smooth'_1, decay' := decay'_1 })),
  { toFun := toFun, smooth' := smooth', decay' := decay' : 𝓢(E, F) } =
    { toFun := toFun_1, smooth' := smooth'_1, decay' := decay'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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)
k n : ℕ
⊢ ∃ (C : ℝ),
    0 < C ∧
      ∀ (x : E),
        ‖x‖ ^ k *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
          C
have rcases : ∀ (C : ℝ)
  (hC :
    ∀ (x : E),
      ‖x‖ ^ k *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n f.toFun x) ≤
        C),
  ∃ (C : ℝ),
    0 < C ∧
      ∀ (x : E),
        ‖x‖ ^ k *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
          C
Tactic: rcases f.decay' k n with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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)
k : ℕ
⊢ IsBigO.{u_5, u_6, 0} (E := F) (F := ℝ) (cocompact E) (⇑f : (a : E) → F) fun (x : E) ↦
    HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))
have obtain : ∀ (d : ℝ),
  0 < d →
    ∀
      (hd' :
        ∀ (x : E),
          ‖x‖ ^ k *
              norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F)
                (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x) ≤
            d),
      IsBigO.{u_5, u_6, 0} (E := F) (F := ℝ) (cocompact E) (⇑f : (a : E) → F) fun (x : E) ↦
        HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))
Tactic: obtain ⟨d, _, hd'⟩ := f.decay k 0
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : 𝓢(E, F)
k : ℕ
d : ℝ
left : 0 < d
hd' :
  ∀ (x : E),
    ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F)
          (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x) ≤
      d
⊢ IsBigO.{u_5, u_6, 0} (E := F) (F := ℝ) (cocompact E) (⇑f : (a : E) → F) fun (x : E) ↦
    HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))
have hd'₁ : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
Tactic: simp only [norm_iteratedFDeriv_zero] at hd'
Cleared hypotheses: hd'
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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)
k : ℕ
d : ℝ
left : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
⊢ IsBigO.{u_5, u_6, 0} (E := F) (F := ℝ) (cocompact E) (⇑f : (a : E) → F) fun (x : E) ↦
    HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))
have simp_rw : ∃ (c : ℝ),
  ∀ᶠ (x : E) in cocompact E, norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))‖
Tactic: simp_rw [Asymptotics.IsBigO, Asymptotics.IsBigOWith]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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)
k : ℕ
d : ℝ
left : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : E) in cocompact E, norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))‖
have refine : ∀ᶠ (x : E) in cofinite, norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d * ‖HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))‖
Tactic: refine ⟨d, Filter.Eventually.filter_mono Filter.cocompact_le_cofinite ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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)
k : ℕ
d : ℝ
left : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
⊢ ∀ᶠ (x : E) in cofinite, norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d * ‖HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))‖
have refine : ∀ (x : E) (hx : x ≠ 0), norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d * ‖HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))‖
Tactic: refine (Filter.eventually_cofinite_ne 0).mono fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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)
k : ℕ
d : ℝ
left : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
x : E
hx : x ≠ 0
⊢ norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d * ‖HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))‖
have rw : HPow.hPow (β := ℤ) ‖x‖ (↑k : ℤ) * norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ d
Tactic: rw [Real.norm_of_nonneg (by positivity), zpow_neg, ← div_eq_mul_inv, le_div_iff₀' (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : 𝓢(E, F)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
⊢ IsBigO.{u_5, u_6, 0} (E := F) (F := ℝ) (cocompact E) (⇑f : (a : E) → F) fun (x : E) ↦ ‖x‖ ^ s
have hk : -(↑k : ℝ) ≤ s
Tactic: have hk : -(k : ℝ) ≤ s := neg_le.mp (Nat.le_ceil (-s))
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
⊢ IsBigO.{u_5, u_6, 0} (E := F) (F := ℝ) (cocompact E) (⇑f : (a : E) → F) fun (x : E) ↦ ‖x‖ ^ s
have refine : IsBigO (E := ℝ) (F := ℝ) (cocompact E) (fun (x : E) ↦ HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))) fun (x : E) ↦ ‖x‖ ^ s
Tactic: refine (isBigO_cocompact_zpow_neg_nat f k).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
⊢ IsBigO (E := ℝ) (F := ℝ) (cocompact E) (fun (x : E) ↦ HPow.hPow (β := ℤ) ‖x‖ (-(↑k : ℤ))) fun (x : E) ↦ ‖x‖ ^ s
have suffices : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℤ) x (-(↑k : ℤ))) fun (x : ℝ) ↦ x ^ s
Tactic: suffices (fun x : ℝ ↦ x ^ (-k : ℤ)) =O[atTop] fun x : ℝ ↦ x ^ s
    from this.comp_tendsto tendsto_norm_cocompact_atTop
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℤ) x (-(↑k : ℤ))) fun (x : ℝ) ↦ x ^ s
have simp_rw : ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, ‖HPow.hPow (β := ℤ) x (-(↑k : ℤ))‖ ≤ c * ‖x ^ s‖
Tactic: simp_rw [Asymptotics.IsBigO, Asymptotics.IsBigOWith]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, ‖HPow.hPow (β := ℤ) x (-(↑k : ℤ))‖ ≤ c * ‖x ^ s‖
have refine : ∀ (x : ℝ) (hx : 1 ≤ x), ‖HPow.hPow (β := ℤ) x (-(↑k : ℤ))‖ ≤ 1 * ‖x ^ s‖
Tactic: refine ⟨1, (Filter.eventually_ge_atTop 1).mono fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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)
inst_4 : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -(↑k : ℝ) ≤ s
x : ℝ
hx : 1 ≤ x
⊢ ‖HPow.hPow (β := ℤ) x (-(↑k : ℤ))‖ ≤ 1 * ‖x ^ s‖
have rw : HPow.hPow (β := ℝ) x (-(↑k : ℝ)) ≤ x ^ s
Tactic: rw [one_mul, Real.norm_of_nonneg (by positivity), Real.norm_of_nonneg (by positivity),
    ← Real.rpow_intCast, Int.cast_neg, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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
inst_4 : ProperSpace E
f : 𝓢(E, F)
⊢ Tendsto.{u_5, u_6} (β := F) (⇑f : (a : E) → F) (cocompact E) (𝓝 0)
have apply : Tendsto (β := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) ‖x‖ (-1)) (cocompact E) (𝓝 0)
Tactic: apply (isBigO_cocompact_rpow f (-1)).trans_tendsto
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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
inst_4 : ProperSpace E
f : 𝓢(E, F)
⊢ Tendsto (β := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) ‖x‖ (-1)) (cocompact E) (𝓝 0)
have simp_rw : Tendsto (β := ℝ) (fun (x : E) ↦ ‖x‖⁻¹) (cocompact E) (𝓝 0)
Tactic: simp_rw [Real.rpow_neg_one]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
    ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x)
have rw : ‖x‖ ^ k *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
  ‖x‖ ^ k *
    (norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x))
Tactic: rw [← mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
    ‖x‖ ^ k *
      (norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x))
have hbc : norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
    (iteratedFDeriv ℝ n (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
  norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x)
Tactic: gcongr _ * ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x)
have hbc : ‖HAdd.hAdd (α := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x)‖ ≤
  norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x)
Tactic: rw [iteratedFDeriv_add_apply (f.smooth _).contDiffAt (g.smooth _).contDiffAt]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (-(⇑f : (a : E) → F)) x) =
    ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
have rw : ‖x‖ ^ k *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (-iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) =
  ‖x‖ ^ k *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
Tactic: rw [iteratedFDeriv_neg_apply, norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (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
k n : ℕ
f : 𝓢(E, F)
x : E
rw :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (-iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) =
    ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (-(⇑f : (a : E) → F)) x) =
    ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
have rw₁ : ‖x‖ ^ k *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) =
  ‖x‖ ^ k *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
Tactic: rw [iteratedFDeriv_neg_apply, norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(E, F)
c : 𝕜
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
    ‖c‖ * ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
have rw : ‖x‖ ^ k *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
  ‖x‖ ^ k * ‖c‖ *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
Tactic: rw [mul_comm ‖c‖, mul_assoc, iteratedFDeriv_const_smul_apply (f.smooth _).contDiffAt,
    norm_smul c (iteratedFDeriv ℝ n (⇑f) x)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(E, F)
c : 𝕜
x : E
rw :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
    ‖x‖ ^ k * ‖c‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
    ‖c‖ * ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
have rw₁ : ‖x‖ ^ k *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
  ‖x‖ ^ k *
    (‖c‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
Tactic: rw [mul_comm ‖c‖, mul_assoc, iteratedFDeriv_const_smul_apply (f.smooth _).contDiffAt,
    norm_smul c (iteratedFDeriv ℝ n (⇑f) x)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(E, F)
c : 𝕜
x : E
rw :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
    ‖x‖ ^ k * ‖c‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
rw₁ :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
    ‖x‖ ^ k *
      (‖c‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
    ‖c‖ * ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
have rw₂ : ‖x‖ ^ k *
    ‖HSMul.hSMul (β := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) c
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)‖ =
  ‖x‖ ^ k *
    (‖c‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
Tactic: rw [mul_comm ‖c‖, mul_assoc, iteratedFDeriv_const_smul_apply (f.smooth _).contDiffAt,
    norm_smul c (iteratedFDeriv ℝ n (⇑f) x)]