case h
V : Type ?u.279839
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.279848
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
f : V₁ →+ V₂
C : ℝ
h : ∀ (x : V₁), ‖↑f x‖ ≤ C * ‖x‖
x : V₁
⊢ C ≤ max C 0
V : Type ?u.279839
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.279848
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
f : V₁ →+ V₂
C : ℝ
h : ∀ (x : V₁), ‖↑f x‖ ≤ C * ‖x‖
x : V₁
⊢ C * ‖x‖ ≤ max C 0 * ‖x‖
gcongr
no goals
case h
V : Type ?u.279839
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.279848
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
f : V₁ →+ V₂
C : ℝ
h : ∀ (x : V₁), ‖↑f x‖ ≤ C * ‖x‖
x : V₁
⊢ C ≤ max C 0
apply le_max_left