inner product equal -1 iff vectors are opposite

Stream: new members

[Ilmārs Cīrulis]

Is there a shorter way to prove/golf this result? I want to put in Mathlib.Analysis.InnerProductSpace.Basic right after inner_eq_one_iff_of_norm_one.

import Mathlib.Analysis.InnerProductSpace.Basic

variable {𝕜 E : Type*}
variable [RCLike 𝕜]
variable [NormedAddCommGroup E]
variable [InnerProductSpace 𝕜 E]

/-- If the inner product of two unit vectors is `-1`, then the two vectors are opposite. -/
theorem inner_eq_neg_one_iff_of_norm_one {x y : E} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) :
    inner 𝕜 x y = -1 ↔ x = -y := by
  have H := inner_eq_one_iff_of_norm_one (𝕜 := 𝕜) (x := x) (y := -y)
  simp only [norm_neg, inner_neg_right] at H
  rw [← H hx hy]
  constructor <;> intros H0
  · rw [H0]; simp
  · rw [← H0]; simp

[Aaron Liu]

#mwe?

[Ilmārs Cīrulis]

Fixed

[Ilmārs Cīrulis]

Ok, this is a bit shorter

import Mathlib.Analysis.InnerProductSpace.Basic

variable {𝕜 E : Type*}
variable [RCLike 𝕜]
variable [NormedAddCommGroup E]
variable [InnerProductSpace 𝕜 E]

/-- If the inner product of two unit vectors is `-1`, then the two vectors are opposite. -/
theorem inner_eq_neg_one_iff_of_norm_one {x y : E} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) :
    inner 𝕜 x y = -1 ↔ x = -y := by
  have H := inner_eq_one_iff_of_norm_one (𝕜 := 𝕜) (x := x) (y := -y)
  simp only [norm_neg, inner_neg_right] at H
  rw [← H hx hy, neg_eq_iff_eq_neg]

[Aaron Liu]

import Mathlib.Analysis.InnerProductSpace.Basic

variable {𝕜 E : Type*}
variable [RCLike 𝕜]
variable [NormedAddCommGroup E]
variable [InnerProductSpace 𝕜 E]

/-- If the inner product of two unit vectors is `-1`, then the two vectors are opposite. -/
theorem inner_eq_neg_one_iff_of_norm_one {x y : E} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) :
    inner 𝕜 x y = -1 ↔ x = -y := by
  simpa [neg_eq_iff_eq_neg] using
    inner_eq_one_iff_of_norm_one (𝕜 := 𝕜) hx (show ‖-y‖ = 1 by simpa using hy)