awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
    (↑((eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ).toNNReal *
            HPow.hPow (α := ℝ≥0) 2 k) :
        ℝ≥0∞) *
      ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
have calc : eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ =
  eLpNorm
    (HSMul.hSMul (α := (x : E) → ℝ) (β := (x : E) → F) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ)))
      fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F))
    p μ
Tactic: calc eLpNorm (⇑f) p μ
  _ = eLpNorm ((fun x : E ↦ (1 + ‖x‖) ^ (-k : ℝ)) • fun x ↦ (1 + ‖x‖) ^ k • f x) p μ := by
    refine congrArg (eLpNorm · p μ) (funext fun x ↦ ?_)
    simp [(h_one_add x).ne']
  _ ≤ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ * eLpNorm (fun x ↦ (1 + ‖x‖) ^ k • f x) ⊤ μ := by
    refine eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top p _ ?_
    refine Continuous.aestronglyMeasurable ?_
    exact .rpow_const (by fun_prop) fun x ↦ .inl (h_one_add x).ne'
  _ ≤ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)) := by
    gcongr
    refine eLpNormEssSup_le_of_ae_nnnorm_bound (ae_of_all μ fun x ↦ ?_)
    rw [← norm_toNNReal, Real.toNNReal_le_iff_le_coe]
    simpa [norm_smul, abs_of_nonneg (h_one_add x).le] using
      one_add_le_sup_seminorm_apply (m := (k, 0)) (le_refl k) (le_refl 0) f x
  _ = _ := by
    rw [ENNReal.coe_mul, ENNReal.coe_toNNReal hk.ne]
    simp only [ENNReal.coe_pow, ENNReal.coe_ofNat]
    ring
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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‖
calc :
  eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ =
    eLpNorm
      (HSMul.hSMul (α := (x : E) → ℝ) (β := (x : E) → F) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ)))
        fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F))
      p μ
⊢ eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
    (↑((eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ).toNNReal *
            HPow.hPow (α := ℝ≥0) 2 k) :
        ℝ≥0∞) *
      ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
have calc₁ : eLpNorm
    (HSMul.hSMul (α := (x : E) → ℝ) (β := (x : E) → F) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ)))
      fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F))
    p μ ≤
  eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ *
    eLpNorm.{u_5, u_6} (ε := F) (fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F)) ∞ μ
Tactic: calc eLpNorm (⇑f) p μ
  _ = eLpNorm ((fun x : E ↦ (1 + ‖x‖) ^ (-k : ℝ)) • fun x ↦ (1 + ‖x‖) ^ k • f x) p μ := by
    refine congrArg (eLpNorm · p μ) (funext fun x ↦ ?_)
    simp [(h_one_add x).ne']
  _ ≤ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ * eLpNorm (fun x ↦ (1 + ‖x‖) ^ k • f x) ⊤ μ := by
    refine eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top p _ ?_
    refine Continuous.aestronglyMeasurable ?_
    exact .rpow_const (by fun_prop) fun x ↦ .inl (h_one_add x).ne'
  _ ≤ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)) := by
    gcongr
    refine eLpNormEssSup_le_of_ae_nnnorm_bound (ae_of_all μ fun x ↦ ?_)
    rw [← norm_toNNReal, Real.toNNReal_le_iff_le_coe]
    simpa [norm_smul, abs_of_nonneg (h_one_add x).le] using
      one_add_le_sup_seminorm_apply (m := (k, 0)) (le_refl k) (le_refl 0) f x
  _ = _ := by
    rw [ENNReal.coe_mul, ENNReal.coe_toNNReal hk.ne]
    simp only [ENNReal.coe_pow, ENNReal.coe_ofNat]
    ring
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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‖
calc :
  eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ =
    eLpNorm
      (HSMul.hSMul (α := (x : E) → ℝ) (β := (x : E) → F) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ)))
        fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F))
      p μ
calc₁ :
  eLpNorm
      (HSMul.hSMul (α := (x : E) → ℝ) (β := (x : E) → F) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ)))
        fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F))
      p μ ≤
    eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ *
      eLpNorm.{u_5, u_6} (ε := F) (fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F)) ∞ μ
⊢ eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
    (↑((eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ).toNNReal *
            HPow.hPow (α := ℝ≥0) 2 k) :
        ℝ≥0∞) *
      ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
have calc₂ : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ *
    eLpNorm.{u_5, u_6} (ε := F) (fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : 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: calc eLpNorm (⇑f) p μ
  _ = eLpNorm ((fun x : E ↦ (1 + ‖x‖) ^ (-k : ℝ)) • fun x ↦ (1 + ‖x‖) ^ k • f x) p μ := by
    refine congrArg (eLpNorm · p μ) (funext fun x ↦ ?_)
    simp [(h_one_add x).ne']
  _ ≤ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ * eLpNorm (fun x ↦ (1 + ‖x‖) ^ k • f x) ⊤ μ := by
    refine eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top p _ ?_
    refine Continuous.aestronglyMeasurable ?_
    exact .rpow_const (by fun_prop) fun x ↦ .inl (h_one_add x).ne'
  _ ≤ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)) := by
    gcongr
    refine eLpNormEssSup_le_of_ae_nnnorm_bound (ae_of_all μ fun x ↦ ?_)
    rw [← norm_toNNReal, Real.toNNReal_le_iff_le_coe]
    simpa [norm_smul, abs_of_nonneg (h_one_add x).le] using
      one_add_le_sup_seminorm_apply (m := (k, 0)) (le_refl k) (le_refl 0) f x
  _ = _ := by
    rw [ENNReal.coe_mul, ENNReal.coe_toNNReal hk.ne]
    simp only [ENNReal.coe_pow, ENNReal.coe_ofNat]
    ring
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
⊢ eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ < ∞
have 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 μ < ∞
Tactic: rcases eLpNorm_le_seminorm ℝ F p μ with ⟨k, C, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
⊢ MemLp.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) ∞ μ
have 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) ∞ μ
Tactic: rcases f.decay 0 0 with ⟨C, _, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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) ∞ μ
have refine : ∀ (x : E), norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ C
Tactic: refine memLp_top_of_bound f.continuous.aestronglyMeasurable C (ae_of_all μ fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 μ‖ = (eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ).toReal
have rw : (eLpNorm (↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) p μ).toReal =
  (eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ).toReal
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae (coeFn_toLp f p μ)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
⊢ ‖f.toLp p μ‖ = (eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ).toReal
have 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
Tactic: rw [Lp.norm_def, eLpNorm_congr_ae (coeFn_toLp f p μ)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
⊢ ‖f.toLp p μ‖ = HPow.hPow (α := ℝ) (∫ (x : E), norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ^ p.toReal ∂μ) p.toReal⁻¹
have 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⁻¹
Tactic: rw [norm_toLp, MeasureTheory.MemLp.eLpNorm_eq_integral_rpow_norm hp₁ hp₂ (f.memLp p μ),
    ENNReal.toReal_ofReal (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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⁻¹
⊢ ‖f.toLp p μ‖ = HPow.hPow (α := ℝ) (∫ (x : E), norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ^ p.toReal ∂μ) p.toReal⁻¹
have 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⁻¹
Tactic: rw [norm_toLp, MeasureTheory.MemLp.eLpNorm_eq_integral_rpow_norm hp₁ hp₂ (f.memLp p μ),
    ENNReal.toReal_ofReal (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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⁻¹
⊢ ‖f.toLp p μ‖ = HPow.hPow (α := ℝ) (∫ (x : E), norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ^ p.toReal ∂μ) p.toReal⁻¹
have 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⁻¹
Tactic: rw [norm_toLp, MeasureTheory.MemLp.eLpNorm_eq_integral_rpow_norm hp₁ hp₂ (f.memLp p μ),
    ENNReal.toReal_ofReal (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 ∞ μ)) (f.toLp ∞ μ) ≤ (SchwartzMap.seminorm ℝ 0 0 : (a : 𝓢(E, F)) → ℝ) f
have rw : eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) ∞ μ ≤ ENNReal.ofReal ((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]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 ≤ C ∧
      ∀ (f : 𝓢(E, F)),
        ‖f.toLp p μ‖ ≤
          HMul.hMul (β := ℝ) C
            ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have 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 : ℝ)
Tactic: rcases eLpNorm_le_seminorm 𝕜 F p μ with ⟨k, C, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 : ℝ)
have refine : ∀ (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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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)
⊢ ‖f.toLp p μ‖ ≤
    HMul.hMul (β := ℝ) (↑C : ℝ)
      ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have 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 : ℝ)
Tactic: rw [norm_toLp]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 μ).toReal ≤
    HMul.hMul (β := ℝ) (↑C : ℝ)
      ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have 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 : ℝ))
Tactic: refine ENNReal.toReal_le_of_le_ofReal (by simp [mul_nonneg]) ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
      (HMul.hMul (β := ℝ) (↑C : ℝ)
        ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ))
have 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)
Tactic: rw [ENNReal.ofReal_mul NNReal.zero_le_coe]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : MeasurableSpace D
inst_6 : MeasurableSpace E
inst_7 : OpensMeasurableSpace E
inst_8 : NormedField 𝕜
inst_9 : NormedSpace 𝕜 F
inst_10 : SMulCommClass ℝ 𝕜 F
inst_11 : SecondCountableTopologyEither E F
p : ℝ≥0∞
inst_12 : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)),
        norm (E := ↥(Lp F p μ)) ((fun (f : 𝓢(E, F)) ↦ f.toLp p μ) f) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have rcases : ∀ (k : ℕ) (C : ℝ) (hC_pos : 0 ≤ C)
  (hC :
    ∀ (f : 𝓢(E, F)),
      ‖f.toLp p μ‖ ≤
        HMul.hMul (β := ℝ) C
          ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)),
  ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)),
        norm (E := ↥(Lp F p μ)) ((fun (f : 𝓢(E, F)) ↦ f.toLp p μ) f) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: rcases norm_toLp_le_seminorm 𝕜 F p μ with ⟨k, C, hC_pos, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
inst_7 : FiniteDimensional ℝ E
inst_8 : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_9 : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
⊢ Membership.mem (γ := Set ↥(Lp F p μ))
    (closure (Set.range (ι := 𝓢(E, F)) (⇑(toLpCLM ℝ F p μ) : (a : 𝓢(E, F)) → ↥(Lp F p μ)))) f
have refine : ∀ (ε : ℝ) (hε : 0 < ε),
  ∃ (y : ↥(Lp F p μ)),
    Membership.mem (γ := Set ↥(Lp F p μ)) (Set.range (ι := 𝓢(E, F)) (⇑(toLpCLM ℝ F p μ) : (a : 𝓢(E, F)) → ↥(Lp F p μ)))
        y ∧
      y ∈ Metric.closedBall f ε
Tactic: refine (mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall).2 fun ε hε ↦ ?_