-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem norm_toLp_le_seminorm (p : ℝ≥0∞) (μ : Measure E

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : SMulCommClass ℝ 𝕜 F
inst✝ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
f : 𝓢(E, F)
⊢ eLpNorm (⇑f) p μ ≤ ENNReal.ofReal ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Tactic:
simpa using hC f

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : SMulCommClass ℝ 𝕜 F
inst✝ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
⊢ ∃ k C, 0 ≤ C ∧ ∀ (f : 𝓢(E, F)), ‖f.toLp p μ‖ ≤ C * ((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f

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

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : SMulCommClass ℝ 𝕜 F
inst✝ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
⊢ ∃ k C, 0 ≤ C ∧ ∀ (f : 𝓢(E, F)), ‖f.toLp p μ‖ ≤ C * ((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : SMulCommClass ℝ 𝕜 F
inst✝ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
f : 𝓢(E, F)
⊢ 0 ≤ ↑C * ((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f

Tactic:
simp [mul_nonneg]

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : SMulCommClass ℝ 𝕜 F
inst✝ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
f : 𝓢(E, F)
⊢ (eLpNorm (⇑f) p μ).toReal ≤ ↑C * ((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f

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

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : SMulCommClass ℝ 𝕜 F
inst✝ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
f : 𝓢(E, F)
⊢ eLpNorm (⇑f) p μ ≤ ENNReal.ofReal (↑C * ((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : SMulCommClass ℝ 𝕜 F
inst✝ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
⊢ ∃ k C, 0 ≤ C ∧ ∀ (f : 𝓢(E, F)), ‖f.toLp p μ‖ ≤ C * ((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f

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

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : SMulCommClass ℝ 𝕜 F
inst✝ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
f : 𝓢(E, F)
⊢ ‖f.toLp p μ‖ ≤ ↑C * ((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : SMulCommClass ℝ 𝕜 F
inst✝ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
f : 𝓢(E, F)
⊢ ‖f.toLp p μ‖ ≤ ↑C * ((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f

Tactic:
rw [norm_toLp]

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : SMulCommClass ℝ 𝕜 F
inst✝ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
f : 𝓢(E, F)
⊢ (eLpNorm (⇑f) p μ).toReal ≤ ↑C * ((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f