awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
m : E
h :
  ∀ (u : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F) ((∂_{m} (𝓕⁻ f) : (a : 𝓢(E, ℂ)) → F) u : F)
      ((𝓕⁻
              (HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
                ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
            (a : 𝓢(E, ℂ)) → F)
          u :
        F)
⊢ ∂_{m} (𝓕⁻ f) =
    𝓕⁻
      (HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
        ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)))

Tactic:
ext u
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
m : E
u : 𝓢(E, ℂ)
this : Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ inner ℝ x m
⊢ Eq.{u_4 + 1} (α := F) ((∂_{m} (𝓕⁻ f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((𝓕⁻
            (HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
              ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)

Tactic:
simp [SchwartzMap.fourierInv_lineDerivOp_eq, ← smulLeftCLM_ofReal ℂ this]

Premises used: SchwartzMap.fourierInv_lineDerivOp_eq, Complex, SchwartzMap.smulLeftCLM_ofReal
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
m : E
h :
  ∀ (u : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F) ((𝓕⁻ (∂_{m} f) : (a : 𝓢(E, ℂ)) → F) u : F)
      ((HSMul.hSMul (β := 𝓢'(E, F)) (-(2 * (↑π : ℂ) * Complex.I))
              ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕⁻ f) : 𝓢'(E, F)) :
            (a : 𝓢(E, ℂ)) → F)
          u :
        F)
⊢ 𝓕⁻ (∂_{m} f) =
    HSMul.hSMul (β := 𝓢'(E, F)) (-(2 * (↑π : ℂ) * Complex.I))
      ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕⁻ f) : 𝓢'(E, F))

Tactic:
ext u
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
m : E
u : 𝓢(E, ℂ)
this : Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ inner ℝ x m
⊢ Eq.{u_4 + 1} (α := F) ((𝓕⁻ (∂_{m} f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((HSMul.hSMul (β := 𝓢'(E, F)) (-(2 * (↑π : ℂ) * Complex.I))
            ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕⁻ f) : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)

Tactic:
simp [SchwartzMap.lineDerivOp_fourierInv_eq, ← smulLeftCLM_ofReal ℂ this]

Premises used: SchwartzMap.lineDerivOp_fourierInv_eq, Complex, SchwartzMap.smulLeftCLM_ofReal
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
f : 𝓢(E, ℂ)
⊢ Eq (α := ℂ) ((delta x : (a : 𝓢(E, ℂ)) → ℂ) f : ℂ) ((f : (a : E) → ℂ) x : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
x : E
⊢ Eq (α := 𝓢'(E, ℂ)) (toTemperedDistribution (dirac x)) (delta x)

Tactic:
aesop
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
h :
  ∀ (f : 𝓢(E, ℂ)),
    Eq (α := ℂ) ((𝓕 (E := 𝓢'(E, ℂ)) (delta 0) : (a : 𝓢(E, ℂ)) → ℂ) f : ℂ)
      ((toTemperedDistribution volume : (a : 𝓢(E, ℂ)) → ℂ) f : ℂ)
⊢ 𝓕 (E := 𝓢'(E, ℂ)) (delta 0) = toTemperedDistribution volume

Tactic:
ext f
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : 𝓢(E, ℂ)
⊢ Eq (α := ℂ) ((𝓕 (E := 𝓢'(E, ℂ)) (delta 0) : (a : 𝓢(E, ℂ)) → ℂ) f : ℂ)
    ((toTemperedDistribution volume : (a : 𝓢(E, ℂ)) → ℂ) f : ℂ)

Tactic:
simp [SchwartzMap.fourier_coe, Real.fourier_eq]

Premises used: Real.fourier_eq, SchwartzMap.fourier_coe
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E_1 : Type u_3
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace ℝ E_1
Ω_1 Ω₁ Ω₂ : Opens E_1
F_1 : Type u_4
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : NormedSpace 𝕜 F_1
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n_1 n₁ n₂ k : ℕ∞
B : Type u_6
E : Type u_7
inst_9 : NormedAddCommGroup E
inst_10 : NormedSpace ℝ E
Ω : Opens E
F : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace ℝ F
n : ℕ∞
inst_13 : TestFunctionClass B Ω F n
f : B
obtain :
  ∀ (C : ℝ) (hC : ∀ (x : E), ‖(f : (a : E) → F) x‖ ≤ C),
    ∃ (C : ℝ), ∀ (x y : E), dist ((f : (a : E) → F) x) ((f : (a : E) → F) y) ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : E), dist ((f : (a : E) → F) x) ((f : (a : E) → F) y) ≤ C

Tactic:
obtain ⟨C, hC⟩ := (map_continuous f).bounded_above_of_compact_support (map_hasCompactSupport f)

Premises used: TestFunctionClass.map_hasCompactSupport, Continuous.bounded_above_of_compact_support, ContinuousMapClass.map_continuous
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E_1 : Type u_3
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace ℝ E_1
Ω_1 Ω₁ Ω₂ : Opens E_1
F_1 : Type u_4
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : NormedSpace 𝕜 F_1
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n_1 n₁ n₂ k : ℕ∞
B : Type u_6
E : Type u_7
inst_9 : NormedAddCommGroup E
inst_10 : NormedSpace ℝ E
Ω : Opens E
F : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace ℝ F
n : ℕ∞
inst_13 : TestFunctionClass B Ω F n
f : B
C : ℝ
hC : ∀ (x : E), ‖(f : (a : E) → F) x‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : E), dist ((f : (a : E) → F) x) ((f : (a : E) → F) y) ≤ C

Tactic:
map_bounded (BoundedContinuousFunction.ofNormedAddCommGroup f (map_continuous f) C hC)

Premises used: BoundedContinuousMapClass.map_bounded, BoundedContinuousFunction.ofNormedAddCommGroup, ContinuousMapClass.map_continuous, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E_1 : Type u_3
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace ℝ E_1
Ω_1 Ω₁ Ω₂ : Opens E_1
F_1 : Type u_4
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : NormedSpace 𝕜 F_1
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n_1 n₁ n₂ k : ℕ∞
B : Type u_6
E : Type u_7
inst_9 : NormedAddCommGroup E
inst_10 : NormedSpace ℝ E
Ω : Opens E
F : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace ℝ F
n : ℕ∞
inst_13 : TestFunctionClass B Ω F n
f : B
C : ℝ
hC : ∀ (x : E), ‖(f : (a : E) → F) x‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : E), dist ((f : (a : E) → F) x) ((f : (a : E) → F) y) ≤ C

Tactic:
exact map_bounded (BoundedContinuousFunction.ofNormedAddCommGroup f (map_continuous f) C hC)

Premises used: BoundedContinuousMapClass.map_bounded, BoundedContinuousFunction.ofNormedAddCommGroup, ContinuousMapClass.map_continuous, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
f g : 𝓓^{n}(Ω, F)
h : Eq (α := (a : E) → F) ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun) f) ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun) g)
mk :
  ∀ (toFun : E → F) (contDiff' : ContDiff ℝ (↑n : ℕ∞ω) toFun) (hasCompactSupport' : HasCompactSupport toFun)
    (tsupport_subset' : tsupport toFun ⊆ (↑Ω : Set E))
    (h :
      Eq (α := (a : E) → F)
        ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun)
          { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
            tsupport_subset' := tsupport_subset' })
        ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun) g)),
    { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
        tsupport_subset' := tsupport_subset' : 𝓓^{n}(Ω, F) } =
      g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
g : 𝓓^{n}(Ω, F)
toFun : E → F
contDiff' : ContDiff ℝ (↑n : ℕ∞ω) toFun
hasCompactSupport' : HasCompactSupport toFun
tsupport_subset' : tsupport toFun ⊆ (↑Ω : Set E)
h :
  Eq (α := (a : E) → F)
    ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun)
      { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
        tsupport_subset' := tsupport_subset' })
    ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun) g)
mk :
  ∀ (toFun_1 : E → F) (contDiff'_1 : ContDiff ℝ (↑n : ℕ∞ω) toFun_1) (hasCompactSupport'_1 : HasCompactSupport toFun_1)
    (tsupport_subset'_1 : tsupport toFun_1 ⊆ (↑Ω : Set E))
    (h :
      Eq (α := (a : E) → F)
        ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun)
          { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
            tsupport_subset' := tsupport_subset' })
        ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun)
          { toFun := toFun_1, contDiff' := contDiff'_1, hasCompactSupport' := hasCompactSupport'_1,
            tsupport_subset' := tsupport_subset'_1 })),
    { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
        tsupport_subset' := tsupport_subset' : 𝓓^{n}(Ω, F) } =
      { toFun := toFun_1, contDiff' := contDiff'_1, hasCompactSupport' := hasCompactSupport'_1,
        tsupport_subset' := tsupport_subset'_1 }
⊢ { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
      tsupport_subset' := tsupport_subset' : 𝓓^{n}(Ω, F) } =
    g

Tactic:
cases g
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
toFun : E → F
contDiff' : ContDiff ℝ (↑n : ℕ∞ω) toFun
hasCompactSupport' : HasCompactSupport toFun
tsupport_subset' : tsupport toFun ⊆ (↑Ω : Set E)
toFun_1 : E → F
contDiff'_1 : ContDiff ℝ (↑n : ℕ∞ω) toFun_1
hasCompactSupport'_1 : HasCompactSupport toFun_1
tsupport_subset'_1 : tsupport toFun_1 ⊆ (↑Ω : Set E)
h :
  Eq (α := (a : E) → F)
    ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun)
      { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
        tsupport_subset' := tsupport_subset' })
    ((fun (f : 𝓓^{n}(Ω, F)) ↦ f.toFun)
      { toFun := toFun_1, contDiff' := contDiff'_1, hasCompactSupport' := hasCompactSupport'_1,
        tsupport_subset' := tsupport_subset'_1 })
⊢ { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
      tsupport_subset' := tsupport_subset' : 𝓓^{n}(Ω, F) } =
    { toFun := toFun_1, contDiff' := contDiff'_1, hasCompactSupport' := hasCompactSupport'_1,
      tsupport_subset' := tsupport_subset'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
f : 𝓓^{n}(Ω, F)
⊢ ContDiff ℝ (↑n : ℕ∞ω) (⇑f : (a : E) → F)

Tactic:
map_contDiff f

Premises used: TestFunctionClass.map_contDiff
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
f : 𝓓^{n}(Ω, F)
⊢ HasCompactSupport (⇑f : (a : E) → F)

Tactic:
map_hasCompactSupport f

Premises used: TestFunctionClass.map_hasCompactSupport
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
f : 𝓓^{n}(Ω, F)
⊢ tsupport (⇑f : (a : E) → F) ⊆ (↑Ω : Set E)

Tactic:
tsupport_map_subset f

Premises used: TestFunctionClass.tsupport_map_subset
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
f : 𝓓^{n}(Ω, F)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : E) → F)

Tactic:
f.contDiff.continuous

Premises used: TestFunction.contDiff, ContDiff.continuous
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
f : 𝓓^{n}(Ω, F)
⊢ f.toFun = (⇑f : (a : E) → F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
f g : 𝓓^{n}(Ω, F)
h : ∀ (a : E), (f : (a : E) → F) a = (g : (a : E) → F) a
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
f : 𝓓^{n}(Ω, F)
f' : E → F
h : f' = (⇑f : (a : E) → F)
⊢ (⇑(f.copy f' h) : (a : E) → F) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
f : 𝓓^{n}(Ω, F)
f' : E → F
h : f' = (⇑f : (a : E) → F)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
f : 𝓓^{n}(Ω, F)
⊢ (⇑{ toFun := (⇑f : (a : E) → F), continuous_toFun := ⋯, map_bounded' := ⋯ } : (a : E) → F) = (⇑f : (a : E) → F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
f : E → F
contDiff : ContDiff ℝ (↑n : ℕ∞ω) f
hasCompactSupport : HasCompactSupport f
tsupport_subset : tsupport f ⊆ (↑Ω : Set E)
⊢ (⇑{ toFun := f, contDiff' := contDiff, hasCompactSupport' := hasCompactSupport, tsupport_subset' := tsupport_subset :
          𝓓^{n}(Ω, F) } :
      (a : E) → F) =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
⊢ tsupport.{u_3, u_4} (α := F) 0 ⊆ (↑Ω : Set E)

Tactic:
simp only [tsupport_zero, empty_subset]

Premises used: Set.empty_subset, tsupport_zero
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
R : Type u_6
S : Type u_7
inst_9 : Semiring R
inst_10 : Semiring S
inst_11 : Module R F
inst_12 : Module S F
inst_13 : SMulCommClass ℝ R F
inst_14 : SMulCommClass ℝ S F
inst_15 : ContinuousConstSMul R F
inst_16 : ContinuousConstSMul S F
inst_17 : SMul R S
inst_18 : IsScalarTower R S F
x : R
x_1 : S
x_2 : 𝓓^{n}(Ω, F)
h : ∀ (a : E), ((x • x_1) • x_2 : (a : E) → F) a = (x • x_1 • x_2 : (a : E) → F) a
⊢ (x • x_1) • x_2 = x • x_1 • x_2

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
R : Type u_6
S : Type u_7
inst_9 : Semiring R
inst_10 : Semiring S
inst_11 : Module R F
inst_12 : Module S F
inst_13 : SMulCommClass ℝ R F
inst_14 : SMulCommClass ℝ S F
inst_15 : ContinuousConstSMul R F
inst_16 : ContinuousConstSMul S F
inst_17 : SMul R S
inst_18 : IsScalarTower R S F
x : R
x_1 : S
x_2 : 𝓓^{n}(Ω, F)
a : E
⊢ ((x • x_1) • x_2 : (a : E) → F) a = (x • x_1 • x_2 : (a : E) → F) a

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
V : Type u_6
inst_9 : AddCommGroup V
inst_10 : Module ℝ V
t : TopologicalSpace V
inst_11 : IsTopologicalAddGroup V
inst_12 : ContinuousSMul ℝ V
inst_13 : LocallyConvexSpace ℝ V
⊢ IsTopologicalAddGroup 𝓓^{n}(Ω, F)

Tactic:
topologicalAddGroup_sInf fun _ ⟨_, ht, _, _⟩ ↦ ht

Premises used: topologicalAddGroup_sInf, TestFunction, _private.0.TestFunction.instIsTopologicalAddGroup.match_1, IsTopologicalAddGroup
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
V : Type u_6
inst_9 : AddCommGroup V
inst_10 : Module ℝ V
t : TopologicalSpace V
inst_11 : IsTopologicalAddGroup V
inst_12 : ContinuousSMul ℝ V
inst_13 : LocallyConvexSpace ℝ V
⊢ IsUniformAddGroup 𝓓^{n}(Ω, F)

Tactic:
isUniformAddGroup_of_addCommGroup

Premises used: isUniformAddGroup_of_addCommGroup
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
V : Type u_6
inst_9 : AddCommGroup V
inst_10 : Module ℝ V
t : TopologicalSpace V
inst_11 : IsTopologicalAddGroup V
inst_12 : ContinuousSMul ℝ V
inst_13 : LocallyConvexSpace ℝ V
⊢ ContinuousSMul ℝ 𝓓^{n}(Ω, F)

Tactic:
continuousSMul_sInf fun _ ⟨_, _, ht, _⟩ ↦ ht

Premises used: Real, ContinuousSMul, continuousSMul_sInf, TestFunction, _private.0.TestFunction.instIsTopologicalAddGroup.match_1
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
𝕂 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace ℝ F'
inst_8 : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
V : Type u_6
inst_9 : AddCommGroup V
inst_10 : Module ℝ V
t : TopologicalSpace V
inst_11 : IsTopologicalAddGroup V
inst_12 : ContinuousSMul ℝ V
inst_13 : LocallyConvexSpace ℝ V
⊢ LocallyConvexSpace ℝ 𝓓^{n}(Ω, F)

Tactic:
.sInf fun _ ⟨_, _, _, ht⟩ ↦ ht

Premises used: Real, LocallyConvexSpace, LocallyConvexSpace.sInf, TestFunction, _private.0.TestFunction.instIsTopologicalAddGroup.match_1
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
⊢ LE.le (α := TopologicalSpace 𝓓^{n}(Ω, F)) (originalTop Ω F n) (topologicalSpace Ω F n)

Tactic:
le_sInf fun _t ⟨ht, _⟩ ↦ ht

Premises used: LE.le, _private.0.TestFunction.originalTop_le.match_1, TestFunction.originalTop, le_sInf
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
t : TopologicalSpace 𝓓^{n}(Ω, F)
inst_4 : IsTopologicalAddGroup 𝓓^{n}(Ω, F)
inst_5 : ContinuousSMul ℝ 𝓓^{n}(Ω, F)
inst_6 : LocallyConvexSpace ℝ 𝓓^{n}(Ω, F)
⊢ topologicalSpace Ω F n ≤ t ↔ originalTop Ω F n ≤ t

Tactic:
⟨le_trans originalTop_le, fun H ↦ sInf_le ⟨H, inferInstance, inferInstance, inferInstance⟩⟩

Premises used: inferInstance, sInf_le, And.intro, Iff.intro, TestFunction.originalTop_le, le_trans
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
rw :
  LE.le (α := TopologicalSpace 𝓓^{n}(Ω, F)) (coinduced (ofSupportedIn K_sub_Ω) ContDiffMapSupportedIn.topologicalSpace)
    (topologicalSpace Ω F n)
⊢ Continuous (X := 𝓓^{n}_{K}(E, F)) (ofSupportedIn K_sub_Ω)

Tactic:
rw [continuous_iff_coinduced_le]

Premises used: continuous_iff_coinduced_le
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
⊢ LE.le (α := TopologicalSpace 𝓓^{n}(Ω, F)) (coinduced (ofSupportedIn K_sub_Ω) ContDiffMapSupportedIn.topologicalSpace)
    (topologicalSpace Ω F n)

Tactic:
le_trans (le_iSup₂_of_le K K_sub_Ω le_rfl) originalTop_le

Premises used: le_iSup₂_of_le, TestFunction.originalTop_le, le_trans
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
⊢ LE.le (α := TopologicalSpace 𝓓^{n}(Ω, F)) (coinduced (ofSupportedIn K_sub_Ω) ContDiffMapSupportedIn.topologicalSpace)
    (topologicalSpace Ω F n)

Tactic:
exact le_trans (le_iSup₂_of_le K K_sub_Ω le_rfl) originalTop_le

Premises used: le_rfl, le_iSup₂_of_le, TestFunction.originalTop_le, le_trans