-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_const_smul_le (hp : p ≠ 0) (c : 𝕜) (f : lp E p) : ‖c • f‖ ≤ ‖c‖ * ‖f‖

Proof state:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
rcases p.trichotomy with (rfl | rfl | hp)

Result:
case inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
c : 𝕜
hp : 0 ≠ 0
f : ↥(lp E 0)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

case inr.inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : ↥(lp E ⊤)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Proof state:
case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p) := { nnnorm := fun f => ⟨‖f‖, ⋯⟩ }
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
⊢ ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal

Tactic:
clear_value inst

Result:
case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
⊢ ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal

Proof state:
case inr.inl.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : ↥(lp E ⊤)
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
have hfc := (lp.isLUB_norm f).mul_left (norm_nonneg c)

Result:
case inr.inl.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : ↥(lp E ⊤)
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB ((fun b => ‖c‖ * b) '' Set.range fun i => ‖↑f i‖) (‖c‖ * ‖f‖)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Proof state:
case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
⊢ ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal

Tactic:
have hLHS := lp.hasSum_norm hp (c • f)

Result:
case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
hLHS : HasSum (fun i => ‖↑(c • f) i‖ ^ p.toReal) (‖c • f‖ ^ p.toReal)
⊢ ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal

Proof state:
case inr.inl.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : ↥(lp E ⊤)
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB (Set.range fun x => ‖c‖ * ‖↑f x‖) (‖c‖ * ‖f‖)
this : ∀ (a : α), ‖c‖ * ‖↑f a‖ ≤ ‖c‖ * ‖f‖
a : α
⊢ ‖↑(c • f) a‖ ≤ ‖c‖ * ‖f‖

Tactic:
exact (norm_smul_le _ _).trans (this a)

Result:
no goals

Proof state:
case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
hRHS : HasSum (fun a => ‖c‖₊ ^ p.toReal * ‖↑f a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
hLHS : HasSum (fun a => ‖↑(c • f) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)
⊢ ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal

Tactic:
refine hasSum_mono hLHS hRHS fun i => ?_

Result:
case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
hRHS : HasSum (fun a => ‖c‖₊ ^ p.toReal * ‖↑f a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
hLHS : HasSum (fun a => ‖↑(c • f) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)
i : α
⊢ ‖↑(c • f) i‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖↑f i‖₊ ^ p.toReal

Proof state:
case inr.inl.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : ↥(lp E ⊤)
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB ((fun b => ‖c‖ * b) '' Set.range fun i => ‖↑f i‖) (‖c‖ * ‖f‖)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
simp_rw [← Set.range_comp, Function.comp_def] at hfc

Result:
case inr.inl.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : ↥(lp E ⊤)
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB (Set.range fun x => ‖c‖ * ‖↑f x‖) (‖c‖ * ‖f‖)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Proof state:
case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p) := { nnnorm := fun f => ⟨‖f‖, ⋯⟩ }
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
suffices ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal by
  rwa [NNReal.rpow_le_rpow_iff hp] at this

Result:
case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p) := { nnnorm := fun f => ⟨‖f‖, ⋯⟩ }
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
⊢ ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal