Theorem: Usa2001P4.lemma1 (Compfiles/Usa2001P4.lean)

State before:
a b c d : ℝ
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Tactic:
let v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
State after:
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)

State before:
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Tactic:
let v2 : EuclideanSpace ℝ (Fin 2) := ![c, d]
State after:
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
v2 : EuclideanSpace ℝ (Fin 2) := ![c, d]
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)

State before:
a b c d : ℝ
v1 : EuclideanSpace ℝ (Fin 2) := ![a, b]
v2 : EuclideanSpace ℝ (Fin 2) := ![c, d]
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Tactic:
have h2 : a * c + b * d ≤ |a * c + b * d| := le_abs_self _
State after:
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)

State before:
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)
Tactic:
have h1 := abs_real_inner_le_norm v1 v2
State after:
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)

State before:
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)
Tactic:
simp [EuclideanSpace.norm_eq] at h1
State after:
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 0 * v2 0 + v1 1 * v2 1| ≤ √(v1 0 ^ 2 + v1 1 ^ 2) * √(v2 0 ^ 2 + v2 1 ^ 2)
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)

State before:
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 0 * v2 0 + v1 1 * v2 1| ≤ √(v1 0 ^ 2 + v1 1 ^ 2) * √(v2 0 ^ 2 + v2 1 ^ 2)
⊢ a * c + b * d ≤ √(a ^ 2 + b ^ 2) * √(c ^ 2 + d ^ 2)
Tactic:
exact h2.trans h1
State after:
no goals