awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
⊢ MemSobolev s 2
    (HSMul.hSMul (β := 𝓢'(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
      ((fourierMultiplierCLM F fun (x : E) ↦
              (↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ) :
            (a : 𝓢'(E, F)) → 𝓢'(E, F))
          f :
        𝓢'(E, F)))
have apply : ∃ (C : ℝ), ∀ (x : E), ‖(↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ)‖ ≤ C
Tactic: apply (hf.fourierMultiplierCLM_of_bounded (by fun_prop) ?_).smul
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
⊢ ∃ (C : ℝ), ∀ (x : E), ‖(↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ)‖ ≤ C
have h : ∀ (x : E), ‖(↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ)‖ ≤ 1
Tactic: use 1
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
x : E
⊢ ‖(↑(HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) (-1)) : ℂ)‖ ≤ 1
have h : ‖(↑(HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 1)⁻¹) : ℂ)‖ ≤ 1
Tactic: rw [Real.rpow_neg (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
x : E
⊢ ‖(↑(HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℝ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 1)⁻¹) : ℂ)‖ ≤ 1
have h : ‖HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 1)⁻¹‖ ≤ 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
x : E
⊢ ‖HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 1)⁻¹‖ ≤ 1
have h : HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℕ) |1 + HPow.hPow (β := ℕ) ‖x‖ 2| 1)⁻¹ ≤ 1
Tactic: simp only [norm_mul, norm_pow, abs_norm, norm_inv, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Sobolev (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : InnerProductSpace ℂ F
inst_7 : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
x : E
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℕ) |1 + HPow.hPow (β := ℕ) ‖x‖ 2| 1)⁻¹ ≤ 1
have h : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ 1 * HPow.hPow (β := ℕ) (1 + HPow.hPow (β := ℕ) ‖x‖ 2) 1
Tactic: rw [abs_of_nonneg (by positivity), mul_inv_le_iff₀ (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst : FunLike F α β
inst_1 : TopologicalSpace α
inst_2 : Zero β
inst_3 : Zero V
f : F → V
x : α
⊢ Membership.mem (γ := Set α) (dsupport.{u_2, u_3, u_6, u_10} (β := β) f) x ↔
    ∀ (s : Set α), x ∈ s → IsOpen[inst_1] s → ∃ (u : F), tsupport.{u_2, u_3} (α := β) (⇑u : (a : α) → β) ⊆ s ∧ f u ≠ 0
have simp_rw : (∀ (s : Set α), x ∈ s → IsOpen[inst_1] s → ¬IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f s) ↔
  ∀ (s : Set α), x ∈ s → IsOpen[inst_1] s → ∃ (u : F), tsupport.{u_2, u_3} (α := β) (⇑u : (a : α) → β) ⊆ s ∧ f u ≠ 0
Tactic: simp_rw [mem_dsupport_iff_not_isVanishingOn, not_isVanishingOn_iff]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst : FunLike F α β
inst_1 : TopologicalSpace α
inst_2 : Zero β
inst_3 : Zero V
f : F → V
x : α
⊢ Membership.mem (γ := Set α) (dsupport.{u_2, u_3, u_6, u_10} (β := β) f) x ↔
    ∃ᶠ (u : Set α) in (𝓝 x).smallSets, ¬IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f u
have rw : Membership.mem (γ := Set α) (dsupport.{u_2, u_3, u_6, u_10} (β := β) f) x ↔
  ∀ (i : Set α), x ∈ i ∧ IsOpen[inst_1] i → ¬IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f i
Tactic: rw [nhds_basis_opens x |>.frequently_smallSets not_isVanishingOn_mono]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst : FunLike F α β
inst_1 : TopologicalSpace α
inst_2 : Zero β
inst_3 : Zero V
f : F → V
ι : Sort u_11
p : ι → Prop
s : ι → Set α
x : α
hl : (𝓝 x).HasBasis p s
⊢ Membership.mem (γ := Set α) (dsupport.{u_2, u_3, u_6, u_10} (β := β) f) x ↔
    ∀ (i : ι), p i → ¬IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f (s i)
have rw : (∃ᶠ (u : Set α) in (𝓝 x).smallSets, ¬IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f u) ↔
  ∀ (i : ι), p i → ¬IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f (s i)
Tactic: rw [mem_dsupport_iff_frequently]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst : FunLike F α β
inst_1 : TopologicalSpace α
inst_2 : Zero β
inst_3 : Zero V
f : F → V
s : Set α
h : IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f s
s_open : IsOpen[inst_1] s
⊢ Disjoint s (dsupport.{u_2, u_3, u_6, u_10} (β := β) f)
have rw : s ⊆ ⋃₀ {a : Set α | IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f a ∧ IsOpen[inst_1] a}
Tactic: rw [← Set.subset_compl_iff_disjoint_right, dsupport_compl_eq]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst : FunLike F α β
inst_1 : PseudoMetricSpace α
inst_2 : Zero β
inst_3 : Zero V
f : F → V
⊢ Eq.{u_2 + 1} (α := Set α) (dsupport.{u_2, u_3, u_6, u_10} (β := β) f)ᶜ
    (⋃₀
      {a : Set α |
        IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f a ∧
          IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧ Bornology.IsBounded a})
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (dsupport.{u_2, u_3, u_6, u_10} (β := β) f)ᶜ x ↔
    Membership.mem (γ := Set α)
      (⋃₀
        {a : Set α |
          IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f a ∧
            IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧ Bornology.IsBounded a})
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
f : 𝓢'(E, F)
s : Set E
hf : IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑f : (a : 𝓢(E, ℂ)) → F) s
g : E → ℂ
hg : Function.HasTemperateGrowth g
u : 𝓢(E, ℂ)
hu : tsupport (α := ℂ) (⇑u : (a : E) → ℂ) ⊆ s
⊢ Eq.{u_6 + 1} (α := F)
    ((((TemperedDistribution.smulLeftCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
    (0 : F)
have apply : tsupport (α := ℂ)
    (⇑(((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (a : E) → ℂ) ⊆
  s
Tactic: apply hf ((SchwartzMap.smulLeftCLM ℂ g) u)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
f : 𝓢'(E, F)
s : Set E
hf : IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑f : (a : 𝓢(E, ℂ)) → F) s
g : E → ℂ
hg : Function.HasTemperateGrowth g
u : 𝓢(E, ℂ)
hu : tsupport (α := ℂ) (⇑u : (a : E) → ℂ) ⊆ s
⊢ tsupport (α := ℂ)
      (⇑(((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (a : E) → ℂ) ⊆
    s
have rw : (tsupport (α := ℂ) fun (x : E) ↦ HSMul.hSMul (β := ℂ) (g x) ((u : (a : E) → ℂ) x : ℂ)) ⊆ s
Tactic: rw [SchwartzMap.smulLeftCLM_apply hg]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
f : 𝓢'(E, F)
s : Set E
hf : IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑f : (a : 𝓢(E, ℂ)) → F) s
m : E
u : 𝓢(E, ℂ)
hu : tsupport (α := ℂ) (⇑u : (a : E) → ℂ) ⊆ s
⊢ Eq.{u_6 + 1} (α := F) ((∂_{m} f : (a : 𝓢(E, ℂ)) → F) u : F) (0 : F)
have simp : Eq.{u_6 + 1} (α := F) ((f : (a : 𝓢(E, ℂ)) → F) (∂_{m} u) : F) (0 : F)
Tactic: simp only [lineDerivOp_apply_apply, map_neg, neg_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
f : 𝓢'(E, F)
s : Set E
n : ℕ
hf : IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑f : (a : 𝓢(E, ℂ)) → F) s
m : Fin n → E
⊢ IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑(∂^{m} f) : (a : 𝓢(E, ℂ)) → F) s
have zero : ∀ (m : Fin 0 → E), IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑(∂^{m} f) : (a : 𝓢(E, ℂ)) → F) s
Tactic: induction n with
  | zero =>
    exact hf
  | succ n IH =>
    exact (IH <| Fin.tail m).lineDerivOp (m 0)
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
f : 𝓢'(E, F)
s : Set E
n : ℕ
hf : IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑f : (a : 𝓢(E, ℂ)) → F) s
m : Fin n → E
zero :
  ∀ (m : Fin 0 → E),
    IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑(∂^{m} f) : (a : 𝓢(E, ℂ)) → F) s
⊢ IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑(∂^{m} f) : (a : 𝓢(E, ℂ)) → F) s
have succ : ∀ (n : ℕ)
  (IH :
    ∀ (m : Fin n → E),
      IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑(∂^{m} f) : (a : 𝓢(E, ℂ)) → F) s)
  (m : Fin (n + 1) → E),
  IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑(∂^{m} f) : (a : 𝓢(E, ℂ)) → F) s
Tactic: induction n with
  | zero =>
    exact hf
  | succ n IH =>
    exact (IH <| Fin.tail m).lineDerivOp (m 0)
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
u : 𝓢(E, ℂ)
hu : Subset (α := Set E) (tsupport (α := ℂ) (⇑u : (a : E) → ℂ)) {x}ᶜ
⊢ Eq (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) u : ℂ) (0 : ℂ)
have hu₁ : x ∉ tsupport (α := ℂ) (⇑u : (a : E) → ℂ)
Tactic: rw [Set.subset_compl_singleton_iff] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
f : 𝓢'(E, F)
g : E → ℂ
hg : Function.HasTemperateGrowth g
⊢ Subset.{u_5} (α := Set E)
    (dsupport.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F)
      (⇑((TemperedDistribution.smulLeftCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F))
    (dsupport.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑f : (a : 𝓢(E, ℂ)) → F))
have h : ∀ (s : Set E),
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s →
    IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑f : (a : 𝓢(E, ℂ)) → F) s →
      IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F)
        (⇑((TemperedDistribution.smulLeftCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
f : 𝓢'(E, F)
m : E
⊢ Subset.{u_5} (α := Set E)
    (dsupport.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑(∂_{m} f) : (a : 𝓢(E, ℂ)) → F))
    (dsupport.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑f : (a : 𝓢(E, ℂ)) → F))
have h : ∀ (s : Set E),
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s →
    IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑f : (a : 𝓢(E, ℂ)) → F) s →
      IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑(∂_{m} f) : (a : 𝓢(E, ℂ)) → F) s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
f : 𝓢'(E, F)
n : ℕ
m : Fin n → E
⊢ Subset.{u_5} (α := Set E)
    (dsupport.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑(∂^{m} f) : (a : 𝓢(E, ℂ)) → F))
    (dsupport.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑f : (a : 𝓢(E, ℂ)) → F))
have h : ∀ (s : Set E),
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s →
    IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑f : (a : 𝓢(E, ℂ)) → F) s →
      IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑(∂^{m} f) : (a : 𝓢(E, ℂ)) → F) s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
⊢ Eq (α := Set E) (dsupport (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ)) {x}
have a : Subset (α := Set E) (dsupport (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ))
  {x}
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
a :
  Subset (α := Set E) (dsupport (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ))
    {x}
⊢ Eq (α := Set E) (dsupport (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ)) {x}
have a₁ : Subset (α := Set E) {x}
  (dsupport (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ))
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x x' : E
hx' :
  Membership.mem (γ := Set E)
    (dsupport (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ)) x'
⊢ Membership.mem (γ := Set E) {x} x'
have hx'₁ : ∀ (s : Set E),
  IsVanishingOn (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ) sᶜ →
    IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → x' ∈ s
Tactic: rw [mem_dsupport_iff] at hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
⊢ Membership.mem (γ := Set E)
    (dsupport (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ)) x
have a : ∀ (s : Set E),
  x ∈ s →
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s →
      ∃ (u : 𝓢(E, ℂ)),
        tsupport (α := ℂ) (⇑u : (a : E) → ℂ) ⊆ s ∧
          Ne (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) u : ℂ) (0 : ℂ)
Tactic: rw [mem_dsupport_iff_forall_exists_ne]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ∃ (u : 𝓢(E, ℂ)),
    tsupport (α := ℂ) (⇑u : (a : E) → ℂ) ⊆ s ∧
      Ne (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) u : ℂ) (0 : ℂ)
have a : ∀ (u : E → ℝ) (h₁ : tsupport u ⊆ s) (h₂ : HasCompactSupport u) (h₃ : ContDiff ℝ (↑⊤ : WithTop ℕ∞) u) (h₄ : u x = 1),
  ∃ (u : 𝓢(E, ℂ)),
    tsupport (α := ℂ) (⇑u : (a : E) → ℂ) ⊆ s ∧
      Ne (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) u : ℂ) (0 : ℂ)
Tactic: obtain ⟨u, h₁, h₂, h₃, -, h₄⟩ :=
    exists_contDiff_tsupport_subset (n := ⊤) ((IsOpen.mem_nhds_iff hs).mpr hx)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
u : E → ℝ
h₁ : tsupport u ⊆ s
h₂ : HasCompactSupport u
h₃ : ContDiff ℝ (↑⊤ : WithTop ℕ∞) u
h₄ : u x = 1
⊢ ∃ (u : 𝓢(E, ℂ)),
    tsupport (α := ℂ) (⇑u : (a : E) → ℂ) ⊆ s ∧
      Ne (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) u : ℂ) (0 : ℂ)
have h₁' : tsupport (α := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ u) ⊆ s
Tactic: have h₁' : tsupport (Complex.ofRealCLM ∘ u) ⊆ s := (tsupport_comp_subset rfl _).trans h₁
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
u : E → ℝ
h₁ : tsupport u ⊆ s
h₂ : HasCompactSupport u
h₃ : ContDiff ℝ (↑⊤ : WithTop ℕ∞) u
h₄ : u x = 1
h₁' : tsupport (α := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ u) ⊆ s
⊢ ∃ (u : 𝓢(E, ℂ)),
    tsupport (α := ℂ) (⇑u : (a : E) → ℂ) ⊆ s ∧
      Ne (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) u : ℂ) (0 : ℂ)
have h₂' : HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ u)
Tactic: have h₂' : HasCompactSupport (Complex.ofRealCLM ∘ u) := h₂.comp_left rfl
-- Lean 4 proof step from Mathlib.Analysis.Distribution.Support (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
u : E → ℝ
h₁ : tsupport u ⊆ s
h₂ : HasCompactSupport u
h₃ : ContDiff ℝ (↑⊤ : WithTop ℕ∞) u
h₄ : u x = 1
h₁' : tsupport (α := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ u) ⊆ s
h₂' : HasCompactSupport (β := ℂ) ((⇑Complex.ofRealCLM : (a : ℝ) → ℂ) ∘ u)
⊢ ∃ (u : 𝓢(E, ℂ)),
    tsupport (α := ℂ) (⇑u : (a : E) → ℂ) ⊆ s ∧
      Ne (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) u : ℂ) (0 : ℂ)
have h : tsupport (α := ℂ) (⇑(h₂'.toSchwartzMap sorry) : (a : E) → ℂ) ⊆ s ∧
  Ne (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) (h₂'.toSchwartzMap sorry) : ℂ) (0 : ℂ)
Tactic: use h₂'.toSchwartzMap (Complex.ofRealCLM.contDiff.comp h₃)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (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
⊢ HasTemperateGrowth f ↔
    ContDiff ℝ ∞ f ∧
      ∀ (n : ℕ),
        ∃ (k : ℕ),
          IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
            (iteratedFDeriv ℝ n f) fun (x : E) ↦ (1 + ‖x‖) ^ k
have simp_rw : HasTemperateGrowth f ↔
  ContDiff ℝ ∞ f ∧
    ∀ (n : ℕ),
      ∃ (k : ℕ) (C : ℝ),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
            C * ‖(1 + ‖x‖) ^ k‖
Tactic: simp_rw [Asymptotics.isBigO_top]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (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
⊢ HasTemperateGrowth f ↔
    ContDiff ℝ ∞ f ∧
      ∀ (n : ℕ),
        ∃ (k : ℕ) (C : ℝ),
          ∀ (x : E),
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
              C * ‖(1 + ‖x‖) ^ k‖
have a : ∀ (n k : ℕ) (C : ℝ) (x : E), (1 + ‖x‖) ^ k = ‖(1 + ‖x‖) ^ k‖
Tactic: congrm ContDiff ℝ ∞ f ∧ (∀ n, ∃ k C, ∀ x, _ ≤ C * ?_)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (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
n k : ℕ
C : ℝ
x : E
⊢ (1 + ‖x‖) ^ k = ‖(1 + ‖x‖) ^ k‖
have a : (1 + ‖x‖) ^ k = ‖1 + ‖x‖‖ ^ k
Tactic: rw [norm_pow, Real.norm_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (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
n k : ℕ
C : ℝ
x : E
a : (1 + ‖x‖) ^ k = ‖1 + ‖x‖‖ ^ k
⊢ (1 + ‖x‖) ^ k = ‖(1 + ‖x‖) ^ k‖
have a₁ : (1 + ‖x‖) ^ k = (1 + ‖x‖) ^ k
Tactic: rw [norm_pow, Real.norm_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (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
hf_temperate : HasTemperateGrowth f
N : ℕ
⊢ ∃ (k : ℕ),
    ∀ n ≤ N,
      IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
        (iteratedFDeriv ℝ n f) fun (x : E) ↦ (1 + ‖x‖) ^ k
have choose : ∀ (k : (n : ℕ) → ℕ)
  (hk :
    ∀ (n : ℕ),
      IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
        (iteratedFDeriv ℝ n f) fun (x : E) ↦ (1 + ‖x‖) ^ k n),
  ∃ (k : ℕ),
    ∀ n ≤ N,
      IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
        (iteratedFDeriv ℝ n f) fun (x : E) ↦ (1 + ‖x‖) ^ k
Tactic: choose k hk using hf_temperate.isBigO
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (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
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤ (iteratedFDeriv ℝ n f)
      fun (x : E) ↦ (1 + ‖x‖) ^ k n
⊢ ∃ (k : ℕ),
    ∀ n ≤ N,
      IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤
        (iteratedFDeriv ℝ n f) fun (x : E) ↦ (1 + ‖x‖) ^ k
have h : ∀ n ≤ N,
  IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤ (iteratedFDeriv ℝ n f)
    fun (x : E) ↦ (1 + ‖x‖) ^ (Finset.range (N + 1)).sup k
Tactic: use (Finset.range (N + 1)).sup k