awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ *
      (HPow.hPow (α := ℝ≥0∞) 2 k *
        ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)) =
    eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ * HPow.hPow (α := ℝ≥0∞) 2 k *
      ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)

Tactic:
ring
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
f : 𝓢(E, F)
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
rcases :
  ∀ (k : ℕ) (C : ℝ≥0)
    (hC :
      ∀ (f : 𝓢(E, F)),
        eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
          (↑C : ℝ≥0∞) *
            ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily ℝ E F) : (a : 𝓢(E, F)) → ℝ) f)),
    eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ < ∞
⊢ eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ < ∞

Tactic:
rcases eLpNorm_le_seminorm ℝ F p μ with ⟨k, C, hC⟩

Premises used: Real, SchwartzMap.eLpNorm_le_seminorm
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
f : 𝓢(E, F)
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)),
    eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
      (↑C : ℝ≥0∞) *
        ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily ℝ E F) : (a : 𝓢(E, F)) → ℝ) f)
⊢ eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ < ∞

Tactic:
lt_of_le_of_lt (hC f) (ENNReal.mul_lt_top ENNReal.coe_lt_top ENNReal.ofReal_lt_top)

Premises used: lt_of_le_of_lt, ENNReal.ofReal_lt_top, ENNReal.mul_lt_top, ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
f : 𝓢(E, F)
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)),
    eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
      (↑C : ℝ≥0∞) *
        ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily ℝ E F) : (a : 𝓢(E, F)) → ℝ) f)
⊢ eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ < ∞

Tactic:
exact lt_of_le_of_lt (hC f) (ENNReal.mul_lt_top ENNReal.coe_lt_top ENNReal.ofReal_lt_top)

Premises used: lt_of_le_of_lt, ENNReal.ofReal_lt_top, ENNReal.mul_lt_top, ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
rcases :
  ∀ (C : ℝ),
    0 < C →
      ∀
        (hC :
          ∀ (x : E),
            HPow.hPow (β := ℕ) ‖x‖ 0 *
                norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F)
                  (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x) ≤
              C),
        MemLp.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) ∞ μ
⊢ MemLp.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) ∞ μ

Tactic:
rcases f.decay 0 0 with ⟨C, _, hC⟩

Premises used: SchwartzMap.decay, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
C : ℝ
left : 0 < C
hC :
  ∀ (x : E),
    HPow.hPow (β := ℕ) ‖x‖ 0 *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F)
          (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x) ≤
      C
⊢ MemLp.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) ∞ μ

Tactic:
memLp_top_of_bound f.continuous.aestronglyMeasurable C (ae_of_all μ fun x ↦ ?_)

Premises used: MeasureTheory.memLp_top_of_bound, SchwartzMap.continuous, MeasureTheory.ae_of_all, Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
C : ℝ
left : 0 < C
hC :
  ∀ (x : E),
    HPow.hPow (β := ℕ) ‖x‖ 0 *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F)
          (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x) ≤
      C
refine : ∀ (x : E), norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ C
⊢ MemLp.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) ∞ μ

Tactic:
refine memLp_top_of_bound f.continuous.aestronglyMeasurable C (ae_of_all μ fun x ↦ ?_)

Premises used: MeasureTheory.memLp_top_of_bound, SchwartzMap.continuous, MeasureTheory.ae_of_all, Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
C : ℝ
left : 0 < C
hC :
  ∀ (x : E),
    HPow.hPow (β := ℕ) ‖x‖ 0 *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F)
          (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x) ≤
      C
x : E
⊢ norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ C

Tactic:
simpa using hC x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ MemLp.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ

Tactic:
⟨f.continuous.aestronglyMeasurable, f.eLpNorm_lt_top p μ⟩

Premises used: SchwartzMap.eLpNorm_lt_top, SchwartzMap.continuous, MeasureTheory.MemLp, And.intro, Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ (↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) =ᶠ[ae μ] (⇑f : (a : E) → F)

Tactic:
(f.memLp p μ).coeFn_toLp

Premises used: SchwartzMap.memLp, MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
rw :
  (eLpNorm (↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) p μ).toReal =
    (eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ).toReal
rw₁ rw₂ :
  (eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ).toReal =
    (eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ).toReal
⊢ ‖f.toLp p μ‖ = (eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ).toReal

Tactic:
rw [Lp.norm_def, eLpNorm_congr_ae (coeFn_toLp f p μ)]

Premises used: SchwartzMap.coeFn_toLp, MeasureTheory.eLpNorm_congr_ae, MeasureTheory.Lp.norm_def
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
p : ℝ≥0∞
μ : Measure E
hp₁ : p ≠ 0
hp₂ : p ≠ ∞
hμ : μ.HasTemperateGrowth
⊢ 0 ≤ HPow.hPow (α := ℝ) (∫ (a : E), norm.{u_6} (E := F) ((f : (a : E) → F) a : F) ^ p.toReal ∂μ) p.toReal⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
p : ℝ≥0∞
μ : Measure E
hp₁ : p ≠ 0
hp₂ : p ≠ ∞
hμ : μ.HasTemperateGrowth
rw :
  (eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ).toReal =
    HPow.hPow (α := ℝ) (∫ (x : E), norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ^ p.toReal ∂μ) p.toReal⁻¹
rw₁ :
  (ENNReal.ofReal
        (HPow.hPow (α := ℝ) (∫ (a : E), norm.{u_6} (E := F) ((f : (a : E) → F) a : F) ^ p.toReal ∂μ)
          p.toReal⁻¹)).toReal =
    HPow.hPow (α := ℝ) (∫ (x : E), norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ^ p.toReal ∂μ) p.toReal⁻¹
rw₂ rw₃ :
  HPow.hPow (α := ℝ) (∫ (a : E), norm.{u_6} (E := F) ((f : (a : E) → F) a : F) ^ p.toReal ∂μ) p.toReal⁻¹ =
    HPow.hPow (α := ℝ) (∫ (x : E), norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ^ p.toReal ∂μ) p.toReal⁻¹
⊢ ‖f.toLp p μ‖ = HPow.hPow (α := ℝ) (∫ (x : E), norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ^ p.toReal ∂μ) p.toReal⁻¹

Tactic:
rw [norm_toLp, MeasureTheory.MemLp.eLpNorm_eq_integral_rpow_norm hp₁ hp₂ (f.memLp p μ),
    ENNReal.toReal_ofReal (by positivity)]

Premises used: SchwartzMap.memLp, SchwartzMap.norm_toLp, MeasureTheory.MemLp.eLpNorm_eq_integral_rpow_norm, ENNReal.toReal_ofReal
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ Ne (α := ℝ≥0∞) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ norm (E := ↥(Lp F 1 μ)) (f.toLp 1 μ) = ∫ (x : E), norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ∂μ

Tactic:
simpa using norm_toLp' (p := 1) (by simp) (by simp)

Premises used: SchwartzMap.norm_toLp'
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ LE.le (α := ℝ) (0 : ℝ) ((SchwartzMap.seminorm ℝ 0 0 : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
hμ : μ.HasTemperateGrowth
rw :
  eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) ∞ μ ≤
    ENNReal.ofReal ((SchwartzMap.seminorm ℝ 0 0 : (a : 𝓢(E, F)) → ℝ) f)
⊢ norm (E := ↥(Lp F ∞ μ)) (f.toLp ∞ μ) ≤ (SchwartzMap.seminorm ℝ 0 0 : (a : 𝓢(E, F)) → ℝ) f

Tactic:
rw [norm_toLp, ← ENNReal.ofReal_le_ofReal_iff (by positivity),
    ENNReal.ofReal_toReal (memLp_top f μ).eLpNorm_ne_top]

Premises used: ENNReal.ofReal_le_ofReal_iff, ENNReal.ofReal_toReal, SchwartzMap.norm_toLp, SchwartzMap.memLp_top, MeasureTheory.MemLp.eLpNorm_ne_top
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) ∞ μ ≤
    ENNReal.ofReal ((SchwartzMap.seminorm ℝ 0 0 : (a : 𝓢(E, F)) → ℝ) f)

Tactic:
eLpNormEssSup_le_of_ae_bound <| .of_forall <| norm_le_seminorm ℝ f

Premises used: Filter.limsSup, SchwartzMap.norm_le_seminorm, Real, Filter.Eventually.of_forall, MeasureTheory.eLpNormEssSup_le_of_ae_bound, Filter.limsup, MeasureTheory.eLpNormEssSup, essSup, MeasureTheory.eLpNorm, ite
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) ∞ μ ≤
    ENNReal.ofReal ((SchwartzMap.seminorm ℝ 0 0 : (a : 𝓢(E, F)) → ℝ) f)

Tactic:
exact eLpNormEssSup_le_of_ae_bound <| .of_forall <| norm_le_seminorm ℝ f

Premises used: SchwartzMap.norm_le_seminorm, Real, MeasureTheory.eLpNormEssSup_le_of_ae_bound
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : μ.IsOpenPosMeasure
f g : 𝓢(E, F)
⊢ Eq (α := ↥(Lp F p μ)) ((fun (f : 𝓢(E, F)) ↦ f.toLp p μ) f) ((fun (f : 𝓢(E, F)) ↦ f.toLp p μ) g) → f = g

Tactic:
simpa [toLp] using (Continuous.ae_eq_iff_eq μ f.continuous g.continuous).mp

Premises used: Continuous.ae_eq_iff_eq, SchwartzMap.continuous, SchwartzMap.toLp, Iff.mp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
inst_9 : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
rcases :
  ∀ (k : ℕ) (C : ℝ≥0)
    (hC :
      ∀ (f : 𝓢(E, F)),
        eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
          (↑C : ℝ≥0∞) *
            ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)),
    ∃ (k : ℕ) (C : ℝ),
      0 ≤ C ∧
        ∀ (f : 𝓢(E, F)),
          ‖f.toLp p μ‖ ≤
            HMul.hMul (β := ℝ) C
              ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ∃ (k : ℕ) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)),
        ‖f.toLp p μ‖ ≤
          HMul.hMul (β := ℝ) C
            ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
rcases eLpNorm_le_seminorm 𝕜 F p μ with ⟨k, C, hC⟩

Premises used: SchwartzMap.eLpNorm_le_seminorm
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
inst_9 : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)),
    eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
      (↑C : ℝ≥0∞) *
        ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
⊢ ∃ (k : ℕ) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)),
        ‖f.toLp p μ‖ ≤
          HMul.hMul (β := ℝ) C
            ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
⟨k, C, C.coe_nonneg, fun f ↦ ?_⟩

Premises used: And.intro, NNReal.coe_nonneg, Exists.intro, NNReal.toReal
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
inst_9 : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)),
    eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
      (↑C : ℝ≥0∞) *
        ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
refine :
  ∀ (f : 𝓢(E, F)),
    ‖f.toLp p μ‖ ≤
      HMul.hMul (β := ℝ) (↑C : ℝ)
        ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ∃ (k : ℕ) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)),
        ‖f.toLp p μ‖ ≤
          HMul.hMul (β := ℝ) C
            ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
refine ⟨k, C, C.coe_nonneg, fun f ↦ ?_⟩
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
inst_9 : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)),
    eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
      (↑C : ℝ≥0∞) *
        ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
f : 𝓢(E, F)
rw :
  (eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ).toReal ≤
    HMul.hMul (β := ℝ) (↑C : ℝ)
      ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ‖f.toLp p μ‖ ≤
    HMul.hMul (β := ℝ) (↑C : ℝ)
      ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
rw [norm_toLp]

Premises used: SchwartzMap.norm_toLp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
inst_9 : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)),
    eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
      (↑C : ℝ≥0∞) *
        ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
f : 𝓢(E, F)
⊢ 0 ≤
    HMul.hMul (β := ℝ) (↑C : ℝ)
      ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
simp [mul_nonneg]

Premises used: mul_nonneg
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
inst_9 : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)),
    eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
      (↑C : ℝ≥0∞) *
        ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
f : 𝓢(E, F)
refine :
  eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
    ENNReal.ofReal
      (HMul.hMul (β := ℝ) (↑C : ℝ)
        ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ))
⊢ (eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ).toReal ≤
    HMul.hMul (β := ℝ) (↑C : ℝ)
      ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
refine ENNReal.toReal_le_of_le_ofReal (by simp [mul_nonneg]) ?_

Premises used: ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
inst_9 : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)),
    eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
      (↑C : ℝ≥0∞) *
        ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
f : 𝓢(E, F)
rw :
  eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
    ENNReal.ofReal (↑C : ℝ) *
      ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
⊢ eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
    ENNReal.ofReal
      (HMul.hMul (β := ℝ) (↑C : ℝ)
        ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ))

Tactic:
rw [ENNReal.ofReal_mul NNReal.zero_le_coe]

Premises used: ENNReal.ofReal_mul, NNReal.zero_le_coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
inst_9 : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)),
    eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
      (↑C : ℝ≥0∞) *
        ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
f : 𝓢(E, F)
⊢ eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
    ENNReal.ofReal (↑C : ℝ) *
      ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)

Tactic:
simpa using hC f