-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem opNorm_le_of_unit_norm [NormedSpace ℝ E] [NormedSpace ℝ F] {f : E →L[ℝ] F} {C : ℝ}
    (hC : 0 ≤ C) (hf : ∀ x, ‖x‖ = 1 → ‖f x‖ ≤ C) : ‖f‖ ≤ C

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
⊢ ‖f x‖ ≤ C * ‖x‖

Tactic:
have H₁ : ‖‖x‖⁻¹ • x‖ = 1 := by rw [norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hx]

Result:
E : Type u_4
F : Type u_5
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖‖x‖⁻¹ • x‖ = 1
⊢ ‖f x‖ ≤ C * ‖x‖

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖‖x‖⁻¹ • x‖ = 1
⊢ ‖f x‖ ≤ C * ‖x‖

Tactic:
have H₂ := hf _ H₁

Result:
E : Type u_4
F : Type u_5
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖‖x‖⁻¹ • x‖ = 1
H₂ : ‖f (‖x‖⁻¹ • x)‖ ≤ C
⊢ ‖f x‖ ≤ C * ‖x‖

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖‖x‖⁻¹ • x‖ = 1
H₂ : ‖f (‖x‖⁻¹ • x)‖ ≤ C
⊢ ‖f x‖ ≤ C * ‖x‖

Tactic:
rwa [map_smul, norm_smul, norm_inv, norm_norm, ← div_eq_inv_mul, div_le_iff₀] at H₂

Result:
E : Type u_4
F : Type u_5
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖‖x‖⁻¹ • x‖ = 1
H₂ : ‖f x‖ / ‖x‖ ≤ C
⊢ 0 < ‖x‖

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖‖x‖⁻¹ • x‖ = 1
H₂ : ‖f x‖ / ‖x‖ ≤ C
⊢ 0 < ‖x‖

Tactic:
exact (norm_nonneg x).lt_of_ne' hx

Result:
no goals

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
⊢ ‖‖x‖⁻¹ • x‖ = 1

Tactic:
rw [norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hx]

Result:
no goals

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
refine opNorm_le_bound' f hC fun x hx => ?_

Result:
E : Type u_4
F : Type u_5
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
⊢ ‖f x‖ ≤ C * ‖x‖