awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
X : Type u_5
inst_4 : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
⊢ (∀ (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) ∘
            φ)
have a : ∀ (i : ℕ),
  Continuous[inst_4, _]
      ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
        φ) ↔
    (↑i : ℕ∞) ≤ n →
      Continuous[inst_4, _]
        ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
          φ)
Tactic: congrm (∀ i, ?_)
-- 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)
i : ℕ
⊢ Continuous[inst_4, _]
      ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
        φ) ↔
    (↑i : ℕ∞) ≤ n →
      Continuous[inst_4, _]
        ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
          φ)
have pos : ∀ (hin : (↑i : ℕ∞) ≤ n),
  Continuous[inst_4, _]
      ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
        φ) ↔
    (↑i : ℕ∞) ≤ n →
      Continuous[inst_4, _]
        ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
          φ)
Tactic: by_cases hin : i ≤ n
-- 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)
i : ℕ
pos :
  ∀ (hin : (↑i : ℕ∞) ≤ n),
    Continuous[inst_4, _]
        ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
          φ) ↔
      (↑i : ℕ∞) ≤ n →
        Continuous[inst_4, _]
          ((⇑(structureMapCLM ℝ n i) :
              (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
            φ)
⊢ Continuous[inst_4, _]
      ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
        φ) ↔
    (↑i : ℕ∞) ≤ n →
      Continuous[inst_4, _]
        ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
          φ)
have neg : ∀ (hin : ¬(↑i : ℕ∞) ≤ n),
  Continuous[inst_4, _]
      ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
        φ) ↔
    (↑i : ℕ∞) ≤ n →
      Continuous[inst_4, _]
        ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
          φ)
Tactic: by_cases hin : i ≤ n
-- 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)
i : ℕ
hin : ¬(↑i : ℕ∞) ≤ n
⊢ Continuous[inst_4, _]
      ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
        φ) ↔
    (↑i : ℕ∞) ≤ n →
      Continuous[inst_4, _]
        ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
          φ)
have neg : Continuous[inst_4, _]
  ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘ φ)
Tactic: simp only [hin, true_imp_iff, false_imp_iff, iff_true]
-- 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)
i : ℕ
hin : ¬(↑i : ℕ∞) ≤ n
⊢ Continuous[inst_4, _]
    ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘ φ)
have neg : ∀ (x : X),
  Eq (α := E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F) (0 x)
    (((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘ φ)
      x)
Tactic: refine continuous_zero.congr fun x ↦ ?_
-- 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)
i : ℕ
hin : ¬(↑i : ℕ∞) ≤ n
x : X
⊢ Eq (α := E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F) (0 x)
    (((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘ φ)
      x)
have neg : ∀ (t : E),
  Eq (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
    ((0 x : (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) t :
      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) ∘ φ)
            x :
          (a : E) → ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F)
        t :
      ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F)
Tactic: ext t : 1
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (hypothesis)
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
p : SeminormFamily 𝕜 𝓓^{n}_{K}(E, F) ((_ : ℕ) × Fin 1) :=
  SeminormFamily.sigma (κ := fun (x : ℕ) ↦ Fin 1) fun (i : ℕ) (x : Fin 1) ↦
    Seminorm.comp (E₂ := E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F) (σ₁₂ := RingHom.id 𝕜)
      (normSeminorm 𝕜 (E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F) :
        Seminorm 𝕜 (E →ᵇ ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin i) ↦ E) F))
      (structureMapLM 𝕜 n i)
⊢ WithSeminorms (𝕜 := 𝕜) (E := 𝓓^{n}_{K}(E, F)) (ι := ℕ) (ContDiffMapSupportedIn.seminorm 𝕜 E F n K)
have this : WithSeminorms p
Tactic: have : WithSeminorms p :=
    withSeminorms_iInf fun i ↦ LinearMap.withSeminorms_induced (norm_withSeminorms _ _) _
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (hypothesis)
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 : n < (↑i : ℕ∞)
⊢ Eq (α := Seminorm 𝕜 𝓓^{n}_{K}(E, F)) (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) ⊥
have this : ¬(↑i : ℕ∞) ≤ n
Tactic: have : ¬(i ≤ n) := by simpa using hin
-- 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
i : ℕ
hin : n < (↑i : ℕ∞)
this : ¬(↑i : ℕ∞) ≤ n
⊢ Eq (α := Seminorm 𝕜 𝓓^{n}_{K}(E, F)) (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) ⊥
have h : ∀ (f : 𝓓^{n}_{K}(E, F)),
  Eq (α := ℝ) ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
    ((⊥ : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
Tactic: ext f
-- 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
i : ℕ
hin : n < (↑i : ℕ∞)
this : ¬(↑i : ℕ∞) ≤ n
f : 𝓓^{n}_{K}(E, F)
⊢ Eq (α := ℝ) ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
    ((⊥ : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
have h : norm (E := 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) =
  0
Tactic: simp [ContDiffMapSupportedIn.seminorm_apply, BoundedContinuousFunction.ext_iff,
    structureMapCLM_apply, this]
-- 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
C : ℝ
hC : 0 ≤ C
i : ℕ
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) ≤
        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
have a : ∀ (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
Tactic: congrm ∀ x, ?_
-- 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
C : ℝ
hC : 0 ≤ C
i : ℕ
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) ≤
      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
have pos : ∀ (hx : 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
Tactic: by_cases hx : x ∈ K
-- 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
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
x : E
pos :
  ∀ (hx : 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
⊢ 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
have neg : ∀ (hx : 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
Tactic: by_cases hx : x ∈ K
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (hypothesis)
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)
⊢ (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
have 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
Tactic: have : (∀ x, ‖iteratedFDeriv ℝ i f x‖ ≤ C) ↔ (∀ x ∈ K, ‖iteratedFDeriv ℝ i f x‖ ≤ C) := by
    congrm ∀ x, ?_
    by_cases hx : x ∈ K
    · simp [hx]
    · simp [hx, f.iteratedFDeriv_zero_on_compl hx, hC]
-- 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
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
⊢ (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
have pos : ∀ (hi : (↑i : ℕ∞) ≤ n),
  (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: by_cases hi : i ≤ n
-- 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
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
pos :
  ∀ (hi : (↑i : ℕ∞) ≤ n),
    (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
⊢ (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
have neg : ∀ (hi : ¬(↑i : ℕ∞) ≤ n),
  (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: by_cases hi : i ≤ n
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (hypothesis)
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
⊢ (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
have hi₁ : n < (↑i : ℕ∞)
Tactic: push Not at hi
Cleared hypotheses: hi
-- 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
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓_{K}(E, F)
⊢ (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
have 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
Tactic: simp_rw [ContDiffMapSupportedIn.seminorm_le_iff 𝕜 hC, le_top, forall_const]
-- 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
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
⊢ (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
have 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
Tactic: simp_rw [ContDiffMapSupportedIn.seminorm_le_iff 𝕜 hC, le_top, forall_const]
-- 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
⊢ ‖(f : (a : E) → F) x‖ ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K 0 : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f
have 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
Tactic: rw [← norm_iteratedFDeriv_zero (𝕜 := ℝ) (f := f) (x := x)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.ContDiffMapSupportedIn (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
⊢ Continuous (X := 𝓓^{n}_{K}(E, F)) (Y := E →ᵇ F) (⇑(toBoundedContinuousFunctionLM 𝕜) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ F)
have 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)
Tactic: refine continuous_of_isBounded (ContDiffMapSupportedIn.withSeminorms ..)
      (norm_withSeminorms 𝕜 _) _ (fun _ ↦ ⟨{0}, 1, fun f ↦ ?_⟩)
-- 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 : ℕ∞
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
⊢ (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 : ℝ)
have 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 : ℝ)
Tactic: change N[ℝ]_{K, n, i} (postcompLM T' f) ≤ ‖T'‖ * N[ℝ]_{K, n, i} f