awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
X : Type u_5
inst_4 : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
⊢ Continuous[inst_4, _] φ ↔
    ∀ (i : ℕ),
      Continuous[inst_4, _]
        ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
          φ)

Tactic:
simp [continuous_iInf_rng, continuous_induced_rng, structureMapCLM]

Premises used: continuous_iInf_rng, ContDiffMapSupportedIn.structureMapCLM, continuous_induced_rng
-- 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
X : Type u_5
inst_4 : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
rw :
  (∀ (i : ℕ),
      Continuous[inst_4, _]
        ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
          φ)) ↔
    ∀ (i : ℕ),
      (↑i : ℕ∞) ≤ n →
        Continuous[inst_4, _]
          ((⇑(structureMapCLM ℝ n i) :
              (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
            φ)
⊢ Continuous[inst_4, _] φ ↔
    ∀ (i : ℕ),
      (↑i : ℕ∞) ≤ n →
        Continuous[inst_4, _]
          ((⇑(structureMapCLM ℝ n i) :
              (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
            φ)

Tactic:
rw [continuous_iff_comp]

Premises used: ContDiffMapSupportedIn.continuous_iff_comp
-- 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
X : Type u_5
inst_4 : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
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) ∘
            φ)
⊢ (∀ (i : ℕ),
      Continuous[inst_4, _]
        ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
          φ)) ↔
    ∀ (i : ℕ),
      (↑i : ℕ∞) ≤ n →
        Continuous[inst_4, _]
          ((⇑(structureMapCLM ℝ n i) :
              (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘
            φ)

Tactic:
congrm (∀ i, ?_)
-- 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
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) ∘
            φ)
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) ∘
            φ)
⊢ 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
-- 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
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) ∘
          φ)

Tactic:
simp only [hin, true_imp_iff, false_imp_iff, iff_true]

Premises used: iff_true, true_imp_iff, false_imp_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
X : Type u_5
inst_4 : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
i : ℕ
hin : ¬(↑i : ℕ∞) ≤ n
neg :
  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) ∘
          φ)

Tactic:
simp only [hin, true_imp_iff, false_imp_iff, iff_true]

Premises used: iff_true, true_imp_iff, false_imp_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
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) ∘ φ)

Tactic:
continuous_zero.congr fun x ↦ ?_

Premises used: Continuous.congr, continuous_zero
-- 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
X : Type u_5
inst_4 : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
i : ℕ
hin : ¬(↑i : ℕ∞) ≤ n
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)
⊢ Continuous[inst_4, _]
    ((⇑(structureMapCLM ℝ n i) : (a : 𝓓^{n}_{K}(E, F)) → E →ᵇ ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) F) ∘ φ)

Tactic:
refine continuous_zero.congr fun x ↦ ?_

Premises used: Continuous.congr, continuous_zero
-- 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
X : Type u_5
inst_4 : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
i : ℕ
hin : ¬(↑i : ℕ∞) ≤ n
x : X
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)
⊢ 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:
ext t : 1
-- 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
X : Type u_5
inst_4 : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
i : ℕ
hin : ¬(↑i : ℕ∞) ≤ n
x : X
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:
simp [hin, structureMapCLM_apply]

Premises used: ContDiffMapSupportedIn.structureMapCLM_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
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 p

Tactic:
have : WithSeminorms p :=
    withSeminorms_iInf fun i ↦ LinearMap.withSeminorms_induced (norm_withSeminorms _ _) _
-- 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
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)
this : WithSeminorms p
⊢ WithSeminorms (𝕜 := 𝕜) (E := 𝓓^{n}_{K}(E, F)) (ι := ℕ) (ContDiffMapSupportedIn.seminorm 𝕜 E F n K)

Tactic:
this.congr_equiv (Equiv.sigmaUnique _ _).symm

Premises used: ContDiffMapSupportedIn.seminorm, setOf, SeminormFamily.sigma, WithSeminorms.congr_equiv, Seminorm.comp, Equiv.symm, Equiv.sigmaUnique
-- 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
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)
this : WithSeminorms p
⊢ WithSeminorms (𝕜 := 𝕜) (E := 𝓓^{n}_{K}(E, F)) (ι := ℕ) (ContDiffMapSupportedIn.seminorm 𝕜 E F n K)

Tactic:
exact this.congr_equiv (Equiv.sigmaUnique _ _).symm

Premises used: WithSeminorms.congr_equiv, Equiv.symm, Equiv.sigmaUnique
-- 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
⊢ WithSeminorms (𝕜 := 𝕜) (E := 𝓓^{n}_{K}(E, F)) (ι := ℕ) (ContDiffMapSupportedIn.supSeminorm 𝕜 E F n K)

Tactic:
(ContDiffMapSupportedIn.withSeminorms 𝕜 E F n K).partial_sups

Premises used: ContDiffMapSupportedIn.supSeminorm, ContDiffMapSupportedIn.withSeminorms, WithSeminorms.partial_sups
-- 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)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f =
    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)

Tactic:
rfl

Premises used: setOf, 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 : ℕ
hin : n < (↑i : ℕ∞)
⊢ ¬(↑i : ℕ∞) ≤ n

Tactic:
simpa using 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 : Compacts E
i : ℕ
hin : n < (↑i : ℕ∞)
⊢ ¬(↑i : ℕ∞) ≤ n

Tactic:
have : ¬(i ≤ n) := by simpa using 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 : Compacts E
i : ℕ
hin : n < (↑i : ℕ∞)
this : ¬(↑i : ℕ∞) ≤ n
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 : ℝ)
⊢ Eq (α := Seminorm 𝕜 𝓓^{n}_{K}(E, F)) (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) ⊥

Tactic:
ext f
-- 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 : n < (↑i : ℕ∞)
this : ¬(↑i : ℕ∞) ≤ n
f : 𝓓^{n}_{K}(E, F)
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
⊢ Eq (α := ℝ) ((ContDiffMapSupportedIn.seminorm 𝕜 E F n K i : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)
    ((⊥ : (a : 𝓓^{n}_{K}(E, F)) → ℝ) f : ℝ)

Tactic:
simp [ContDiffMapSupportedIn.seminorm_apply, BoundedContinuousFunction.ext_iff,
    structureMapCLM_apply, this]

Premises used: ContDiffMapSupportedIn.structureMapCLM_apply, ContDiffMapSupportedIn.seminorm_apply, BoundedContinuousFunction.ext_iff
-- 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)
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
⊢ (∀ (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, ?_
-- 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)
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
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
⊢ 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
-- 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)
x : E
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:
simp [hx]
-- 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)
x : E
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:
simp [hx, f.iteratedFDeriv_zero_on_compl hx, hC]

Premises used: ContDiffMapSupportedIn.iteratedFDeriv_zero_on_compl
-- 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)
⊢ (∀ (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]
-- 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
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
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
⊢ (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
-- 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
⊢ (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, forall_const, ContDiffMapSupportedIn.seminorm_apply, structureMapCLM_apply,
      BoundedContinuousFunction.norm_le hC, this]

Premises used: ContDiffMapSupportedIn.structureMapCLM_apply, BoundedContinuousFunction.norm_le, ContDiffMapSupportedIn.seminorm_apply, forall_const