awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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
⊢ Eq (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
    (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) (0 x)
have 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
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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)
⊢ { 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') }
have h : ∀ (x : E),
  ({ toFun := (⇑T : (a : F) → F') ∘ (⇑(f + g) : (a : E) → F), contDiff' := sorry, zero_on_compl' := sorry : 𝓓^{n}_{K}(E, F') } :
        (a : E) → F')
      x =
    (HAdd.hAdd (α := 𝓓^{n}_{K}(E, F'))
          { toFun := (⇑T : (a : F) → F') ∘ (⇑f : (a : E) → F), contDiff' := sorry, zero_on_compl' := sorry : 𝓓^{n}_{K}(E, F') }
          { toFun := (⇑T : (a : F) → F') ∘ (⇑g : (a : E) → F), contDiff' := sorry, zero_on_compl' := sorry :
            𝓓^{n}_{K}(E, F') } :
        (a : E) → F')
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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)
⊢ { 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') }
have h : ∀ (x : E),
  ({ toFun := (⇑T : (a : F) → F') ∘ (⇑(c • f) : (a : E) → F), contDiff' := sorry, zero_on_compl' := sorry : 𝓓^{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' := sorry, zero_on_compl' := sorry :
            𝓓^{n}_{K}(E, F') } :
        (a : E) → F')
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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)
⊢ (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)
have pos : ∀ (h : n₂ ≤ n₁ ∧ K₁ ≤ K₂),
  ContDiffMapSupportedIn.of_support_subset sorry sorry =
    ContDiffMapSupportedIn.of_support_subset sorry sorry + ContDiffMapSupportedIn.of_support_subset sorry sorry
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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 ⋯ ⋯
⊢ (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)
have neg : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂) → 0 = HAdd.hAdd (α := 𝓓^{n₂}_{K₂}(E, F)) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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₂
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ + ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
have pos : ∀ (a : E),
  (ContDiffMapSupportedIn.of_support_subset sorry sorry : (a : E) → F) a =
    (ContDiffMapSupportedIn.of_support_subset sorry sorry + ContDiffMapSupportedIn.of_support_subset sorry sorry : (a : E) → F) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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₂)
⊢ 0 = HAdd.hAdd (α := 𝓓^{n₂}_{K₂}(E, F)) 0 0
have neg : ∀ (a : E), (0 : (a : E) → F) a = (HAdd.hAdd (α := 𝓓^{n₂}_{K₂}(E, F)) 0 0 : (a : E) → F) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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)
⊢ (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)
have pos : ∀ (h : n₂ ≤ n₁ ∧ K₁ ≤ K₂),
  ContDiffMapSupportedIn.of_support_subset sorry sorry =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (ContDiffMapSupportedIn.of_support_subset sorry sorry)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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 ⋯ ⋯)
⊢ (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)
have neg : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂) → 0 = HSMul.hSMul (α := 𝕜) (β := 𝓓^{n₂}_{K₂}(E, F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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₂
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
have pos : ∀ (a : E),
  (ContDiffMapSupportedIn.of_support_subset sorry sorry : (a : E) → F) a =
    (HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (ContDiffMapSupportedIn.of_support_subset sorry sorry) :
        (a : E) → F)
      a
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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₂)
⊢ 0 = HSMul.hSMul (α := 𝕜) (β := 𝓓^{n₂}_{K₂}(E, F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) 0
have neg : ∀ (a : E),
  (0 : (a : E) → F) a =
    (HSMul.hSMul (α := 𝕜) (β := 𝓓^{n₂}_{K₂}(E, F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) 0 : (a : E) → F) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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)
⊢ (⇑((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)
have rw : (⇑(({
              toFun := fun (f : 𝓓^{n₁}_{K₁}(E, F)) ↦
                if h : n₂ ≤ n₁ ∧ K₁ ≤ K₂ then ContDiffMapSupportedIn.of_support_subset sorry sorry else 0,
              map_add' := sorry, map_smul' := sorry : 𝓓^{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: rw [monoLM]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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)
⊢ (⇑(({
                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)
have pos : ∀ (h : n₂ ≤ n₁ ∧ K₁ ≤ K₂),
  (⇑(({ toFun := fun (f : 𝓓^{n₁}_{K₁}(E, F)) ↦ ContDiffMapSupportedIn.of_support_subset sorry sorry, map_add' := sorry,
                map_smul' := sorry : 𝓓^{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: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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)
⊢ (⇑(({
                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)
have neg : ∀ (h : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)),
  (⇑(({ toFun := fun (f : 𝓓^{n₁}_{K₁}(E, F)) ↦ 0, map_add' := sorry, map_smul' := sorry :
                𝓓^{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: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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₂)
⊢ Eq (α := 𝓓^{n₁}_{K₁}(E, F) →ₗ[𝕜] 𝓓^{n₂}_{K₂}(E, F)) (monoLM 𝕜) 0
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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)
⊢ (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)
have pos : ∀ (hk : k + 1 ≤ n),
  ContDiffMapSupportedIn.of_support_subset sorry sorry =
    HAdd.hAdd (α := 𝓓^{k}_{K}(E, E →L[ℝ] F)) (ContDiffMapSupportedIn.of_support_subset sorry sorry)
      (ContDiffMapSupportedIn.of_support_subset sorry sorry)
Tactic: split_ifs with hk
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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 ⋯ ⋯)
⊢ (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)
have neg : ∀ (hk : ¬k + 1 ≤ n), 0 = HAdd.hAdd (α := 𝓓^{k}_{K}(E, E →L[ℝ] F)) 0 0
Tactic: split_ifs with hk
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (hypothesis)
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
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    HAdd.hAdd (α := 𝓓^{k}_{K}(E, E →L[ℝ] F)) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
      (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
have hk' : 0 < (↑n : ℕ∞ω)
Tactic: have hk' : 0 < (n : ℕ∞ω) := mod_cast (ENat.add_one_pos.trans_le hk)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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 : ℕ∞ω)
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    HAdd.hAdd (α := 𝓓^{k}_{K}(E, E →L[ℝ] F)) (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
      (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
have pos : ∀ (a x : E),
  Eq.{u_3 + 1} (α := F) (((ContDiffMapSupportedIn.of_support_subset sorry sorry : (a : E) → E →L[ℝ] F) a : (a : E) → F) x : F)
    (((HAdd.hAdd (α := 𝓓^{k}_{K}(E, E →L[ℝ] F)) (ContDiffMapSupportedIn.of_support_subset sorry sorry)
                (ContDiffMapSupportedIn.of_support_subset sorry sorry) :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x :
      F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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)
⊢ (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)
have pos : ∀ (hk : k + 1 ≤ n),
  ContDiffMapSupportedIn.of_support_subset sorry sorry =
    HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, E →L[ℝ] F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (ContDiffMapSupportedIn.of_support_subset sorry sorry)
Tactic: split_ifs with hk
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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 ⋯ ⋯)
⊢ (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)
have neg : ∀ (hk : ¬k + 1 ≤ n), 0 = HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, E →L[ℝ] F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) 0
Tactic: split_ifs with hk
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (hypothesis)
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
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, E →L[ℝ] F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
have hk' : 0 < (↑n : ℕ∞ω)
Tactic: have hk' : 0 < (n : ℕ∞ω) := mod_cast (ENat.add_one_pos.trans_le hk)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
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 : ℕ∞ω)
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    HSMul.hSMul (α := 𝕜) (β := 𝓓^{k}_{K}(E, E →L[ℝ] F)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯)
have pos : ∀ (a x : E),
  Eq.{u_3 + 1} (α := F) (((ContDiffMapSupportedIn.of_support_subset sorry sorry : (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 sorry sorry) :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x :
      F)
Tactic: ext