-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem MemLp.of_measure_le_smul {μ' : Measure α} {c : ℝ≥0∞} (hc : c ≠ ∞) (hμ'_le : μ' ≤ c • μ)
    {f : α → E} (hf : MemLp f p μ) : MemLp f p μ'

Proof state:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : MemLp f p μ
hc0 : c = 0
⊢ eLpNorm f p (c • μ) < ⊤

Tactic:
simp [hc0]

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : MemLp f p μ
hc0 : ¬c = 0
⊢ c ^ (1 / p).toReal * eLpNorm f p μ < ⊤

Tactic:
refine ENNReal.mul_lt_top (Ne.lt_top ?_) hf.2

Result:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : MemLp f p μ
hc0 : ¬c = 0
⊢ c ^ (1 / p).toReal ≠ ⊤

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : MemLp f p μ
⊢ MemLp f p μ'

Tactic:
refine ⟨hf.1.mono_ac (Measure.absolutelyContinuous_of_le_smul hμ'_le), ?_⟩

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : MemLp f p μ
⊢ eLpNorm f p μ' < ⊤

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : MemLp f p μ
⊢ eLpNorm f p μ' < ⊤

Tactic:
refine (eLpNorm_mono_measure f hμ'_le).trans_lt ?_

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : MemLp f p μ
⊢ eLpNorm f p (c • μ) < ⊤

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : MemLp f p μ
hc0 : ¬c = 0
⊢ eLpNorm f p (c • μ) < ⊤

Tactic:
rw [eLpNorm_smul_measure_of_ne_zero hc0, smul_eq_mul]

Result:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : MemLp f p μ
hc0 : ¬c = 0
⊢ c ^ (1 / p).toReal * eLpNorm f p μ < ⊤

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : MemLp f p μ
hc0 : ¬c = 0
⊢ c ^ (1 / p).toReal ≠ ⊤

Tactic:
simp [hc, hc0]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : MemLp f p μ
⊢ eLpNorm f p (c • μ) < ⊤

Tactic:
by_cases hc0 : c = 0

Result:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : MemLp f p μ
hc0 : c = 0
⊢ eLpNorm f p (c • μ) < ⊤

case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ⊤
hμ'_le : μ' ≤ c • μ
f : α → E
hf : MemLp f p μ
hc0 : ¬c = 0
⊢ eLpNorm f p (c • μ) < ⊤