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
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:
exact map_add T (f x) (g x)

Premises used: map_add, DFunLike.coe
-- 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'
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
h :
  ∀ (x : E),
    ({ toFun := (⇑T : (a : F) → F') ∘ (⇑(c • f) : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ :
            𝓓^{n}_{K}(E, F') } :
          (a : E) → F')
        x =
      (HSMul.hSMul (α := 𝕜) (β := 𝓓^{n}_{K}(E, F')) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
            { toFun := (⇑T : (a : F) → F') ∘ (⇑f : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ :
              𝓓^{n}_{K}(E, F') } :
          (a : E) → F')
        x
⊢ { toFun := (⇑T : (a : F) → F') ∘ (⇑(c • f) : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ } =
    HSMul.hSMul (α := 𝕜) (β := 𝓓^{n}_{K}(E, F')) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      { toFun := (⇑T : (a : F) → F') ∘ (⇑f : (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'
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
x : E
⊢ ({ toFun := (⇑T : (a : F) → F') ∘ (⇑(c • f) : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ : 𝓓^{n}_{K}(E, F') } :
        (a : E) → F')
      x =
    (HSMul.hSMul (α := 𝕜) (β := 𝓓^{n}_{K}(E, F')) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
          { toFun := (⇑T : (a : F) → F') ∘ (⇑f : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ :
            𝓓^{n}_{K}(E, F') } :
        (a : E) → F')
      x

Tactic:
map_smul T c (f x)

Premises used: DFunLike.coe, map_smul
-- 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'
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
x : E
⊢ ({ toFun := (⇑T : (a : F) → F') ∘ (⇑(c • f) : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ : 𝓓^{n}_{K}(E, F') } :
        (a : E) → F')
      x =
    (HSMul.hSMul (α := 𝕜) (β := 𝓓^{n}_{K}(E, F')) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
          { toFun := (⇑T : (a : F) → F') ∘ (⇑f : (a : E) → F), contDiff' := ⋯, zero_on_compl' := ⋯ :
            𝓓^{n}_{K}(E, F') } :
        (a : E) → F')
      x

Tactic:
exact map_smul T c (f x)

Premises used: DFunLike.coe, map_smul
-- 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 : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
⊢ (⇑((postcompLM T : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}_{K}(E, F')) f : 𝓓^{n}_{K}(E, F')) : (a : E) → F') =
    (⇑T : (a : F) → 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)
pos :
  ∀ (h : n₂ ≤ n₁ ∧ K₁ ≤ K₂),
    ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
      ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ + ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
neg : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂) → 0 = HAdd.hAdd (α := 𝓓^{n₂}_{K₂}(E, F)) 0 0
⊢ (if h : n₂ ≤ n₁ ∧ K₁ ≤ K₂ then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0) =
    HAdd.hAdd (α := 𝓓^{n₂}_{K₂}(E, F))
      (if h : n₂ ≤ n₁ ∧ K₁ ≤ K₂ then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0)
      (if h : n₂ ≤ n₁ ∧ K₁ ≤ K₂ then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0)

Tactic:
split_ifs
-- 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)
h : n₂ ≤ n₁ ∧ K₁ ≤ K₂
pos :
  ∀ (a : E),
    (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ : (a : E) → F) a =
      (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ + ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ : (a : E) → F) a
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ + ContDiffMapSupportedIn.of_support_subset ⋯ ⋯

Tactic:
ext
-- 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)
h : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
neg : ∀ (a : E), (0 : (a : E) → F) a = (HAdd.hAdd (α := 𝓓^{n₂}_{K₂}(E, F)) 0 0 : (a : E) → F) a
⊢ 0 = HAdd.hAdd (α := 𝓓^{n₂}_{K₂}(E, F)) 0 0

Tactic:
ext
-- 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)
h : n₂ ≤ n₁ ∧ K₁ ≤ K₂
a : E
⊢ (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ : (a : E) → F) a =
    (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ + ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ : (a : E) → F) a

Tactic:
simp
-- 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)
h : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
a : E
⊢ (0 : (a : E) → F) a = (HAdd.hAdd (α := 𝓓^{n₂}_{K₂}(E, F)) 0 0 : (a : E) → F) a

Tactic:
simp
-- 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
c : 𝕜
f : 𝓓^{n₁}_{K₁}(E, F)
pos :
  ∀ (h : n₂ ≤ n₁ ∧ K₁ ≤ K₂),
    ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
      HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
neg : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂) → 0 = HSMul.hSMul (α := 𝕜) (β := 𝓓^{n₂}_{K₂}(E, F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) 0
⊢ (if h : n₂ ≤ n₁ ∧ K₁ ≤ K₂ then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0) =
    HSMul.hSMul (α := 𝕜) (β := 𝓓^{n₂}_{K₂}(E, F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (if h : n₂ ≤ n₁ ∧ K₁ ≤ K₂ then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0)

Tactic:
split_ifs
-- 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
c : 𝕜
f : 𝓓^{n₁}_{K₁}(E, F)
h : n₂ ≤ n₁ ∧ K₁ ≤ K₂
pos :
  ∀ (a : E),
    (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ : (a : E) → F) a =
      (HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) :
          (a : E) → F)
        a
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)

Tactic:
ext
-- 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
c : 𝕜
f : 𝓓^{n₁}_{K₁}(E, F)
h : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
neg :
  ∀ (a : E),
    (0 : (a : E) → F) a =
      (HSMul.hSMul (α := 𝕜) (β := 𝓓^{n₂}_{K₂}(E, F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) 0 : (a : E) → F) a
⊢ 0 = HSMul.hSMul (α := 𝕜) (β := 𝓓^{n₂}_{K₂}(E, F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) 0

Tactic:
ext
-- 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
c : 𝕜
f : 𝓓^{n₁}_{K₁}(E, F)
h : n₂ ≤ n₁ ∧ K₁ ≤ K₂
a : E
⊢ (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ : (a : E) → F) a =
    (HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) :
        (a : E) → F)
      a

Tactic:
simp
-- 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
c : 𝕜
f : 𝓓^{n₁}_{K₁}(E, F)
h : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
a : E
⊢ (0 : (a : E) → F) a =
    (HSMul.hSMul (α := 𝕜) (β := 𝓓^{n₂}_{K₂}(E, F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) 0 : (a : E) → F) a

Tactic:
simp
-- 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
f : 𝓓^{n₁}_{K₁}(E, F)
rw :
  (⇑(({
                toFun := fun (f : 𝓓^{n₁}_{K₁}(E, F)) ↦
                  if h : n₂ ≤ n₁ ∧ K₁ ≤ K₂ then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0,
                map_add' := ⋯, map_smul' := ⋯ : 𝓓^{n₁}_{K₁}(E, F) →ₗ[𝕜] 𝓓^{n₂}_{K₂}(E, F) } :
              (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F))
            f :
          𝓓^{n₂}_{K₂}(E, F)) :
      (a : E) → F) =
    (⇑(if n₂ ≤ n₁ ∧ K₁ ≤ K₂ then f else 0) : (a : E) → F)
⊢ (⇑((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) f : 𝓓^{n₂}_{K₂}(E, F)) : (a : E) → F) =
    (⇑(if n₂ ≤ n₁ ∧ K₁ ≤ K₂ then f else 0) : (a : E) → F)

Tactic:
rw [monoLM]

Premises used: ContDiffMapSupportedIn.monoLM
-- 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
f : 𝓓^{n₁}_{K₁}(E, F)
pos :
  ∀ (h : n₂ ≤ n₁ ∧ K₁ ≤ K₂),
    (⇑(({ toFun := fun (f : 𝓓^{n₁}_{K₁}(E, F)) ↦ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯, map_add' := ⋯,
                  map_smul' := ⋯ : 𝓓^{n₁}_{K₁}(E, F) →ₗ[𝕜] 𝓓^{n₂}_{K₂}(E, F) } :
                (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F))
              f :
            𝓓^{n₂}_{K₂}(E, F)) :
        (a : E) → F) =
      (⇑f : (a : E) → F)
neg :
  ∀ (h : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)),
    (⇑(({ toFun := fun (f : 𝓓^{n₁}_{K₁}(E, F)) ↦ 0, map_add' := ⋯, map_smul' := ⋯ :
                  𝓓^{n₁}_{K₁}(E, F) →ₗ[𝕜] 𝓓^{n₂}_{K₂}(E, F) } :
                (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F))
              f :
            𝓓^{n₂}_{K₂}(E, F)) :
        (a : E) → F) =
      (⇑0 : (a : E) → F)
⊢ (⇑(({
                toFun := fun (f : 𝓓^{n₁}_{K₁}(E, F)) ↦
                  if h : n₂ ≤ n₁ ∧ K₁ ≤ K₂ then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0,
                map_add' := ⋯, map_smul' := ⋯ : 𝓓^{n₁}_{K₁}(E, F) →ₗ[𝕜] 𝓓^{n₂}_{K₂}(E, F) } :
              (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F))
            f :
          𝓓^{n₂}_{K₂}(E, F)) :
      (a : E) → F) =
    (⇑(if n₂ ≤ n₁ ∧ K₁ ≤ K₂ then f else 0) : (a : E) → F)

Tactic:
split_ifs
-- 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
f : 𝓓^{n₁}_{K₁}(E, F)
h : n₂ ≤ n₁ ∧ K₁ ≤ K₂
⊢ (⇑(({ toFun := fun (f : 𝓓^{n₁}_{K₁}(E, F)) ↦ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯, map_add' := ⋯,
                map_smul' := ⋯ : 𝓓^{n₁}_{K₁}(E, F) →ₗ[𝕜] 𝓓^{n₂}_{K₂}(E, F) } :
              (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F))
            f :
          𝓓^{n₂}_{K₂}(E, F)) :
      (a : E) → F) =
    (⇑f : (a : E) → F)

Tactic:
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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
f : 𝓓^{n₁}_{K₁}(E, F)
h : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
⊢ (⇑(({ toFun := fun (f : 𝓓^{n₁}_{K₁}(E, F)) ↦ 0, map_add' := ⋯, map_smul' := ⋯ :
                𝓓^{n₁}_{K₁}(E, F) →ₗ[𝕜] 𝓓^{n₂}_{K₂}(E, F) } :
              (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F))
            f :
          𝓓^{n₂}_{K₂}(E, F)) :
      (a : E) → F) =
    (⇑0 : (a : E) → F)

Tactic:
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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
H : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
h :
  ∀ (x : 𝓓^{n₁}_{K₁}(E, F)) (a : E),
    (((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) x : 𝓓^{n₂}_{K₂}(E, F)) : (a : E) → F) a =
      (((0 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) x : 𝓓^{n₂}_{K₂}(E, F)) : (a : E) → F) a
⊢ Eq (α := 𝓓^{n₁}_{K₁}(E, F) →ₗ[𝕜] 𝓓^{n₂}_{K₂}(E, F)) (monoLM 𝕜) 0

Tactic:
ext
-- 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
H : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
x : 𝓓^{n₁}_{K₁}(E, F)
a : E
⊢ (((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) x : 𝓓^{n₂}_{K₂}(E, F)) : (a : E) → F) a =
    (((0 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) x : 𝓓^{n₂}_{K₂}(E, F)) : (a : E) → F) a

Tactic:
simp [H]
-- 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
𝕜' : Type u_5
inst_7 : NontriviallyNormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
⊢ Eq (α := (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) (⇑(monoLM 𝕜) : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F))
    (⇑(monoLM 𝕜') : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(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)
pos :
  ∀ (hk : k + 1 ≤ n),
    ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
      HAdd.hAdd (α := 𝓓^{k}_{K}(E, E →L[ℝ] F)) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
        (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
neg : ∀ (hk : ¬k + 1 ≤ n), 0 = HAdd.hAdd (α := 𝓓^{k}_{K}(E, E →L[ℝ] F)) 0 0
⊢ (if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0) =
    HAdd.hAdd (α := 𝓓^{k}_{K}(E, E →L[ℝ] F))
      (if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0)
      (if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0)

Tactic:
split_ifs with hk
-- 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)
hk : k + 1 ≤ n
⊢ 0 < (↑n : ℕ∞ω)

Tactic:
have hk' : 0 < (n : ℕ∞ω) := mod_cast (ENat.add_one_pos.trans_le hk)
-- 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)
hk : k + 1 ≤ n
hk' : 0 < (↑n : ℕ∞ω)
pos :
  ∀ (a x : E),
    Eq.{u_3 + 1} (α := F) (((ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ : (a : E) → E →L[ℝ] F) a : (a : E) → F) x : F)
      (((HAdd.hAdd (α := 𝓓^{k}_{K}(E, E →L[ℝ] F)) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
                  (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) :
                (a : E) → E →L[ℝ] F)
              a :
            (a : E) → F)
          x :
        F)
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    HAdd.hAdd (α := 𝓓^{k}_{K}(E, E →L[ℝ] F)) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
      (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)

Tactic:
ext
-- 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)
hk : k + 1 ≤ n
hk' : 0 < (↑n : ℕ∞ω)
a x : E
⊢ Eq.{u_3 + 1} (α := F) (((ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ : (a : E) → E →L[ℝ] F) a : (a : E) → F) x : F)
    (((HAdd.hAdd (α := 𝓓^{k}_{K}(E, E →L[ℝ] F)) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
                (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x :
      F)

Tactic:
simp [fderiv_add (f.contDiff.differentiable hk'.ne').differentiableAt
                       (g.contDiff.differentiable hk'.ne').differentiableAt]

Premises used: ContDiffMapSupportedIn.contDiff, Differentiable.differentiableAt, LT.lt.ne', fderiv_add, ContDiff.differentiable
-- 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)
hk : ¬k + 1 ≤ n
⊢ 0 = HAdd.hAdd (α := 𝓓^{k}_{K}(E, E →L[ℝ] F)) 0 0

Tactic:
simp