-- Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean
theorem norm_smulRight_apply (c : E →L[𝕜] 𝕜) (f : Fₗ) : ‖smulRight c f‖ = ‖c‖ * ‖f‖

Proof state:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
⊢ ‖c.smulRight f‖ = ‖c‖ * ‖f‖

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
⊢ ‖c.smulRight f‖ ≤ ‖c‖ * ‖f‖

case refine_2
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
⊢ ‖c‖ * ‖f‖ ≤ ‖c.smulRight f‖

Proof state:
case refine_2.inr
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
hf : 0 < ‖f‖
x : E
⊢ ‖c x‖ ≤ ‖c.smulRight f‖ / ‖f‖ * ‖x‖

Tactic:
rw [div_mul_eq_mul_div, le_div_iff₀ hf]

Result:
case refine_2.inr
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
hf : 0 < ‖f‖
x : E
⊢ ‖c x‖ * ‖f‖ ≤ ‖c.smulRight f‖ * ‖x‖

Proof state:
case refine_2.inr
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
hf : 0 < ‖f‖
⊢ ‖c‖ * ‖f‖ ≤ ‖c.smulRight f‖

Tactic:
rw [← le_div_iff₀ hf]

Result:
case refine_2.inr
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
hf : 0 < ‖f‖
⊢ ‖c‖ ≤ ‖c.smulRight f‖ / ‖f‖

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
⊢ ‖c.smulRight f‖ ≤ ‖c‖ * ‖f‖

Tactic:
refine opNorm_le_bound _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) fun x => ?_

Result:
case refine_1
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
x : E
⊢ ‖(c.smulRight f) x‖ ≤ ‖c‖ * ‖f‖ * ‖x‖

Proof state:
case refine_2.inr
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
hf : 0 < ‖f‖
⊢ ‖c‖ ≤ ‖c.smulRight f‖ / ‖f‖

Tactic:
refine opNorm_le_bound _ (div_nonneg (norm_nonneg _) (norm_nonneg f)) fun x => ?_

Result:
case refine_2.inr
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
hf : 0 < ‖f‖
x : E
⊢ ‖c x‖ ≤ ‖c.smulRight f‖ / ‖f‖ * ‖x‖

Proof state:
case refine_2.inr
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
hf : 0 < ‖f‖
x : E
⊢ ‖c x‖ * ‖f‖ ≤ ‖c.smulRight f‖ * ‖x‖

Tactic:
calc
  ‖c x‖ * ‖f‖ = ‖c x • f‖ := (norm_smul _ _).symm
  _ = ‖smulRight c f x‖ := rfl
  _ ≤ ‖smulRight c f‖ * ‖x‖ := le_opNorm _ _

Result:
no goals

Proof state:
case refine_2.inl
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
hf : ‖f‖ = 0
⊢ ‖c‖ * ‖f‖ ≤ ‖c.smulRight f‖

Tactic:
simp [hf]

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
⊢ ‖c‖ * ‖f‖ ≤ ‖c.smulRight f‖

Tactic:
obtain hf | hf := (norm_nonneg f).eq_or_gt

Result:
case refine_2.inl
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
hf : ‖f‖ = 0
⊢ ‖c‖ * ‖f‖ ≤ ‖c.smulRight f‖

case refine_2.inr
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
hf : 0 < ‖f‖
⊢ ‖c‖ * ‖f‖ ≤ ‖c.smulRight f‖

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
x : E
⊢ ‖(c.smulRight f) x‖ ≤ ‖c‖ * ‖f‖ * ‖x‖

Tactic:
calc
  ‖c x • f‖ = ‖c x‖ * ‖f‖ := norm_smul _ _
  _ ≤ ‖c‖ * ‖x‖ * ‖f‖ := mul_le_mul_of_nonneg_right (le_opNorm _ _) (norm_nonneg _)
  _ = ‖c‖ * ‖f‖ * ‖x‖ := by ring

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : E →L[𝕜] 𝕜
f : Fₗ
x : E
⊢ ‖c‖ * ‖x‖ * ‖f‖ = ‖c‖ * ‖f‖ * ‖x‖

Tactic:
ring

Result:
no goals