-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem norm_le_mul_norm_of_ae_le_mul {c : ℝ} {f : Lp E p μ} {g : Lp F p μ}
    (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ c * ‖g x‖) : ‖f‖ ≤ c * ‖g‖

Proof state:
case inr
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : c < 0
this : eLpNorm (↑↑f) p μ = 0 ∧ eLpNorm (↑↑g) p μ = 0
⊢ (eLpNorm (↑↑f) p μ).toReal ≤ c * (eLpNorm (↑↑g) p μ).toReal

Tactic:
simp [this]

Result:
no goals

Proof state:
case inl
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : 0 ≤ c
⊢ ‖f‖ ≤ c * ‖g‖

Tactic:
lift c to ℝ≥0 using hc

Result:
case inl.intro
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑c * ‖↑↑g x‖
⊢ ‖f‖ ≤ ↑c * ‖g‖

Proof state:
case inl.intro
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑c * ‖↑↑g x‖
⊢ ‖f‖ ≤ ↑c * ‖g‖

Tactic:
exact NNReal.coe_le_coe.mpr (nnnorm_le_mul_nnnorm_of_ae_le_mul h)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
⊢ ‖f‖ ≤ c * ‖g‖

Tactic:
rcases le_or_lt 0 c with hc | hc

Result:
case inl
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : 0 ≤ c
⊢ ‖f‖ ≤ c * ‖g‖

case inr
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : c < 0
⊢ ‖f‖ ≤ c * ‖g‖

Proof state:
case inr
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : c < 0
⊢ (eLpNorm (↑↑f) p μ).toReal ≤ c * (eLpNorm (↑↑g) p μ).toReal

Tactic:
have := eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg h hc p

Result:
case inr
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : c < 0
this : eLpNorm (↑↑f) p μ = 0 ∧ eLpNorm (↑↑g) p μ = 0
⊢ (eLpNorm (↑↑f) p μ).toReal ≤ c * (eLpNorm (↑↑g) p μ).toReal

Proof state:
case inr
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : c < 0
⊢ ‖f‖ ≤ c * ‖g‖

Tactic:
simp only [norm_def]

Result:
case inr
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
c : ℝ
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖
hc : c < 0
⊢ (eLpNorm (↑↑f) p μ).toReal ≤ c * (eLpNorm (↑↑g) p μ).toReal