awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.Support
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 α), IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f sᶜ → IsClosed[inst_1] s → x ∈ s

Tactic:
simp [dsupport]

Premises used: Distribution.dsupport
-- Module: Mathlib.Analysis.Distribution.Support
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
⊢ 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[inst_1] a})

Tactic:
simp [dsupport, Set.compl_sInter, Set.compl_image_set_of]

Premises used: Set.compl_sInter, Distribution.dsupport, Set.compl_image_set_of
-- Module: Mathlib.Analysis.Distribution.Support
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 : α
⊢ x ∉ dsupport.{u_2, u_3, u_6, u_10} (β := β) f ↔
    ∃ (s : Set α), IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f s ∧ IsOpen[inst_1] s ∧ x ∈ s

Tactic:
simp [← Set.mem_compl_iff, dsupport_compl_eq, Set.mem_sUnion, and_assoc]

Premises used: and_assoc, Distribution.dsupport_compl_eq, Set.mem_sUnion, Set.mem_compl_iff
-- Module: Mathlib.Analysis.Distribution.Support
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 → ¬IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f s

Tactic:
grind only [notMem_dsupport_iff]

Premises used: Distribution.notMem_dsupport_iff
-- Module: Mathlib.Analysis.Distribution.Support
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 : α
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
⊢ 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

Tactic:
simp_rw [mem_dsupport_iff_not_isVanishingOn, not_isVanishingOn_iff]

Premises used: Distribution.mem_dsupport_iff_not_isVanishingOn, Distribution.not_isVanishingOn_iff
-- Module: Mathlib.Analysis.Distribution.Support
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 : α
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
⊢ 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

Tactic:
rw [nhds_basis_opens x |>.frequently_smallSets not_isVanishingOn_mono]

Premises used: Filter.HasBasis.frequently_smallSets, Distribution.not_isVanishingOn_mono
-- Module: Mathlib.Analysis.Distribution.Support
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 ↔
    ∀ (i : Set α), x ∈ i ∧ IsOpen[inst_1] i → ¬IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f i

Tactic:
simpa using mem_dsupport_iff_not_isVanishingOn x

Premises used: Distribution.mem_dsupport_iff_not_isVanishingOn
-- Module: Mathlib.Analysis.Distribution.Support
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
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)
⊢ 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)

Tactic:
rw [mem_dsupport_iff_frequently]

Premises used: Distribution.mem_dsupport_iff_frequently
-- Module: Mathlib.Analysis.Distribution.Support
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
⊢ (∃ᶠ (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:
hl.frequently_smallSets not_isVanishingOn_mono

Premises used: Filter.HasBasis.frequently_smallSets, Distribution.not_isVanishingOn_mono
-- Module: Mathlib.Analysis.Distribution.Support
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
⊢ (∃ᶠ (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:
exact hl.frequently_smallSets not_isVanishingOn_mono

Premises used: Filter.HasBasis.frequently_smallSets, Distribution.not_isVanishingOn_mono
-- Module: Mathlib.Analysis.Distribution.Support
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 : α
⊢ x ∉ dsupport.{u_2, u_3, u_6, u_10} (β := β) f ↔
    ∀ᶠ (u : Set α) in (𝓝 x).smallSets, IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f u

Tactic:
simp [mem_dsupport_iff_frequently]

Premises used: Distribution.mem_dsupport_iff_frequently
-- Module: Mathlib.Analysis.Distribution.Support
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
⊢ x ∉ dsupport.{u_2, u_3, u_6, u_10} (β := β) f ↔ ∃ (i : ι), p i ∧ IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f (s i)

Tactic:
simp [hl.mem_dsupport]

Premises used: Filter.HasBasis.mem_dsupport
-- Module: Mathlib.Analysis.Distribution.Support
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 g : F → V
h :
  ∀ (s : Set α),
    IsOpen[inst_1] s →
      IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) g s → IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f s
⊢ Subset.{u_2} (α := Set α) (dsupport.{u_2, u_3, u_6, u_10} (β := β) f) (dsupport.{u_2, u_3, u_6, u_10} (β := β) g)

Tactic:
Set.sInter_mono fun s ⟨g_van, s_cl⟩ ↦ ⟨h sᶜ s_cl.isOpen_compl g_van, s_cl⟩

Premises used: IsClosed.isOpen_compl, Distribution.dsupport, Compl.compl, setOf, Membership.mem, IsClosed, _private.0.Distribution.dsupport_subset_dsupport.match_1, And, And.intro, Distribution.IsVanishingOn, Set.sInter_mono
-- Module: Mathlib.Analysis.Distribution.Support
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
⊢ IsClosed[inst_1] (dsupport.{u_2, u_3, u_6, u_10} (β := β) f)

Tactic:
grind [dsupport, isClosed_sInter]

Premises used: Distribution.dsupport, isClosed_sInter
-- Module: Mathlib.Analysis.Distribution.Support
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
rw : s ⊆ ⋃₀ {a : Set α | IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f a ∧ IsOpen[inst_1] a}
⊢ Disjoint s (dsupport.{u_2, u_3, u_6, u_10} (β := β) f)

Tactic:
rw [← Set.subset_compl_iff_disjoint_right, dsupport_compl_eq]

Premises used: Set.subset_compl_iff_disjoint_right, Distribution.dsupport_compl_eq
-- Module: Mathlib.Analysis.Distribution.Support
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
⊢ s ⊆ ⋃₀ {a : Set α | IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f a ∧ IsOpen[inst_1] a}

Tactic:
Set.subset_sUnion_of_mem ⟨h, s_open⟩

Premises used: And.intro, Set.subset_sUnion_of_mem
-- Module: Mathlib.Analysis.Distribution.Support
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
⊢ s ⊆ ⋃₀ {a : Set α | IsVanishingOn.{u_2, u_3, u_6, u_10} (β := β) f a ∧ IsOpen[inst_1] a}

Tactic:
exact Set.subset_sUnion_of_mem ⟨h, s_open⟩
-- Module: Mathlib.Analysis.Distribution.Support
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
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
⊢ 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})

Tactic:
ext x
-- Module: Mathlib.Analysis.Distribution.Support
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
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:
grind [(Metric.hasBasis_nhds_isOpen_isBounded x).notMem_dsupport]

Premises used: Filter.HasBasis.notMem_dsupport, Metric.hasBasis_nhds_isOpen_isBounded
-- Module: Mathlib.Analysis.Distribution.Support
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
apply :
  tsupport (α := ℂ)
      (⇑(((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (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)

Tactic:
apply hf ((SchwartzMap.smulLeftCLM ℂ g) u)

Premises used: SchwartzMap.smulLeftCLM, Complex, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.Support
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
rw : (tsupport (α := ℂ) fun (x : E) ↦ HSMul.hSMul (β := ℂ) (g x) ((u : (a : E) → ℂ) x : ℂ)) ⊆ s
⊢ tsupport (α := ℂ)
      (⇑(((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (a : E) → ℂ) ⊆
    s

Tactic:
rw [SchwartzMap.smulLeftCLM_apply hg]

Premises used: SchwartzMap.smulLeftCLM_apply
-- Module: Mathlib.Analysis.Distribution.Support
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 (α := ℂ) fun (x : E) ↦ HSMul.hSMul (β := ℂ) (g x) ((u : (a : E) → ℂ) x : ℂ)) ⊆ s

Tactic:
(tsupport_smul_subset_right g u).trans hu

Premises used: HasSubset.Subset.trans, tsupport_smul_subset_right, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.Support
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 (α := ℂ) fun (x : E) ↦ HSMul.hSMul (β := ℂ) (g x) ((u : (a : E) → ℂ) x : ℂ)) ⊆ s

Tactic:
exact (tsupport_smul_subset_right g u).trans hu

Premises used: HasSubset.Subset.trans, tsupport_smul_subset_right, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.Support
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
simp : Eq.{u_6 + 1} (α := F) ((f : (a : 𝓢(E, ℂ)) → F) (∂_{m} u) : F) (0 : F)
⊢ Eq.{u_6 + 1} (α := F) ((∂_{m} f : (a : 𝓢(E, ℂ)) → F) u : F) (0 : F)

Tactic:
simp only [lineDerivOp_apply_apply, map_neg, neg_eq_zero]

Premises used: neg_eq_zero, map_neg, TemperedDistribution.lineDerivOp_apply_apply
-- Module: Mathlib.Analysis.Distribution.Support
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) ((f : (a : 𝓢(E, ℂ)) → F) (∂_{m} u) : F) (0 : F)

Tactic:
hf (∂_{m} u) <| (tsupport_fderiv_apply_subset ℝ m).trans hu

Premises used: Real, HasSubset.Subset.trans, tsupport_fderiv_apply_subset, LineDeriv.lineDerivOp
-- Module: Mathlib.Analysis.Distribution.Support
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) ((f : (a : 𝓢(E, ℂ)) → F) (∂_{m} u) : F) (0 : F)

Tactic:
exact hf (∂_{m} u) <| (tsupport_fderiv_apply_subset ℝ m).trans hu

Premises used: Real, HasSubset.Subset.trans, tsupport_fderiv_apply_subset, LineDeriv.lineDerivOp
-- Module: Mathlib.Analysis.Distribution.Support
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 : Fin 0 → E
⊢ IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑(∂^{m} f) : (a : 𝓢(E, ℂ)) → F) s

Tactic:
hf

Premises used: LineDeriv.iteratedLineDerivOp
-- Module: Mathlib.Analysis.Distribution.Support
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 : Fin 0 → E
⊢ IsVanishingOn.{u_5, 0, u_5, u_6} (β := ℂ) (F := 𝓢(E, ℂ)) (V := F) (⇑(∂^{m} f) : (a : 𝓢(E, ℂ)) → F) s

Tactic:
exact hf
-- Module: Mathlib.Analysis.Distribution.Support
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
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:
(IH <| Fin.tail m).lineDerivOp (m 0)

Premises used: LineDeriv.iteratedLineDerivOp, OfNat.ofNat, Fin.tail, Distribution.IsVanishingOn.lineDerivOp
-- Module: Mathlib.Analysis.Distribution.Support
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
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:
exact (IH <| Fin.tail m).lineDerivOp (m 0)

Premises used: OfNat.ofNat, Fin.tail, Distribution.IsVanishingOn.lineDerivOp
-- Module: Mathlib.Analysis.Distribution.Support
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
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
⊢ 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)
-- Module: Mathlib.Analysis.Distribution.Support
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}ᶜ
⊢ x ∉ tsupport (α := ℂ) (⇑u : (a : E) → ℂ)

Tactic:
rw [Set.subset_compl_singleton_iff] at hu

Premises used: Set.subset_compl_singleton_iff
-- Module: Mathlib.Analysis.Distribution.Support
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
u : 𝓢(E, ℂ)
hu : x ∉ tsupport (α := ℂ) (⇑u : (a : E) → ℂ)
⊢ Eq (α := ℂ) ((TemperedDistribution.delta x : (a : 𝓢(E, ℂ)) → ℂ) u : ℂ) (0 : ℂ)

Tactic:
apply image_eq_zero_of_notMem_tsupport hu

Premises used: image_eq_zero_of_notMem_tsupport
-- Module: Mathlib.Analysis.Distribution.Support
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
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
⊢ 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))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Distribution.Support
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
⊢ ∀ (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:
fun_prop
-- Module: Mathlib.Analysis.Distribution.Support
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
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
⊢ 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))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Distribution.Support
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
⊢ ∀ (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:
fun_prop
-- Module: Mathlib.Analysis.Distribution.Support
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
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
⊢ 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))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Distribution.Support
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
⊢ ∀ (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:
fun_prop
-- Module: Mathlib.Analysis.Distribution.Support
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}
a₁ :
  Subset (α := Set E) {x}
    (dsupport (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ))
⊢ Eq (α := Set E) (dsupport (β := ℂ) (F := 𝓢(E, ℂ)) (V := ℂ) (⇑(TemperedDistribution.delta x) : (a : 𝓢(E, ℂ)) → ℂ)) {x}

Tactic:
apply subset_antisymm

Premises used: subset_antisymm