case intro.intro
V : Type ?u.224218
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.224227
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ∀ (x : V₁), ‖↑f x‖ ≤ C * ‖x‖
⊢ ‖↑f x‖ ≤ ‖f‖ * ‖x‖
V : Type ?u.224218
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.224227
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x : V₁
⊢ ‖↑f x‖ ≤ ‖f‖ * ‖x‖
obtain ⟨C, _Cpos, hC⟩ := f.bound
case intro.intro
V : Type ?u.224218
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.224227
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖↑f x‖ ≤ C * ‖x‖
⊢ ‖↑f x‖ ≤ ‖f‖ * ‖x‖
case intro.intro
V : Type ?u.224218
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.224227
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ∀ (x : V₁), ‖↑f x‖ ≤ C * ‖x‖
⊢ ‖↑f x‖ ≤ ‖f‖ * ‖x‖
replace hC := hC x
case pos
V : Type ?u.224218
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.224227
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : 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.224218
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.224227
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖↑f x‖ ≤ C * ‖x‖
h : ¬‖x‖ = 0
⊢ ‖↑f x‖ ≤ ‖f‖ * ‖x‖
case intro.intro
V : Type ?u.224218
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.224227
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖↑f x‖ ≤ C * ‖x‖
⊢ ‖↑f x‖ ≤ ‖f‖ * ‖x‖
by_cases h : ‖x‖ = 0
case neg
V : Type ?u.224218
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.224227
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖↑f x‖ ≤ C * ‖x‖
h : ¬‖x‖ = 0
hlt : 0 < ‖x‖
⊢ ‖↑f x‖ ≤ ‖f‖ * ‖x‖
case neg
V : Type ?u.224218
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.224227
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖↑f x‖ ≤ C * ‖x‖
h : ¬‖x‖ = 0
⊢ ‖↑f x‖ ≤ ‖f‖ * ‖x‖
have hlt : 0 < ‖x‖ := lt_of_le_of_ne (norm_nonneg x) (Ne.symm h)
no goals
case neg
V : Type ?u.224218
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.224227
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖↑f x‖ ≤ C * ‖x‖
h : ¬‖x‖ = 0
hlt : 0 < ‖x‖
⊢ ‖↑f x‖ ≤ ‖f‖ * ‖x‖
exact
  (div_le_iff hlt).mp
    (le_csInf bounds_nonempty fun c ⟨_, hc⟩ => (div_le_iff hlt).mpr <| by apply hc)
no goals
case pos
V : Type ?u.224218
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.224227
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖↑f x‖ ≤ C * ‖x‖
h : ‖x‖ = 0
⊢ ‖↑f x‖ ≤ ‖f‖ * ‖x‖
rwa [h, mul_zero] at hC⊢
no goals
V : Type ?u.224218
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.224227
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : 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‖
apply hc