awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
Goal:
D : Type u_4
E : Type u_5
V : Type u_7
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : NormedAddCommGroup V
inst_5 : NormedSpace ℝ V
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : MeasurableSpace D
μ : Measure D
inst_9 : BorelSpace D
inst_10 : FiniteDimensional ℝ D
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(D, E)
g : 𝓢(D, F)
L : E →L[ℝ] F →L[ℝ] V
v : D
⊢ Eq.{u_7 + 1} (α := V)
    (∫ (x : D),
      (((L : (a : E) → F →L[ℝ] V) ((f : (a : D) → E) x) : F →L[ℝ] V) : (a : F) → V) ((∂_{v} g : (a : D) → F) x : F) ∂μ)
    (-∫ (x : D),
        (((L : (a : E) → F →L[ℝ] V) ((∂_{v} f : (a : D) → E) x) : F →L[ℝ] V) : (a : F) → V)
          ((g : (a : D) → F) x : F) ∂μ)
have hf : ∀ (x : D),
  Membership.mem (γ := Set D) (tsupport.{u_4, u_8} (α := F) (⇑g : (a : D) → F)) x →
    HasLineDerivAt.{0, u_5, u_4} ℝ (F := E) ((⇑f : (a : D) → E) : (a : D) → E) ((∂_{v} f : (a : D) → E) x : E) x v
Tactic: apply integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable (v := v)
    (bilinLeftCLM L g.hasTemperateGrowth _).integrable
    (bilinLeftCLM L (∂_{v} g).hasTemperateGrowth _).integrable
    (bilinLeftCLM L g.hasTemperateGrowth _).integrable
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
Goal:
D : Type u_4
E : Type u_5
V : Type u_7
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : NormedAddCommGroup V
inst_5 : NormedSpace ℝ V
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : MeasurableSpace D
μ : Measure D
inst_9 : BorelSpace D
inst_10 : FiniteDimensional ℝ D
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(D, E)
g : 𝓢(D, F)
L : E →L[ℝ] F →L[ℝ] V
v : D
hf :
  ∀ (x : D),
    Membership.mem (γ := Set D) (tsupport.{u_4, u_8} (α := F) (⇑g : (a : D) → F)) x →
      HasLineDerivAt.{0, u_5, u_4} ℝ (F := E) ((⇑f : (a : D) → E) : (a : D) → E) ((∂_{v} f : (a : D) → E) x : E) x v
⊢ Eq.{u_7 + 1} (α := V)
    (∫ (x : D),
      (((L : (a : E) → F →L[ℝ] V) ((f : (a : D) → E) x) : F →L[ℝ] V) : (a : F) → V) ((∂_{v} g : (a : D) → F) x : F) ∂μ)
    (-∫ (x : D),
        (((L : (a : E) → F →L[ℝ] V) ((∂_{v} f : (a : D) → E) x) : F →L[ℝ] V) : (a : F) → V)
          ((g : (a : D) → F) x : F) ∂μ)
have hg : ∀ (x : D),
  Membership.mem (γ := Set D) (tsupport.{u_4, u_5} (α := E) (⇑f : (a : D) → E)) x →
    HasLineDerivAt.{0, u_8, u_4} ℝ (F := F) ((⇑g : (a : D) → F) : (a : D) → F) ((∂_{v} g : (a : D) → F) x : F) x v
Tactic: apply integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable (v := v)
    (bilinLeftCLM L g.hasTemperateGrowth _).integrable
    (bilinLeftCLM L (∂_{v} g).hasTemperateGrowth _).integrable
    (bilinLeftCLM L g.hasTemperateGrowth _).integrable
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
Goal:
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace ℝ F₁
inst_5 : NormedAddCommGroup F₂
inst_6 : NormedSpace ℝ F₂
inst_7 : NormedAddCommGroup F₃
inst_8 : NormedSpace ℝ F₃
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : BorelSpace E
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ Eq.{u_11 + 1} (α := F₃)
    (∫ (x : E),
      (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((f : (a : E) → F₁) x) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
        ((Δ g : (a : E) → F₂) x : F₂) ∂μ)
    (∫ (x : E),
      (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((Δ f : (a : E) → F₁) x) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
        ((g : (a : E) → F₂) x : F₂) ∂μ)
have simp_rw : Eq.{u_11 + 1} (α := F₃)
  (∫ (x : E),
    ∑ x_1 : Fin (Module.finrank ℝ E),
      (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((f : (a : E) → F₁) x) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
        ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) x_1 : E)
                (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) x_1 : E) g) :
              (a : E) → F₂)
            x :
          F₂) ∂μ)
  (∫ (x : E),
    ∑ c : Fin (Module.finrank ℝ E),
      (((L : (a : F₁) → F₂ →L[ℝ] F₃)
              ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) c : E)
                    (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) c : E) f) :
                  (a : E) → F₁)
                x) :
            F₂ →L[ℝ] F₃) :
          (a : F₂) → F₃)
        ((g : (a : E) → F₂) x : F₂) ∂μ)
Tactic: simp_rw [laplacian_eq_sum (stdOrthonormalBasis ℝ E), sum_apply, map_sum,
    ContinuousLinearMap.coe_sum', Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
Goal:
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace ℝ F₁
inst_5 : NormedAddCommGroup F₂
inst_6 : NormedSpace ℝ F₂
inst_7 : NormedAddCommGroup F₃
inst_8 : NormedSpace ℝ F₃
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : BorelSpace E
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ Eq.{u_11 + 1} (α := F₃)
    (∫ (x : E),
      ∑ x_1 : Fin (Module.finrank ℝ E),
        (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((f : (a : E) → F₁) x) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
          ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) x_1 : E)
                  (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) x_1 : E) g) :
                (a : E) → F₂)
              x :
            F₂) ∂μ)
    (∫ (x : E),
      ∑ c : Fin (Module.finrank ℝ E),
        (((L : (a : F₁) → F₂ →L[ℝ] F₃)
                ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) c : E)
                      (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) c : E) f) :
                    (a : E) → F₁)
                  x) :
              F₂ →L[ℝ] F₃) :
            (a : F₂) → F₃)
          ((g : (a : E) → F₂) x : F₂) ∂μ)
have rw : Eq.{u_11 + 1} (α := F₃)
  (∑ i : Fin (Module.finrank ℝ E),
    ∫ (a : E),
      (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((f : (a : E) → F₁) a) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
        ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) g) :
              (a : E) → F₂)
            a :
          F₂) ∂μ)
  (∑ i : Fin (Module.finrank ℝ E),
    ∫ (a : E),
      (((L : (a : F₁) → F₂ →L[ℝ] F₃)
              ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                    (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) f) :
                  (a : E) → F₁)
                a) :
            F₂ →L[ℝ] F₃) :
          (a : F₂) → F₃)
        ((g : (a : E) → F₂) a : F₂) ∂μ)
Tactic: rw [MeasureTheory.integral_finsetSum, MeasureTheory.integral_finsetSum]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
Goal:
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace ℝ F₁
inst_5 : NormedAddCommGroup F₂
inst_6 : NormedSpace ℝ F₂
inst_7 : NormedAddCommGroup F₃
inst_8 : NormedSpace ℝ F₃
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : BorelSpace E
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
rw :
  Eq.{u_11 + 1} (α := F₃)
    (∑ i : Fin (Module.finrank ℝ E),
      ∫ (a : E),
        (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((f : (a : E) → F₁) a) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
          ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                  (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) g) :
                (a : E) → F₂)
              a :
            F₂) ∂μ)
    (∑ i : Fin (Module.finrank ℝ E),
      ∫ (a : E),
        (((L : (a : F₁) → F₂ →L[ℝ] F₃)
                ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                      (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) f) :
                    (a : E) → F₁)
                  a) :
              F₂ →L[ℝ] F₃) :
            (a : F₂) → F₃)
          ((g : (a : E) → F₂) a : F₂) ∂μ)
⊢ Eq.{u_11 + 1} (α := F₃)
    (∫ (x : E),
      ∑ x_1 : Fin (Module.finrank ℝ E),
        (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((f : (a : E) → F₁) x) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
          ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) x_1 : E)
                  (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) x_1 : E) g) :
                (a : E) → F₂)
              x :
            F₂) ∂μ)
    (∫ (x : E),
      ∑ c : Fin (Module.finrank ℝ E),
        (((L : (a : F₁) → F₂ →L[ℝ] F₃)
                ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) c : E)
                      (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) c : E) f) :
                    (a : E) → F₁)
                  x) :
              F₂ →L[ℝ] F₃) :
            (a : F₂) → F₃)
          ((g : (a : E) → F₂) x : F₂) ∂μ)
have hf : ∀ (i : Fin (Module.finrank ℝ E)),
  Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i →
    Integrable.{u_11, u_5} (ε := F₃)
      (fun (x : E) ↦
        (((L : (a : F₁) → F₂ →L[ℝ] F₃)
                ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                      (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) f) :
                    (a : E) → F₁)
                  x) :
              F₂ →L[ℝ] F₃) :
            (a : F₂) → F₃)
          ((g : (a : E) → F₂) x : F₂))
      μ
Tactic: rw [MeasureTheory.integral_finsetSum, MeasureTheory.integral_finsetSum]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
⊢ 𝓢(V, E) →L[𝕜] 𝓢(V, E)
have refine_1 : ∀ (f g : 𝓢(V, E)) (x : V),
  (fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) (f + g) x =
    HAdd.hAdd (α := E) ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f x)
      ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) g x)
Tactic: refine mkCLM ((𝓕 : (V → E) → (V → E)) ·) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
refine_1 :
  ∀ (f g : 𝓢(V, E)) (x : V),
    (fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) (f + g) x =
      HAdd.hAdd (α := E) ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f x)
        ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) g x)
⊢ 𝓢(V, E) →L[𝕜] 𝓢(V, E)
have refine_2 : ∀ (a : 𝕜) (f : 𝓢(V, E)) (x : V),
  (fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) (a • f) x =
    HSMul.hSMul (α := 𝕜) (β := E) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)
      ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f x)
Tactic: refine mkCLM ((𝓕 : (V → E) → (V → E)) ·) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
refine_1 :
  ∀ (f g : 𝓢(V, E)) (x : V),
    (fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) (f + g) x =
      HAdd.hAdd (α := E) ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f x)
        ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) g x)
refine_2 :
  ∀ (a : 𝕜) (f : 𝓢(V, E)) (x : V),
    (fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) (a • f) x =
      HSMul.hSMul (α := 𝕜) (β := E) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)
        ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f x)
⊢ 𝓢(V, E) →L[𝕜] 𝓢(V, E)
have refine_3 : ∀ (f : 𝓢(V, E)),
  ContDiff.{0, u_3, u_2} ℝ (E := V) (F := E) (↑⊤ : WithTop ℕ∞)
    ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f)
Tactic: refine mkCLM ((𝓕 : (V → E) → (V → E)) ·) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
refine_1 :
  ∀ (f g : 𝓢(V, E)) (x : V),
    (fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) (f + g) x =
      HAdd.hAdd (α := E) ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f x)
        ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) g x)
refine_2 :
  ∀ (a : 𝕜) (f : 𝓢(V, E)) (x : V),
    (fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) (a • f) x =
      HSMul.hSMul (α := 𝕜) (β := E) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)
        ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f x)
refine_3 :
  ∀ (f : 𝓢(V, E)),
    ContDiff.{0, u_3, u_2} ℝ (E := V) (F := E) (↑⊤ : WithTop ℕ∞)
      ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f)
⊢ 𝓢(V, E) →L[𝕜] 𝓢(V, E)
have refine_4 : ∀ (n : ℕ × ℕ),
  ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(V, E)) (x : V),
        ‖x‖ ^ n.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin n.2) ↦ V) E)
              (iteratedFDeriv ℝ n.2 ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f) x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 V E) : (a : 𝓢(V, E)) → ℝ) f : ℝ)
Tactic: refine mkCLM ((𝓕 : (V → E) → (V → E)) ·) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(V, E)) (x : V),
        ‖x‖ ^ (k, n).1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin (k, n).2) ↦ V) E)
              (iteratedFDeriv ℝ (k, n).2 ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f) x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 V E) : (a : 𝓢(V, E)) → ℝ) f : ℝ)
have refine_4 : ∀ (f : 𝓢(V, E)) (x : V),
  ‖x‖ ^ (k, n).1 *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin (k, n).2) ↦ V) E)
        (iteratedFDeriv ℝ (k, n).2 ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f) x) ≤
    HMul.hMul (β := ℝ)
      (((2 * π) ^ n * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
              (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
            HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        2)
      (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
              (schwartzSeminormFamily 𝕜 V E) :
            (a : 𝓢(V, E)) → ℝ)
          f :
        ℝ)
Tactic: refine ⟨Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1),
      (2 * π) ^ n * (2 * n + 2) ^ k * (Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card *
        2 ^ integrablePower (volume : Measure V) *
        (∫ x : V, (1 + ‖x‖) ^ (- integrablePower (volume : Measure V) : ℝ)) * 2, by positivity,
      fun f x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
⊢ ‖x‖ ^ (k, n).1 *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin (k, n).2) ↦ V) E)
        (iteratedFDeriv ℝ (k, n).2 ((fun (x : 𝓢(V, E)) ↦ 𝓕 (E := V → E) (⇑x : (a : V) → E)) f) x) ≤
    HMul.hMul (β := ℝ)
      (((2 * π) ^ n * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
              (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
            HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        2)
      (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
              (schwartzSeminormFamily 𝕜 V E) :
            (a : 𝓢(V, E)) → ℝ)
          f :
        ℝ)
have refine_4 : ((2 * π) ^ (k, n).2 * (HMul.hMul (α := ℝ) 2 (↑(k, n).2 : ℝ) + 2) ^ (k, n).1 *
    ∑ p ∈ Finset.range ((k, n).2 + 1) ×ˢ Finset.range ((k, n).1 + 1),
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
  HMul.hMul (β := ℝ)
    (((2 * π) ^ n * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
            (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
          HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
      2)
    (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
            (schwartzSeminormFamily 𝕜 V E) :
          (a : 𝓢(V, E)) → ℝ)
        f :
      ℝ)
Tactic: apply (pow_mul_norm_iteratedFDeriv_fourier_le (f.smooth ⊤)
      (fun k n _hk _hn ↦ integrable_pow_mul_iteratedFDeriv _ f k n) le_top le_top x).trans
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
⊢ ((2 * π) ^ (k, n).2 * (HMul.hMul (α := ℝ) 2 (↑(k, n).2 : ℝ) + 2) ^ (k, n).1 *
      ∑ p ∈ Finset.range ((k, n).2 + 1) ×ˢ Finset.range ((k, n).1 + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
    HMul.hMul (β := ℝ)
      (((2 * π) ^ n * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
              (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
            HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        2)
      (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
              (schwartzSeminormFamily 𝕜 V E) :
            (a : 𝓢(V, E)) → ℝ)
          f :
        ℝ)
have refine_4 : (2 * π) ^ n *
    ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
      ∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
  (2 * π) ^ n *
    ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
      ((↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
        (HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
          ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
              HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
            HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
              (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                      (schwartzSeminormFamily 𝕜 V E) :
                    (a : 𝓢(V, E)) → ℝ)
                  f :
                ℝ)))))
Tactic: simp only [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
⊢ (2 * π) ^ n *
      ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
        ∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            ‖v‖ ^ p.1 *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
                (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
    (2 * π) ^ n *
      ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k *
        ((↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
          (HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
            ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
                HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
              HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
                (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                        (schwartzSeminormFamily 𝕜 V E) :
                      (a : 𝓢(V, E)) → ℝ)
                    f :
                  ℝ)))))
have refine_4 : (∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      ‖v‖ ^ p.1 *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
          (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
  (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
    (HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
      ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
          (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                  (schwartzSeminormFamily 𝕜 V E) :
                (a : 𝓢(V, E)) → ℝ)
              f :
            ℝ)))
Tactic: gcongr