-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem le_opNorm (x : V₁) : ‖f x‖ ≤ ‖f‖ * ‖x‖

Proof state:
case neg
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
h : ¬‖x‖ = 0
hlt : 0 < ‖x‖
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖

Tactic:
exact
  (div_le_iff₀ hlt).mp
    (le_csInf bounds_nonempty fun c ⟨_, hc⟩ => (div_le_iff₀ hlt).mpr <| by apply hc)

Result:
no goals

Proof state:
case intro.intro
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖

Tactic:
by_cases h : ‖x‖ = 0

Result:
case pos
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
h : ‖x‖ = 0
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖

case neg
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
h : ¬‖x‖ = 0
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖

Proof state:
case neg
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
h : ¬‖x‖ = 0
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖

Tactic:
have hlt : 0 < ‖x‖ := lt_of_le_of_ne (norm_nonneg x) (Ne.symm h)

Result:
case neg
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
h : ¬‖x‖ = 0
hlt : 0 < ‖x‖
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖

Tactic:
obtain ⟨C, _Cpos, hC⟩ := f.bound

Result:
case intro.intro
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖

Proof state:
case pos
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
h : ‖x‖ = 0
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖

Tactic:
rwa [h, mul_zero] at hC ⊢

Result:
no goals

Proof state:
case intro.intro
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖

Tactic:
replace hC := hC x

Result:
case intro.intro
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
⊢ ‖f x‖ ≤ ‖f‖ * ‖x‖

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
h : ¬‖x‖ = 0
hlt : 0 < ‖x‖
c : ℝ
x✝ : c ∈ {c | 0 ≤ c ∧ ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖}
left✝ : 0 ≤ c
hc : ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖
⊢ ‖f x‖ ≤ c * ‖x‖

Tactic:
apply hc

Result:
no goals