awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 k : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ (⇑(({ 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
have pos : ∀ (h : k + 1 ≤ n),
  (⇑(({ toFun := fun (f : 𝓓^{n}_{K}(E, F)) ↦ ContDiffMapSupportedIn.of_support_subset sorry sorry, map_add' := sorry,
                map_smul' := sorry : 𝓓^{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: 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 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)
⊢ (⇑(({ 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
have neg : ∀ (h : ¬k + 1 ≤ n),
  (⇑(({ toFun := fun (f : 𝓓^{n}_{K}(E, F)) ↦ 0, map_add' := sorry, map_smul' := sorry :
                𝓓^{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: 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 k : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
hk : n < k + 1
⊢ 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))
have 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
Tactic: ext : 1
-- 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
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
⊢ (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)
have pos : ∀ (hi : k + (↑i : ℕ∞) ≤ n),
  ContDiffMapSupportedIn.of_support_subset sorry sorry =
    HAdd.hAdd (α := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
      (ContDiffMapSupportedIn.of_support_subset sorry sorry) (ContDiffMapSupportedIn.of_support_subset sorry sorry)
Tactic: split_ifs with hi
-- 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
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 ⋯ ⋯)
⊢ (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)
have 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
Tactic: split_ifs with hi
-- 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
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
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 ⋯ ⋯)
have hi' : (↑i : ℕ∞ω) ≤ (↑n : ℕ∞ω)
Tactic: have hi' : (i : ℕ∞ω) ≤ n := mod_cast (le_of_add_le_right hi)
-- 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
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
hi : k + (↑i : ℕ∞) ≤ n
hi' : (↑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 ⋯ ⋯)
have pos : ∀ (a : E) (x : (i : Fin i) → E),
  Eq.{u_3 + 1} (α := F)
    (((ContDiffMapSupportedIn.of_support_subset sorry sorry : (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 sorry sorry) (ContDiffMapSupportedIn.of_support_subset sorry sorry) :
              (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F)
            a :
          (a : (i : Fin i) → 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
i : ℕ
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
⊢ (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)
have pos : ∀ (hi : k + (↑i : ℕ∞) ≤ n),
  ContDiffMapSupportedIn.of_support_subset sorry sorry =
    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 sorry sorry)
Tactic: split_ifs with hi
-- 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
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 ⋯ ⋯)
⊢ (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)
have 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
Tactic: split_ifs with hi
-- 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
i : ℕ
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
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 ⋯ ⋯)
have hi' : (↑i : ℕ∞ω) ≤ (↑n : ℕ∞ω)
Tactic: have hi' : (i : ℕ∞ω) ≤ n := mod_cast (le_of_add_le_right hi)
-- 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
i : ℕ
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hi : k + (↑i : ℕ∞) ≤ n
hi' : (↑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 ⋯ ⋯)
have pos : ∀ (a : E) (x : (i : Fin i) → E),
  Eq.{u_3 + 1} (α := F)
    (((ContDiffMapSupportedIn.of_support_subset sorry sorry : (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 sorry sorry) :
              (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F)
            a :
          (a : (i : Fin i) → 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
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)
⊢ (⇑(({
                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
have pos : ∀ (h : k + (↑i : ℕ∞) ≤ n),
  (⇑(({ toFun := fun (f : 𝓓^{n}_{K}(E, F)) ↦ ContDiffMapSupportedIn.of_support_subset sorry sorry, map_add' := sorry,
                map_smul' := sorry :
                𝓓^{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: 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 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)
⊢ (⇑(({
                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
have neg : ∀ (h : ¬k + (↑i : ℕ∞) ≤ n),
  (⇑(({ toFun := fun (f : 𝓓^{n}_{K}(E, F)) ↦ 0, map_add' := sorry, map_smul' := sorry :
                𝓓^{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
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 k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
hin : n < k + (↑i : ℕ∞)
⊢ Eq (α := 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
    ((iteratedFDerivLM 𝕜 n k i :
          (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))
    (0 : 𝓓^{k}_{K}(E, ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
have h : ∀ (a : E),
  (((iteratedFDerivLM 𝕜 n k i :
              (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)
      a =
    (0 : (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) a
Tactic: ext : 1
-- 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 : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
x : E
⊢ Eq (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ E) F)
    ((((structureMapLM 𝕜 n 0 : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin 0) ↦ E) F) f :
            E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ E) F) :
          (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin 0) ↦ E) F)
        x :
      ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ E) F)
    (ContinuousMultilinearMap.uncurry0 ℝ E ((f : (a : E) → F) x) :
      ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ E) F)
have H : ∀ (x_1 : (i : Fin 0) → E),
  Eq.{u_3 + 1} (α := F)
    ((((((structureMapLM 𝕜 n 0 : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin 0) ↦ E) F) f :
                  E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ E) F) :
                (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin 0) ↦ E) F)
              x :
            ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ E) F) :
          (a : (i : Fin 0) → E) → F)
        x_1 :
      F)
    ((ContinuousMultilinearMap.uncurry0 ℝ E ((f : (a : E) → F) x) : (a : (i : Fin 0) → E) → F) x_1 : 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
⊢ IsUniformAddGroup 𝓓^{n}_{K}(E, F)
have rw : IsUniformAddGroup 𝓓^{n}_{K}(E, F)
Tactic: rw [ContDiffMapSupportedIn.uniformSpace_eq_iInf]
-- 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 : ℕ∞
K : Compacts E
⊢ IsUniformInducing (α := 𝓓^{n}_{K}(E, F)) (β :=
    (i : ℕ) → E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
    (⇑(ContinuousLinearMap.pi (φ := fun (i : ℕ) ↦
          E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F) (structureMapCLM 𝕜 n)) :
      (a : 𝓓^{n}_{K}(E, F)) → (i : ℕ) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F)
have simp_rw : Eq (α := UniformSpace 𝓓^{n}_{K}(E, F))
  (⨅ (i : ℕ),
    comap (β := E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
      (comp (β := (i : ℕ) → E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
          (eval (β := fun (i : ℕ) ↦ E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F) i)
          (⇑(ContinuousLinearMap.pi (φ := fun (i : ℕ) ↦
                E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F) (structureMapCLM 𝕜 n)) :
            (a : 𝓓^{n}_{K}(E, F)) → (i : ℕ) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) :
        𝓓^{n}_{K}(E, F) → E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
      (PseudoMetricSpace.toUniformSpace :
        UniformSpace (E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)))
  (⨅ (i : ℕ),
    comap (β := E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
      (⇑(structureMapLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F)
      inferInstance)
Tactic: simp_rw [isUniformInducing_iff_uniformSpace, ContDiffMapSupportedIn.uniformSpace_eq_iInf,
      Pi.uniformSpace_eq, comap_iInf, ← comap_comap]
-- 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
X : Type u_5
inst_4 : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
⊢ Continuous[inst_4, _] φ ↔
    ∀ (i : ℕ),
      (↑i : ℕ∞) ≤ n →
        Continuous[inst_4, _]
          ((⇑(structureMapCLM ℝ n i) :
              (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
            φ)
have rw : (∀ (i : ℕ),
    Continuous[inst_4, _]
      ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
        φ)) ↔
  ∀ (i : ℕ),
    (↑i : ℕ∞) ≤ n →
      Continuous[inst_4, _]
        ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
          φ)
Tactic: rw [continuous_iff_comp]