no goals
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
C : ℝ
Cpos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
x✝ : E × F
x : E
y : F
⊢ ‖f (x, y)‖ ≤ ?m.295592 h C Cpos hC * ‖‖(x, y).fst‖ * ‖(x, y).snd‖‖
simpa [mul_assoc] using hC x y