awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n : ℕ∞
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')
      (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))
ℝ₁ :
  ‖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 : ℝ)
⊢ 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 : ℝ)

Tactic:
calc
      ‖iteratedFDeriv ℝ i (T' ∘ f) x‖
  _ = ‖T'.compContinuousMultilinearMap (iteratedFDeriv ℝ i f x)‖ := by
        rw [T'.iteratedFDeriv_comp_left f.contDiff.contDiffAt (mod_cast hi)]
  _ ≤ ‖T'‖ * ‖iteratedFDeriv ℝ i f x‖ := T'.norm_compContinuousMultilinearMap_le _
  _ ≤ ‖T'‖ * N[ℝ]_{K, n, i} f := by grw [norm_iteratedFDeriv_apply_le_seminorm ℝ hi]

Premises used: Real, ContinuousLinearMap.norm_compContinuousMultilinearMap_le, ContDiffMapSupportedIn.seminorm, ContinuousLinearMap.compContinuousMultilinearMap, Function.comp, iteratedFDeriv, 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 n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
T : F →L[𝕜] F'
⊢ Continuous (X := 𝓓^{n}_{K}(E, F)) (Y := 𝓓^{n}_{K}(E, F')) (⇑(postcompLM T) : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}_{K}(E, F'))

Tactic:
continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
      (ContDiffMapSupportedIn.withSeminorms ..) _ (.of_real fun i ↦ ⟨{i}, ‖T‖, fun f ↦ ?_⟩)

Premises used: Norm.norm, Seminorm.IsBounded.of_real, Exists.intro, WithSeminorms.continuous_of_isBounded, ContDiffMapSupportedIn.withSeminorms, Singleton.singleton
-- 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
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
T : F →L[𝕜] F'
refine :
  ∀ (i : ℕ) (f : 𝓓^{n}_{K}(E, 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‖
        ((Finset.sup {i} (ContDiffMapSupportedIn.seminorm 𝕜 E F n K) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
⊢ Continuous (X := 𝓓^{n}_{K}(E, F)) (Y := 𝓓^{n}_{K}(E, F')) (⇑(postcompLM T) : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}_{K}(E, F'))

Tactic:
refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
      (ContDiffMapSupportedIn.withSeminorms ..) _ (.of_real fun i ↦ ⟨{i}, ‖T‖, fun f ↦ ?_⟩)

Premises used: Norm.norm, Seminorm.IsBounded.of_real, Exists.intro, WithSeminorms.continuous_of_isBounded, ContDiffMapSupportedIn.withSeminorms, Singleton.singleton
-- 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
inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜
T : F →L[𝕜] F'
i : ℕ
f : 𝓓^{n}_{K}(E, 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‖
      ((Finset.sup {i} (ContDiffMapSupportedIn.seminorm 𝕜 E F n K) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)

Tactic:
simpa using seminorm_postcompLM_le 𝕜 T f

Premises used: ContDiffMapSupportedIn.seminorm_postcompLM_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' ℝ 𝕜
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
⊢ (⇑((postcompCLM T : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{n}_{K}(E, F')) f : 𝓓^{n}_{K}(E, F')) : (a : E) → F') =
    (⇑T : (a : F) → F') ∘ (⇑f : (a : 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
pos :
  ∀ (H : n₂ ≤ n₁ ∧ K₁ ≤ K₂),
    LE.le (α := ℝ)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i : (a : 𝓓^{n₂}_{K₂}(E, F)) → ℝ)
          ((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) f : 𝓓^{n₂}_{K₂}(E, F)) :
        ℝ)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f : ℝ)
neg :
  ∀ (H : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)),
    LE.le (α := ℝ)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i : (a : 𝓓^{n₂}_{K₂}(E, F)) → ℝ)
          ((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) f : 𝓓^{n₂}_{K₂}(E, F)) :
        ℝ)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f : ℝ)
⊢ LE.le (α := ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i : (a : 𝓓^{n₂}_{K₂}(E, F)) → ℝ)
        ((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) f : 𝓓^{n₂}_{K₂}(E, F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f : ℝ)

Tactic:
by_cases H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
-- 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
pos :
  (↑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) ≤
        (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f
⊢ LE.le (α := ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i : (a : 𝓓^{n₂}_{K₂}(E, F)) → ℝ)
        ((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) f : 𝓓^{n₂}_{K₂}(E, F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f : ℝ)

Tactic:
simp (discharger := positivity) only [ContDiffMapSupportedIn.seminorm_le_iff, monoLM_apply, H,
      and_self, ↓reduceIte]

Premises used: ContDiffMapSupportedIn.monoLM_apply, and_self, ContDiffMapSupportedIn.seminorm_le_iff, reduceIte
-- 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
hik : (↑i : ℕ∞) ≤ n₂
pos :
  ∀ x ∈ K₂,
    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 n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f
⊢ ∀ x ∈ K₂,
    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 n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f

Tactic:
_
-- 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
hik : (↑i : ℕ∞) ≤ n₂
x : E
pos :
  x ∈ K₂ →
    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 n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f
⊢ x ∈ K₂ →
    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 n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f

Tactic:
_
-- 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
hik : (↑i : ℕ∞) ≤ n₂
x : E
h : x ∈ K₂
⊢ 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 n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f

Tactic:
norm_iteratedFDeriv_apply_le_seminorm _ (hik.trans (mod_cast H.1))

Premises used: ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm, LE.le.trans
-- 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
hik : (↑i : ℕ∞) ≤ n₂
x : E
h : x ∈ K₂
⊢ 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 n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f

Tactic:
exact norm_iteratedFDeriv_apply_le_seminorm _ (hik.trans (mod_cast H.1))

Premises used: ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm, LE.le.trans
-- 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
⊢ LE.le (α := ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i : (a : 𝓓^{n₂}_{K₂}(E, F)) → ℝ)
        ((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) f : 𝓓^{n₂}_{K₂}(E, F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f : ℝ)

Tactic:
simp [monoLM_eq_zero, H]

Premises used: ContDiffMapSupportedIn.monoLM_eq_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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
h₁ : n₁ = n₂
h₂ : K₁ ≤ K₂
f : 𝓓^{n₁}_{K₁}(E, F)
⊢ Eq (α := ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i : (a : 𝓓^{n₂}_{K₂}(E, F)) → ℝ)
        ((monoLM 𝕜 : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) f : 𝓓^{n₂}_{K₂}(E, F)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i : (a : 𝓓^{n₁}_{K₁}(E, F)) → ℝ) f : ℝ)

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

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 := 𝓓^{n₂}_{K₂}(E, F))
    (⇑(monoLM 𝕜) : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F))

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

Premises used: Exists.intro, 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 :
  ∀ (i : ℕ) (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₂ := 𝓓^{n₂}_{K₂}(E, F)) (σ₁₂ := RingHom.id 𝕜)
          (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) (monoLM 𝕜))
        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 {i} (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁)))
        f)
⊢ Continuous (X := 𝓓^{n₁}_{K₁}(E, F)) (Y := 𝓓^{n₂}_{K₂}(E, F))
    (⇑(monoLM 𝕜) : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F))

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

Premises used: Exists.intro, 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
i : ℕ
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₂ := 𝓓^{n₂}_{K₂}(E, F)) (σ₁₂ := RingHom.id 𝕜)
        (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) (monoLM 𝕜))
      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 {i} (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁)))
      f)

Tactic:
simpa using seminorm_monoLM_le 𝕜 f

Premises used: ContDiffMapSupportedIn.seminorm_monoLM_le
-- 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
f : 𝓓^{n₁}_{K₁}(E, F)
⊢ (⇑((monoCLM 𝕜 : (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:
monoLM_apply 𝕜 f

Premises used: ContDiffMapSupportedIn.monoLM_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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
H : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
h :
  ∀ (x : 𝓓^{n₁}_{K₁}(E, F)) (a : E),
    (((monoCLM 𝕜 : (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
⊢ Eq (α := 𝓓^{n₁}_{K₁}(E, F) →L[𝕜] 𝓓^{n₂}_{K₂}(E, F)) (monoCLM 𝕜) 0

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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
H : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
x : 𝓓^{n₁}_{K₁}(E, F)
a : E
⊢ (((monoCLM 𝕜 : (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:
simp [H]
-- 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
𝕜' : Type u_5
inst_7 : NontriviallyNormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
⊢ Eq (α := (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F)) (⇑(monoCLM 𝕜) : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(E, F))
    (⇑(monoCLM 𝕜') : (a : 𝓓^{n₁}_{K₁}(E, F)) → 𝓓^{n₂}_{K₂}(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 : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
pos :
  ∀ (hk : k + 1 ≤ n),
    LE.le (α := ℝ)
      (((ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i : Seminorm 𝕜 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
            (a : 𝓓^{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)) :
        ℝ)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
neg :
  ∀ (hk : n < k + 1),
    LE.le (α := ℝ)
      (((ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i : Seminorm 𝕜 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
            (a : 𝓓^{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)) :
        ℝ)
      ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
⊢ LE.le (α := ℝ)
    (((ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i : Seminorm 𝕜 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
          (a : 𝓓^{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)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)

Tactic:
by_cases! hk : k + 1 ≤ n
-- 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)
hk : k + 1 ≤ n
pos :
  (↑i : ℕ∞) ≤ k →
    ∀ x ∈ K,
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) (E →L[ℝ] F))
          (iteratedFDeriv ℝ i
            (⇑((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)
            x) ≤
        (ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f
⊢ LE.le (α := ℝ)
    (((ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i : Seminorm 𝕜 𝓓^{k}_{K}(E, E →L[ℝ] F)) :
          (a : 𝓓^{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)) :
      ℝ)
    ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)

Tactic:
rw [ContDiffMapSupportedIn.seminorm_le_iff 𝕜 (apply_nonneg ..)]

Premises used: ContDiffMapSupportedIn.seminorm_le_iff, NonnegHomClass.apply_nonneg
-- 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)
hk : k + 1 ≤ n
hi : (↑i : ℕ∞) ≤ k
x : E
hx : x ∈ K
⊢ HAdd.hAdd (α := ℕ∞) (↑i : ℕ∞) 1 ≤ n

Tactic:
have hi' : i + 1 ≤ n := (add_le_add_left hi 1).trans hk
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
n k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
hi : (↑i : ℕ∞) ≤ k
x : E
hx : x ∈ K
hi' : HAdd.hAdd (α := ℕ∞) (↑i : ℕ∞) 1 ≤ n
⊢ norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) (E →L[ℝ] F))
      (iteratedFDeriv ℝ i
        (⇑((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)
        x) ≤
    (ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1) : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f

Tactic:
simpa [hk, norm_iteratedFDeriv_fderiv] using
      norm_iteratedFDeriv_apply_le_seminorm 𝕜 hi'

Premises used: ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm, norm_iteratedFDeriv_fderiv