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 : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
this :
  (∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
          (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
        C) ↔
    ∀ x ∈ K,
      norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
          (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
        C
hi : ¬(↑i : ℕ∞) ≤ n
⊢ n < (↑i : ℕ∞)

Tactic:
push Not at hi

Premises used: Not
-- 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
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
this :
  (∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
          (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
        C) ↔
    ∀ x ∈ K,
      norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
          (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
        C
hi : n < (↑i : ℕ∞)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f ≤ C ↔
    (↑i : ℕ∞) ≤ n →
      ∀ x ∈ K,
        norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
            (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
          C

Tactic:
simp [hi, ContDiffMapSupportedIn.seminorm_eq_bot_of_gt _ hi, hC]

Premises used: ContDiffMapSupportedIn.seminorm_eq_bot_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
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓_{K}(E, F)
simp_rw :
  (LE.le (α := ℕ∞) (↑i : ℕ∞) ⊤ →
      ∀ x ∈ K,
        norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
            (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
          C) ↔
    ∀ x ∈ K,
      norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
          (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
        C
simp_rw₁ :
  (True →
      ∀ x ∈ K,
        norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
            (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
          C) ↔
    ∀ x ∈ K,
      norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
          (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
        C
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F ⊤ K i : (a : 𝓓_{K}(E, F)) → ℝ) f ≤ C ↔
    ∀ x ∈ K,
      norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
          (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
        C

Tactic:
simp_rw [ContDiffMapSupportedIn.seminorm_le_iff 𝕜 hC, le_top, forall_const]

Premises used: ContDiffMapSupportedIn.seminorm_le_iff, le_top, forall_const
-- 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 : ℕ
hin : (↑i : ℕ∞) ≤ n
f : 𝓓^{n}_{K}(E, F)
x : E
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
      (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) =
    norm (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)
          x :
        ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)

Tactic:
simp [structureMapLM_apply, hin]

Premises used: 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)
x : E
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
      (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
    (ContDiffMapSupportedIn.seminorm 𝕜 E F ⊤ K i : (a : 𝓓_{K}(E, F)) → ℝ) f

Tactic:
norm_iteratedFDeriv_apply_le_seminorm 𝕜 (mod_cast le_top)

Premises used: ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm
-- 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
rw :
  norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ E) F)
      (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x) ≤
    (ContDiffMapSupportedIn.seminorm 𝕜 E F n K 0 : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f
⊢ ‖(f : (a : E) → F) x‖ ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K 0 : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f

Tactic:
rw [← norm_iteratedFDeriv_zero (𝕜 := ℝ) (f := f) (x := x)]

Premises used: norm_iteratedFDeriv_zero
-- 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
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ E) F)
      (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x) ≤
    (ContDiffMapSupportedIn.seminorm 𝕜 E F n K 0 : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f

Tactic:
norm_iteratedFDeriv_apply_le_seminorm 𝕜 zero_le

Premises used: zero_le, ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm, setOf
-- 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
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 0) ↦ E) F)
      (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x) ≤
    (ContDiffMapSupportedIn.seminorm 𝕜 E F n K 0 : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f

Tactic:
exact norm_iteratedFDeriv_apply_le_seminorm 𝕜 zero_le

Premises used: zero_le, ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm
-- 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)
⊢ norm (E := E →ᵇ F) { toFun := (⇑f : (a : E) → F), continuous_toFun := ⋯, map_bounded' := ⋯ : E →ᵇ F } =
    (ContDiffMapSupportedIn.seminorm 𝕜 E F n K 0 : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f

Tactic:
simp [BoundedContinuousFunction.norm_eq_iSup_norm,
    ContDiffMapSupportedIn.seminorm_apply, structureMapCLM_apply]

Premises used: ContDiffMapSupportedIn.structureMapCLM_apply, ContDiffMapSupportedIn.seminorm_apply, BoundedContinuousFunction.norm_eq_iSup_norm
-- 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
⊢ Continuous (X := 𝓓^{n}_{K}(E, F)) (Y := E →ᵇ F) (⇑(toBoundedContinuousFunctionLM 𝕜) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ F)

Tactic:
continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
      (norm_withSeminorms 𝕜 _) _ (fun _ ↦ ⟨{0}, 1, fun f ↦ ?_⟩)

Premises used: Exists.intro, norm_withSeminorms, WithSeminorms.continuous_of_isBounded, ContDiffMapSupportedIn.withSeminorms, Singleton.singleton, 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
refine :
  ∀ (x : Fin 1) (f : 𝓓^{n}_{K}(E, F)),
    LE.le (α := (fun (a : 𝓓^{n}_{K}(E, F)) ↦ ℝ) f)
      ((fun (f : Seminorm 𝕜 𝓓^{n}_{K}(E, F)) ↦ ((⇑f : (a : 𝓓^{n}_{K}(E, F)) → ℝ) : (a : 𝓓^{n}_{K}(E, F)) → ℝ))
        (Seminorm.comp (E₂ := E →ᵇ F) (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 (E →ᵇ F)) (toBoundedContinuousFunctionLM 𝕜))
        f)
      ((fun (f : Seminorm 𝕜 𝓓^{n}_{K}(E, F)) ↦ ((⇑f : (a : 𝓓^{n}_{K}(E, F)) → ℝ) : (a : 𝓓^{n}_{K}(E, F)) → ℝ))
        (HSMul.hSMul (α := ℝ≥0) (β := Seminorm 𝕜 𝓓^{n}_{K}(E, F)) 1
          (Finset.sup {0} (ContDiffMapSupportedIn.seminorm 𝕜 E F n K)))
        f)
⊢ Continuous (X := 𝓓^{n}_{K}(E, F)) (Y := E →ᵇ F) (⇑(toBoundedContinuousFunctionLM 𝕜) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ F)

Tactic:
refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
      (norm_withSeminorms 𝕜 _) _ (fun _ ↦ ⟨{0}, 1, fun f ↦ ?_⟩)

Premises used: Exists.intro, norm_withSeminorms, WithSeminorms.continuous_of_isBounded, ContDiffMapSupportedIn.withSeminorms, Singleton.singleton, 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
x : Fin 1
f : 𝓓^{n}_{K}(E, F)
⊢ LE.le (α := (fun (a : 𝓓^{n}_{K}(E, F)) ↦ ℝ) f)
    ((fun (f : Seminorm 𝕜 𝓓^{n}_{K}(E, F)) ↦ ((⇑f : (a : 𝓓^{n}_{K}(E, F)) → ℝ) : (a : 𝓓^{n}_{K}(E, F)) → ℝ))
      (Seminorm.comp (E₂ := E →ᵇ F) (σ₁₂ := RingHom.id 𝕜) (normSeminorm 𝕜 (E →ᵇ F)) (toBoundedContinuousFunctionLM 𝕜))
      f)
    ((fun (f : Seminorm 𝕜 𝓓^{n}_{K}(E, F)) ↦ ((⇑f : (a : 𝓓^{n}_{K}(E, F)) → ℝ) : (a : 𝓓^{n}_{K}(E, F)) → ℝ))
      (HSMul.hSMul (α := ℝ≥0) (β := Seminorm 𝕜 𝓓^{n}_{K}(E, F)) 1
        (Finset.sup {0} (ContDiffMapSupportedIn.seminorm 𝕜 E F n K)))
      f)

Tactic:
simp [norm_toBoundedContinuousFunction 𝕜 f]

Premises used: ContDiffMapSupportedIn.norm_toBoundedContinuousFunction
-- 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)
⊢ Eq (α := E →ᵇ F) ((toBoundedContinuousFunctionCLM 𝕜 : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ F) f : E →ᵇ F)
    ({ toFun := (⇑f : (a : E) → F), continuous_toFun := ⋯, map_bounded' := ⋯ } : 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
𝕜' : Type u_5
inst_7 : NontriviallyNormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
⊢ Eq (α := (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ F) (⇑(toBoundedContinuousFunctionCLM 𝕜) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ F)
    (⇑(toBoundedContinuousFunctionCLM 𝕜') : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
⊢ ContinuousEval 𝓓^{n}_{K}(E, F) E F

Tactic:
ContinuousEval.of_continuous_forget
    (toBoundedContinuousFunctionCLM ℝ).continuous

Premises used: Real, ContinuousLinearMap.continuous, ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM, ContinuousEval.of_continuous_forget
-- 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
⊢ T3Space 𝓓^{n}_{K}(E, F)

Tactic:
have : Injective (toBoundedContinuousFunctionCLM ℝ : 𝓓^{n}_{K}(E, F) →L[ℝ] E →ᵇ F) :=
    fun _ _ hfg ↦ ext fun x ↦ congr(($hfg : E → F) x)
  have : T2Space 𝓓^{n}_{K}(E, F) := .of_injective_continuous this
    (toBoundedContinuousFunctionCLM ℝ).continuous
  inferInstance

Premises used: Real, congrArg, T2Space.of_injective_continuous, inferInstance, ContDiffMapSupportedIn.ext, id, ContinuousLinearMap.continuous, ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
change :
  (ContDiffMapSupportedIn.seminorm ℝ E F' n K i : (a : 𝓓^{n}_{K}(E, F')) → ℝ)
      ((postcompLM T' : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}_{K}(E, F')) f : 𝓓^{n}_{K}(E, F')) ≤
    HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F' n K i : (a : 𝓓^{n}_{K}(E, F')) → ℝ)
      ((postcompLM T : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}_{K}(E, F')) f : 𝓓^{n}_{K}(E, F')) ≤
    HMul.hMul (β := ℝ) ‖T‖ ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)

Tactic:
change N[ℝ]_{K, n, i} (postcompLM T' f) ≤ ‖T'‖ * N[ℝ]_{K, n, i} f

Premises used: Real, ContDiffMapSupportedIn.seminorm, ContDiffMapSupportedIn.postcompLM, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
⊢ 0 ≤ HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
rw :
  (↑i : ℕ∞) ≤ n →
    ∀ x ∈ K,
      norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
          (iteratedFDeriv ℝ i
            (⇑((postcompLM T' : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}_{K}(E, F')) f : 𝓓^{n}_{K}(E, F')) : (a : E) → F') x) ≤
        HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
⊢ (ContDiffMapSupportedIn.seminorm ℝ E F' n K i : (a : 𝓓^{n}_{K}(E, F')) → ℝ)
      ((postcompLM T' : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}_{K}(E, F')) f : 𝓓^{n}_{K}(E, F')) ≤
    HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)

Tactic:
rw [ContDiffMapSupportedIn.seminorm_le_iff ℝ (by positivity)]

Premises used: Real, ContDiffMapSupportedIn.seminorm_le_iff
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
hi : (↑i : ℕ∞) ≤ n
x : E
hx : x ∈ K
rw :
  norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
      (iteratedFDeriv ℝ i ((⇑T' : (a : F) → F') ∘ (⇑f : (a : E) → F)) x) ≤
    HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
      (iteratedFDeriv ℝ i
        (⇑((postcompLM T' : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}_{K}(E, F')) f : 𝓓^{n}_{K}(E, F')) : (a : E) → F') x) ≤
    HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)

Tactic:
rw [postcompLM_apply]

Premises used: ContDiffMapSupportedIn.postcompLM_apply
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
hi : (↑i : ℕ∞) ≤ n
x : E
hx : x ∈ K
rw rw₁ :
  norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
      (T'.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x)) =
    norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
      (T'.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x))
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
      (iteratedFDeriv ℝ i ((⇑T' : (a : F) → F') ∘ (⇑f : (a : E) → F)) x) =
    norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
      (T'.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x))

Tactic:
rw [T'.iteratedFDeriv_comp_left f.contDiff.contDiffAt (mod_cast hi)]

Premises used: ContDiffMapSupportedIn.contDiff, ContinuousLinearMap.iteratedFDeriv_comp_left, 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 : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
hi : (↑i : ℕ∞) ≤ n
x : E
hx : x ∈ K
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_4} ℝ (fun (i : Fin i) ↦ E) F')
      (T'.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x)) ≤
    ‖T'‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x)

Tactic:
T'.norm_compContinuousMultilinearMap_le _

Premises used: ContinuousLinearMap.norm_compContinuousMultilinearMap_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 : ℕ∞
K : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
hi : (↑i : ℕ∞) ≤ n
x : E
hx : x ∈ K
h₁ : 0 ≤ ‖T'‖
grw grw₁ :
  HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ) ≤
    HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
⊢ ‖T'‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) x) ≤
    HMul.hMul (β := ℝ) ‖T'‖ ((ContDiffMapSupportedIn.seminorm ℝ E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)

Tactic:
grw [norm_iteratedFDeriv_apply_le_seminorm ℝ hi]

Premises used: ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm, Real