awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)) ↦ 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

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
i : ℕ
f : 𝓓^{n}_{K}(E, F)
hin : k + (↑i : ℕ∞) ≤ n
⊢ (⇑((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) =
    iteratedFDeriv ℝ i (⇑f : (a : E) → F)

Tactic:
simp [hin]
-- 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)
hin : n < k + (↑i : ℕ∞)
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
⊢ 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))

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
i : ℕ
f : 𝓓^{n}_{K}(E, F)
hin : n < k + (↑i : ℕ∞)
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:
simp [not_le_of_gt hin]

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
i : ℕ
𝕜' : Type u_5
inst_7 : NontriviallyNormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
⊢ Eq (α := (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{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))
    (⇑(iteratedFDerivLM 𝕜' n k i) :
      (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
i : ℕ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl

Premises used: ContDiffMapSupportedIn.structureMapLM, rfl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
⊢ Eq (α := (a : 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) f :
          E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F) :
      (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F)
    (if (↑i : ℕ∞) ≤ n then iteratedFDeriv ℝ i (⇑f : (a : E) → F) else 0)

Tactic:
simp [structureMapLM]

Premises used: ContDiffMapSupportedIn.structureMapLM
-- 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
K : Compacts E
i : ℕ
f : 𝓓_{K}(E, F)
⊢ Eq (α := (a : E) → ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
    (⇑((structureMapLM 𝕜 ⊤ i : (a : 𝓓_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) f :
          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:
simp [structureMapLM_eq]

Premises used: ContDiffMapSupportedIn.structureMapLM_eq
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
i : ℕ
𝕜' : Type u_5
inst_7 : NontriviallyNormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
⊢ Eq (α := (a : 𝓓^{n}_{K}(E, F)) → 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)
    (⇑(structureMapLM 𝕜' n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
x : E
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)
⊢ 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)

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 : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
x : E
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:
simp [structureMapLM_apply, iteratedFDeriv_zero_eq_comp]

Premises used: iteratedFDeriv_zero_eq_comp, ContDiffMapSupportedIn.structureMapLM_apply
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
f g : 𝓓^{n}_{K}(E, F)
hfg :
  Eq (α := E →ᵇ 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)
    ((structureMapLM 𝕜 n 0 : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin 0) ↦ E) F) g :
      E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ E) F)
⊢ f = g

Tactic:
simpa [BoundedContinuousFunction.ext_iff, ContinuousMultilinearMap.ext_iff,
    structureMapLM_zero_apply, ContDiffMapSupportedIn.ext_iff] using hfg

Premises used: ContDiffMapSupportedIn.ext_iff, ContinuousMultilinearMap.ext_iff, ContDiffMapSupportedIn.structureMapLM_zero_apply, BoundedContinuousFunction.ext_iff
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
⊢ Eq (α := UniformSpace 𝓓^{n}_{K}(E, F)) uniformSpace
    (⨅ (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:
UniformSpace.replaceTopology_eq _ toTopologicalSpace_iInf.symm

Premises used: setOf, UniformSpace.replaceTopology_eq, UniformSpace.toTopologicalSpace_iInf, Eq.symm
-- 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
⊢ IsTopologicalAddGroup 𝓓^{n}_{K}(E, F)

Tactic:
topologicalAddGroup_iInf fun _ ↦ topologicalAddGroup_induced _

Premises used: Unit.unit, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat, topologicalAddGroup_iInf
-- 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
rw : IsUniformAddGroup 𝓓^{n}_{K}(E, F)
⊢ IsUniformAddGroup 𝓓^{n}_{K}(E, F)

Tactic:
rw [ContDiffMapSupportedIn.uniformSpace_eq_iInf]

Premises used: ContDiffMapSupportedIn.uniformSpace_eq_iInf
-- 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
⊢ IsUniformAddGroup 𝓓^{n}_{K}(E, F)

Tactic:
isUniformAddGroup_iInf fun _ ↦ IsUniformAddGroup.comap _

Premises used: Unit.unit, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, isUniformAddGroup_iInf, Function.const, Lean.Name, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
⊢ IsUniformAddGroup 𝓓^{n}_{K}(E, F)

Tactic:
exact isUniformAddGroup_iInf fun _ ↦ IsUniformAddGroup.comap _

Premises used: isUniformAddGroup_iInf, IsUniformAddGroup.comap
-- 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
⊢ ContinuousSMul 𝕜 𝓓^{n}_{K}(E, F)

Tactic:
continuousSMul_iInf fun i ↦ continuousSMul_induced (structureMapLM 𝕜 n i)

Premises used: ContDiffMapSupportedIn.structureMapLM, continuousSMul_induced, continuousSMul_iInf
-- 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
⊢ LocallyConvexSpace ℝ 𝓓^{n}_{K}(E, F)

Tactic:
LocallyConvexSpace.iInf fun _ ↦ LocallyConvexSpace.induced _

Premises used: Unit.unit, sorryAx, LocallyConvexSpace.iInf, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
⊢ Eq (α := (a : E) → ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
    (⇑((structureMapCLM 𝕜 n i : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) f :
          E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F) :
      (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F)
    (if (↑i : ℕ∞) ≤ n then iteratedFDeriv ℝ i (⇑f : (a : E) → F) else 0)

Tactic:
simp [structureMapCLM, structureMapLM_apply]

Premises used: ContDiffMapSupportedIn.structureMapCLM, ContDiffMapSupportedIn.structureMapLM_apply
-- 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
K : Compacts E
i : ℕ
f : 𝓓_{K}(E, F)
⊢ Eq (α := (a : E) → ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
    (⇑((structureMapCLM 𝕜 ⊤ i : (a : 𝓓_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) f :
          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:
simp [structureMapCLM, structureMapLM_top_apply]

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
x : E
⊢ Eq (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ E) F)
    ((((structureMapCLM 𝕜 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)

Tactic:
structureMapLM_zero_apply 𝕜

Premises used: ContDiffMapSupportedIn.structureMapLM_zero_apply
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
⊢ Injective (α := 𝓓^{n}_{K}(E, F)) (β := E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ E) F)
    (⇑(structureMapCLM 𝕜 n 0) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin 0) ↦ E) F)

Tactic:
structureMapLM_zero_injective 𝕜

Premises used: ContDiffMapSupportedIn.structureMapLM_zero_injective
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
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)
⊢ 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)

Tactic:
simp_rw [isUniformInducing_iff_uniformSpace, ContDiffMapSupportedIn.uniformSpace_eq_iInf,
      Pi.uniformSpace_eq, comap_iInf, ← comap_comap]

Premises used: Pi.uniformSpace_eq, ContDiffMapSupportedIn.uniformSpace_eq_iInf, isUniformInducing_iff_uniformSpace, UniformSpace.comap_comap, UniformSpace.comap_iInf
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
⊢ 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:
rfl