have h1 := abs_real_inner_le_norm v1 v2
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
v2 : EuclideanSpace ℝ (Fin 2) := ![c, d]
h2 : a * c + b * d ≤ |a * c + b * d|
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
v2 : EuclideanSpace ℝ (Fin 2) := ![c, d]
h2 : a * c + b * d ≤ |a * c + b * d|
h1 : |⟪v1, v2⟫_ℝ| ≤ ‖v1‖ * ‖v2‖
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)