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
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
pos :
  ∀ (hk : k + 1 ≤ n),
    ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
      HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, E →L[ℝ] F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
        (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
neg :
  ∀ (hk : ¬k + 1 ≤ n), 0 = HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, E →L[ℝ] F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) 0
⊢ (if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0) =
    HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, E →L[ℝ] F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (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
c : 𝕜
f : 𝓓^{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
c : 𝕜
f : 𝓓^{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)
      (((HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, E →L[ℝ] F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
                  (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) :
                (a : E) → E →L[ℝ] F)
              a :
            (a : E) → F)
          x :
        F)
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, E →L[ℝ] F)) ((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)
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)
    (((HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, E →L[ℝ] F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
                (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x :
      F)

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

Premises used: ContDiffMapSupportedIn.contDiff, Differentiable.differentiableAt, LT.lt.ne', ContDiff.differentiable, fderiv_const_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
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hk : ¬k + 1 ≤ n
⊢ 0 = HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, E →L[ℝ] F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) 0

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

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 k : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
h : k + 1 ≤ n
⊢ (⇑(({ toFun := fun (f : 𝓓^{n}_{K}(E, F)) ↦ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯, map_add' := ⋯,
                map_smul' := ⋯ : 𝓓^{n}_{K}(E, F) →ₗ[𝕜] 𝓓^{k}_{K}(E, E →L[ℝ] F) } :
              (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F))
            f :
          𝓓^{k}_{K}(E, E →L[ℝ] F)) :
      (a : E) → E →L[ℝ] F) =
    fderiv ℝ (⇑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 k : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
h : ¬k + 1 ≤ n
⊢ (⇑(({ toFun := fun (f : 𝓓^{n}_{K}(E, F)) ↦ 0, map_add' := ⋯, map_smul' := ⋯ :
                𝓓^{n}_{K}(E, F) →ₗ[𝕜] 𝓓^{k}_{K}(E, E →L[ℝ] F) } :
              (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F))
            f :
          𝓓^{k}_{K}(E, E →L[ℝ] F)) :
      (a : E) → E →L[ℝ] F) =
    0

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 k : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
⊢ (⇑((fderivLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
      (a : E) → E →L[ℝ] F) =
    fderiv ℝ (⇑f : (a : E) → F)

Tactic:
simp [hk]
-- 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 : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
hk : n < k + 1
h :
  ∀ (a : E),
    (((fderivLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
          (a : E) → E →L[ℝ] F)
        a =
      (0 : (a : E) → E →L[ℝ] F) a
⊢ Eq (α := 𝓓^{k}_{K}(E, E →L[ℝ] F))
    ((fderivLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F))
    (0 : 𝓓^{k}_{K}(E, E →L[ℝ] F))

Tactic:
ext : 1
-- 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 : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
hk : n < k + 1
a : E
⊢ (((fderivLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f : 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
        (a : E) → E →L[ℝ] F)
      a =
    (0 : (a : E) → E →L[ℝ] F) a

Tactic:
simp [not_le_of_gt hk]

Premises used: not_le_of_gt
-- 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 : ℕ∞
K : Compacts E
𝕜' : Type u_5
inst_7 : NontriviallyNormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
⊢ Eq (α := (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F))
    (⇑(fderivLM 𝕜 n k) : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F))
    (⇑(fderivLM 𝕜' n k) : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] 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
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
pos :
  ∀ (hi : k + (↑i : ℕ∞) ≤ n),
    ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
      HAdd.hAdd (α := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
        (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
neg :
  ∀ (hi : ¬k + (↑i : ℕ∞) ≤ n),
    0 = HAdd.hAdd (α := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)) 0 0
⊢ (if hi : k + (↑i : ℕ∞) ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0) =
    HAdd.hAdd (α := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
      (if hi : k + (↑i : ℕ∞) ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0)
      (if hi : k + (↑i : ℕ∞) ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0)

Tactic:
split_ifs with hi
-- 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
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
hi : k + (↑i : ℕ∞) ≤ n
⊢ (↑i : ℕ∞ω) ≤ (↑n : ℕ∞ω)

Tactic:
have hi' : (i : ℕ∞ω) ≤ n := mod_cast (le_of_add_le_right hi)
-- 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
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
hi : k + (↑i : ℕ∞) ≤ n
hi' : (↑i : ℕ∞ω) ≤ (↑n : ℕ∞ω)
pos :
  ∀ (a : E) (x : (i : Fin i) → E),
    Eq.{u_3 + 1} (α := F)
      (((ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ : (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F)
              a :
            (a : (i : Fin i) → E) → F)
          x :
        F)
      (((HAdd.hAdd (α := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
                  (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) :
                (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F)
              a :
            (a : (i : Fin i) → E) → F)
          x :
        F)
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    HAdd.hAdd (α := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) 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
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
hi : k + (↑i : ℕ∞) ≤ n
hi' : (↑i : ℕ∞ω) ≤ (↑n : ℕ∞ω)
a : E
x : (i : Fin i) → E
⊢ Eq.{u_3 + 1} (α := F)
    (((ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ : (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) a :
          (a : (i : Fin i) → E) → F)
        x :
      F)
    (((HAdd.hAdd (α := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
                (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) :
              (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F)
            a :
          (a : (i : Fin i) → E) → F)
        x :
      F)

Tactic:
simp [iteratedFDeriv_add (f.contDiff.of_le hi') (g.contDiff.of_le hi')]

Premises used: ContDiffMapSupportedIn.contDiff, iteratedFDeriv_add, ContDiff.of_le
-- 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
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
hi : ¬k + (↑i : ℕ∞) ≤ n
⊢ 0 = HAdd.hAdd (α := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)) 0 0

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
i : ℕ
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
pos :
  ∀ (hi : k + (↑i : ℕ∞) ≤ n),
    ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
      HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
        ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
neg :
  ∀ (hi : ¬k + (↑i : ℕ∞) ≤ n),
    0 =
      HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
        ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) 0
⊢ (if hi : k + (↑i : ℕ∞) ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0) =
    HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
      ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (if hi : k + (↑i : ℕ∞) ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0)

Tactic:
split_ifs with hi
-- 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
i : ℕ
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hi : k + (↑i : ℕ∞) ≤ n
⊢ (↑i : ℕ∞ω) ≤ (↑n : ℕ∞ω)

Tactic:
have hi' : (i : ℕ∞ω) ≤ n := mod_cast (le_of_add_le_right hi)
-- 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
i : ℕ
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hi : k + (↑i : ℕ∞) ≤ n
hi' : (↑i : ℕ∞ω) ≤ (↑n : ℕ∞ω)
pos :
  ∀ (a : E) (x : (i : Fin i) → E),
    Eq.{u_3 + 1} (α := F)
      (((ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ : (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F)
              a :
            (a : (i : Fin i) → E) → F)
          x :
        F)
      (((HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
                  ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) :
                (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F)
              a :
            (a : (i : Fin i) → E) → F)
          x :
        F)
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
      ((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
i : ℕ
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hi : k + (↑i : ℕ∞) ≤ n
hi' : (↑i : ℕ∞ω) ≤ (↑n : ℕ∞ω)
a : E
x : (i : Fin i) → E
⊢ Eq.{u_3 + 1} (α := F)
    (((ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ : (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) a :
          (a : (i : Fin i) → E) → F)
        x :
      F)
    (((HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
                ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) :
              (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F)
            a :
          (a : (i : Fin i) → E) → F)
        x :
      F)

Tactic:
simp [iteratedFDeriv_const_smul_apply (f.contDiff.of_le hi').contDiffAt]

Premises used: ContDiffMapSupportedIn.contDiff, iteratedFDeriv_const_smul_apply, ContDiff.of_le, ContDiff.contDiffAt
-- 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
i : ℕ
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hi : ¬k + (↑i : ℕ∞) ≤ n
⊢ 0 =
    HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
      ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) 0

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 k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
pos :
  ∀ (h : k + (↑i : ℕ∞) ≤ n),
    (⇑(({ toFun := fun (f : 𝓓^{n}_{K}(E, F)) ↦ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯, map_add' := ⋯,
                  map_smul' := ⋯ :
                  𝓓^{n}_{K}(E, F) →ₗ[𝕜]
                    𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F) } :
                (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F))
              f :
            𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)) :
        (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) =
      iteratedFDeriv ℝ i (⇑f : (a : E) → F)
neg :
  ∀ (h : ¬k + (↑i : ℕ∞) ≤ n),
    (⇑(({ toFun := fun (f : 𝓓^{n}_{K}(E, F)) ↦ 0, map_add' := ⋯, map_smul' := ⋯ :
                  𝓓^{n}_{K}(E, F) →ₗ[𝕜]
                    𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F) } :
                (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F))
              f :
            𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)) :
        (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) =
      0
⊢ (⇑(({
                toFun := fun (f : 𝓓^{n}_{K}(E, F)) ↦
                  if hi : k + (↑i : ℕ∞) ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0,
                map_add' := ⋯, map_smul' := ⋯ :
                𝓓^{n}_{K}(E, F) →ₗ[𝕜]
                  𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F) } :
              (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F))
            f :
          𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)) :
      (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) =
    if k + (↑i : ℕ∞) ≤ n then iteratedFDeriv ℝ i (⇑f : (a : E) → F) else 0

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 k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
h : k + (↑i : ℕ∞) ≤ n
⊢ (⇑(({ toFun := fun (f : 𝓓^{n}_{K}(E, F)) ↦ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯, map_add' := ⋯,
                map_smul' := ⋯ :
                𝓓^{n}_{K}(E, F) →ₗ[𝕜]
                  𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F) } :
              (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F))
            f :
          𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)) :
      (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) =
    iteratedFDeriv ℝ i (⇑f : (a : E) → F)

Tactic:
rfl