awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
toFun : E → F
contDiff' : ContDiff ℝ (↑n : ℕ∞ω) toFun
zero_on_compl' : EqOn toFun 0 (↑K : Set E)ᶜ
toFun_1 : E → F
contDiff'_1 : ContDiff ℝ (↑n : ℕ∞ω) toFun_1
zero_on_compl'_1 : EqOn toFun_1 0 (↑K : Set E)ᶜ
h :
  Eq (α := (a : E) → F)
    ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun) { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' })
    ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun)
      { toFun := toFun_1, contDiff' := contDiff'_1, zero_on_compl' := zero_on_compl'_1 })
⊢ { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' : 𝓓^{n}_{K}(E, F) } =
    { toFun := toFun_1, contDiff' := contDiff'_1, zero_on_compl' := zero_on_compl'_1 }

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

Tactic:
map_contDiff f

Premises used: ContDiffMapSupportedInClass.map_contDiff
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ EqOn (⇑f : (a : E) → F) 0 (↑K : Set E)ᶜ

Tactic:
map_zero_on_compl f

Premises used: Set.Mem, setOf, ContDiffMapSupportedInClass.map_zero_on_compl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ HasCompactSupport (⇑f : (a : E) → F)

Tactic:
.intro K.isCompact (map_zero_on_compl f)

Premises used: HasCompactSupport.intro, TopologicalSpace.Compacts.isCompact, ContDiffMapSupportedInClass.map_zero_on_compl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ f.toFun = (⇑f : (a : E) → F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f g : 𝓓^{n}_{K}(E, 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.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, 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.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, 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.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, 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.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
rw : EqOn ((⇑f : (a : E) → F) + (⇑g : (a : E) → F)) (HAdd.hAdd (α := E → F) 0 0) (↑K : Set E)ᶜ
⊢ EqOn ((⇑f : (a : E) → F) + (⇑g : (a : E) → F)) 0 (↑K : Set E)ᶜ

Tactic:
rw [← add_zero 0]

Premises used: add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
⊢ EqOn ((⇑f : (a : E) → F) + (⇑g : (a : E) → F)) (HAdd.hAdd (α := E → F) 0 0) (↑K : Set E)ᶜ

Tactic:
f.zero_on_compl.comp_left₂ g.zero_on_compl

Premises used: ContDiffMapSupportedIn.zero_on_compl, Set.EqOn.comp_left₂
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
⊢ EqOn ((⇑f : (a : E) → F) + (⇑g : (a : E) → F)) (HAdd.hAdd (α := E → F) 0 0) (↑K : Set E)ᶜ

Tactic:
exact f.zero_on_compl.comp_left₂ g.zero_on_compl

Premises used: ContDiffMapSupportedIn.zero_on_compl, Set.EqOn.comp_left₂
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f : 𝓓^{n}_{K}(E, F)
rw : EqOn (-(⇑f : (a : E) → F)) (-0) (↑K : Set E)ᶜ
⊢ EqOn (-(⇑f : (a : E) → F)) 0 (↑K : Set E)ᶜ

Tactic:
rw [← neg_zero]

Premises used: neg_zero
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ EqOn (-(⇑f : (a : E) → F)) (-0) (↑K : Set E)ᶜ

Tactic:
f.zero_on_compl.comp_left

Premises used: ContDiffMapSupportedIn.zero_on_compl, Set.EqOn.comp_left
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ EqOn (-(⇑f : (a : E) → F)) (-0) (↑K : Set E)ᶜ

Tactic:
exact f.zero_on_compl.comp_left

Premises used: ContDiffMapSupportedIn.zero_on_compl, Set.EqOn.comp_left
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
rw : EqOn ((⇑f : (a : E) → F) - (⇑g : (a : E) → F)) (HSub.hSub (α := E → F) 0 0) (↑K : Set E)ᶜ
⊢ EqOn ((⇑f : (a : E) → F) - (⇑g : (a : E) → F)) 0 (↑K : Set E)ᶜ

Tactic:
rw [← sub_zero 0]

Premises used: sub_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
⊢ EqOn ((⇑f : (a : E) → F) - (⇑g : (a : E) → F)) (HSub.hSub (α := E → F) 0 0) (↑K : Set E)ᶜ

Tactic:
f.zero_on_compl.comp_left₂ g.zero_on_compl

Premises used: ContDiffMapSupportedIn.zero_on_compl, Set.EqOn.comp_left₂
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
⊢ EqOn ((⇑f : (a : E) → F) - (⇑g : (a : E) → F)) (HSub.hSub (α := E → F) 0 0) (↑K : Set E)ᶜ

Tactic:
exact f.zero_on_compl.comp_left₂ g.zero_on_compl

Premises used: ContDiffMapSupportedIn.zero_on_compl, Set.EqOn.comp_left₂
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
R : Type u_5
inst_11 : Semiring R
inst_12 : Module R F
inst_13 : SMulCommClass ℝ R F
inst_14 : ContinuousConstSMul R F
c : R
f : 𝓓^{n}_{K}(E, F)
rw : EqOn (c • (⇑f : (a : E) → F)) (HSMul.hSMul (β := E → F) c 0) (↑K : Set E)ᶜ
⊢ EqOn (c • (⇑f : (a : E) → F)) 0 (↑K : Set E)ᶜ

Tactic:
rw [← smul_zero c]

Premises used: smul_zero
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
R : Type u_5
inst_11 : Semiring R
inst_12 : Module R F
inst_13 : SMulCommClass ℝ R F
inst_14 : ContinuousConstSMul R F
c : R
f : 𝓓^{n}_{K}(E, F)
⊢ EqOn (c • (⇑f : (a : E) → F)) (HSMul.hSMul (β := E → F) c 0) (↑K : Set E)ᶜ

Tactic:
f.zero_on_compl.comp_left

Premises used: ContDiffMapSupportedIn.zero_on_compl, Set.EqOn.comp_left
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
R : Type u_5
inst_11 : Semiring R
inst_12 : Module R F
inst_13 : SMulCommClass ℝ R F
inst_14 : ContinuousConstSMul R F
c : R
f : 𝓓^{n}_{K}(E, F)
⊢ EqOn (c • (⇑f : (a : E) → F)) (HSMul.hSMul (β := E → F) c 0) (↑K : Set E)ᶜ

Tactic:
exact f.zero_on_compl.comp_left

Premises used: ContDiffMapSupportedIn.zero_on_compl, Set.EqOn.comp_left
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
⊢ Eq (α := (a : 𝓓^{n}_{K}(E, F)) → E → F) (⇑(coeHom E F n K) : (a : 𝓓^{n}_{K}(E, F)) → E → F)
    (DFunLike.coe (β := fun (a : E) ↦ F))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
rw : Injective (α := 𝓓^{n}_{K}(E, F)) (DFunLike.coe (β := fun (a : E) ↦ F))
⊢ Injective (α := 𝓓^{n}_{K}(E, F)) (β := E → F) (⇑(coeHom E F n K) : (a : 𝓓^{n}_{K}(E, F)) → E → F)

Tactic:
rw [coe_coeHom]

Premises used: ContDiffMapSupportedIn.coe_coeHom
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
⊢ Injective (α := 𝓓^{n}_{K}(E, F)) (DFunLike.coe (β := fun (a : E) ↦ F))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
⊢ Injective (α := 𝓓^{n}_{K}(E, F)) (DFunLike.coe (β := fun (a : E) ↦ F))

Tactic:
exact DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ support (⇑f : (a : E) → F) ⊆ (↑K : Set E)

Tactic:
support_subset_iff'.mpr f.zero_on_compl

Premises used: Iff.mpr, ContDiffMapSupportedIn.zero_on_compl, Function.support_subset_iff'
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ tsupport (⇑f : (a : E) → F) ⊆ (↑K : Set E)

Tactic:
closure_minimal f.support_subset K.isCompact.isClosed

Premises used: closure_minimal, tsupport, TopologicalSpace.Compacts.isCompact, ContDiffMapSupportedIn.support_subset, IsCompact.isClosed
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ HasCompactSupport (⇑f : (a : E) → F)

Tactic:
HasCompactSupport.intro K.isCompact f.zero_on_compl

Premises used: HasCompactSupport.intro, ContDiffMapSupportedIn.zero_on_compl, TopologicalSpace.Compacts.isCompact
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : E) → F)

Tactic:
f.contDiff.continuous

Premises used: ContDiffMapSupportedIn.contDiff, ContDiff.continuous
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
i : ℕ
hi : (↑i : ℕ∞) ≤ n
⊢ ∃ (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
          (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
        C

Tactic:
Continuous.bounded_above_of_compact_support
    (f.contDiff.continuous_iteratedFDeriv <| (WithTop.le_coe rfl).mpr hi)
    (f.hasCompactSupport.iteratedFDeriv i)

Premises used: Iff.mpr, ContDiffMapSupportedIn.contDiff, ContDiffMapSupportedIn.hasCompactSupport, HasCompactSupport.iteratedFDeriv, Continuous.bounded_above_of_compact_support, ContDiff.continuous_iteratedFDeriv, WithTop.le_coe, rfl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
i : ℕ
x : E
x₁ :
  ∀ (hx : x ∉ K),
    Eq (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
      (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) (0 x)
⊢ x ∈ (↑K : Set E)ᶜ →
    Eq (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
      (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) (0 x)

Tactic:
(hx : x ∉ K)
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
i : ℕ
x : E
hx : x ∉ K
contrapose! :
  ∀
    (hx :
      Ne (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) (0 x)),
    x ∈ K
⊢ Eq (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
    (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) (0 x)

Tactic:
contrapose! hx
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
i : ℕ
x : E
hx :
  Ne (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
    (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) (0 x)
⊢ x ∈ K

Tactic:
f.tsupport_subset (support_iteratedFDeriv_subset i hx)

Premises used: ContDiffMapSupportedIn.tsupport_subset, support_iteratedFDeriv_subset
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
i : ℕ
x : E
hx :
  Ne (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
    (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) (0 x)
⊢ x ∈ K

Tactic:
exact f.tsupport_subset (support_iteratedFDeriv_subset i hx)

Premises used: ContDiffMapSupportedIn.tsupport_subset, support_iteratedFDeriv_subset
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ Eq (α := E →ᵇ F) ((toBoundedContinuousFunctionLM 𝕜 : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ F) f : E →ᵇ F)
    ({ toFun := (⇑f : (a : E) → F), continuous_toFun := ⋯, map_bounded' := ⋯ } : E →ᵇ F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
𝕜' : Type u_5
inst_7 : NontriviallyNormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
⊢ Eq (α := (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ F) (⇑(toBoundedContinuousFunctionLM 𝕜) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ F)
    (⇑(toBoundedContinuousFunctionLM 𝕜') : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
x : E
hx : x ∈ (↑K : Set E)ᶜ
⊢ Eq.{u_4 + 1} (α := F') (((⇑T : (a : F) → F') ∘ (⇑f : (a : E) → F)) x) (0 x)

Tactic:
simp [f.zero_on_compl hx]

Premises used: ContDiffMapSupportedIn.zero_on_compl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
T : F →L[𝕜] F'
f g : 𝓓^{n}_{K}(E, F)
h :
  ∀ (x : E),
    ({ toFun := (⇑T : (a : F) → F') ∘ (⇑(f + g) : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ :
            𝓓^{n}_{K}(E, F') } :
          (a : E) → F')
        x =
      (HAdd.hAdd (α := 𝓓^{n}_{K}(E, F'))
            { toFun := (⇑T : (a : F) → F') ∘ (⇑f : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ :
              𝓓^{n}_{K}(E, F') }
            { toFun := (⇑T : (a : F) → F') ∘ (⇑g : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ :
              𝓓^{n}_{K}(E, F') } :
          (a : E) → F')
        x
⊢ { toFun := (⇑T : (a : F) → F') ∘ (⇑(f + g) : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ } =
    HAdd.hAdd (α := 𝓓^{n}_{K}(E, F'))
      { toFun := (⇑T : (a : F) → F') ∘ (⇑f : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ : 𝓓^{n}_{K}(E, F') }
      { toFun := (⇑T : (a : F) → F') ∘ (⇑g : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ : 𝓓^{n}_{K}(E, F') }

Tactic:
ext x
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
T : F →L[𝕜] F'
f g : 𝓓^{n}_{K}(E, F)
x : E
⊢ ({ toFun := (⇑T : (a : F) → F') ∘ (⇑(f + g) : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ : 𝓓^{n}_{K}(E, F') } :
        (a : E) → F')
      x =
    (HAdd.hAdd (α := 𝓓^{n}_{K}(E, F'))
          { toFun := (⇑T : (a : F) → F') ∘ (⇑f : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ : 𝓓^{n}_{K}(E, F') }
          { toFun := (⇑T : (a : F) → F') ∘ (⇑g : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ :
            𝓓^{n}_{K}(E, F') } :
        (a : E) → F')
      x

Tactic:
map_add T (f x) (g x)

Premises used: map_add, DFunLike.coe