awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
rw : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * (‖x‖ * ‖y‖) + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
⊢ ‖x - y‖ = |‖x‖ - ‖y‖|

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg (x - y)) (abs_nonneg (‖x‖ - ‖y‖)), norm_sub_pow_two_real,
    inner_eq_mul_norm_of_angle_eq_zero h, sq_abs (‖x‖ - ‖y‖)]

Premises used: Norm.norm, norm_sub_pow_two_real, HSub.hSub, InnerProductGeometry.inner_eq_mul_norm_of_angle_eq_zero, sq_abs, sq_eq_sq₀, abs_nonneg, norm_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * (‖x‖ * ‖y‖) + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x - y‖ = ‖x‖ + ‖y‖ ↔ angle x y = π

Tactic:
⟨fun h => ?_, norm_sub_eq_add_norm_of_angle_eq_pi⟩

Premises used: InnerProductGeometry.norm_sub_eq_add_norm_of_angle_eq_pi, Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
refine : ∀ (h : ‖x - y‖ = ‖x‖ + ‖y‖), angle x y = π
⊢ ‖x - y‖ = ‖x‖ + ‖y‖ ↔ angle x y = π

Tactic:
refine ⟨fun h => ?_, norm_sub_eq_add_norm_of_angle_eq_pi⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = ‖x‖ + ‖y‖
rw : ⟪x, y⟫ = -(‖x‖ * ‖y‖)
⊢ angle x y = π

Tactic:
rw [← inner_eq_neg_mul_norm_iff_angle_eq_pi hx hy]

Premises used: InnerProductGeometry.inner_eq_neg_mul_norm_iff_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = ‖x‖ + ‖y‖
⊢ 0 ≤ ‖x - y‖

Tactic:
obtain ⟨hxy₁, hxy₂⟩ := norm_nonneg (x - y), add_nonneg (norm_nonneg x) (norm_nonneg y)

Premises used: HSub.hSub, add_nonneg, norm_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = ‖x‖ + ‖y‖
hxy₁ : 0 ≤ ‖x - y‖
⊢ 0 ≤ ‖x‖ + ‖y‖

Tactic:
obtain ⟨hxy₁, hxy₂⟩ := norm_nonneg (x - y), add_nonneg (norm_nonneg x) (norm_nonneg y)

Premises used: HSub.hSub, add_nonneg, norm_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = ‖x‖ + ‖y‖
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2

Tactic:
rw [← sq_eq_sq₀ hxy₁ hxy₂, norm_sub_pow_two_real] at h

Premises used: norm_sub_pow_two_real, sq_eq_sq₀
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = ‖x‖ + ‖y‖
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
h₁ : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
⊢ 0 ≤ ‖x - y‖

Tactic:
rw [← sq_eq_sq₀ hxy₁ hxy₂, norm_sub_pow_two_real] at h

Premises used: norm_sub_pow_two_real, sq_eq_sq₀
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = ‖x‖ + ‖y‖
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
h₁ : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
hxy₃ : 0 ≤ ‖x - y‖
⊢ 0 ≤ ‖x‖ + ‖y‖

Tactic:
rw [← sq_eq_sq₀ hxy₁ hxy₂, norm_sub_pow_two_real] at h

Premises used: norm_sub_pow_two_real, sq_eq_sq₀
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
linarith linarith₁ linarith₂ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₃ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 → 2 / 2 = 1
linarith₄ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 →
    GT.gt (α := ℝ) 2 0
linarith₆ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 →
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 +
        (2 * ⟪x, y⟫ -
          (1 * HPow.hPow (β := ℕ) (1 * ‖x‖) 2 + 1 * HPow.hPow (β := ℕ) (1 * ‖y‖) 2 -
            1 * HPow.hPow (β := ℕ) (1 * ‖x‖ + 1 * ‖y‖) 2)) =
      0
linarith₇ linarith₈ linarith₉ :
  (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 < ⟪x, y⟫ →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁₀ :
  (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 < ⟪x, y⟫ → 2 / 2 = 1
linarith₁₁ :
  (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 < ⟪x, y⟫ →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₂ :
  (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 < ⟪x, y⟫ →
    GT.gt (α := ℝ) 2 0
linarith₁₃ :
  (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 < ⟪x, y⟫ →
    -(HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) +
        (1 * HPow.hPow (β := ℕ) (1 * ‖x‖) 2 + 1 * HPow.hPow (β := ℕ) (1 * ‖y‖) 2 -
            1 * HPow.hPow (β := ℕ) (1 * ‖x‖ + 1 * ‖y‖) 2 -
          2 * ⟪x, y⟫) =
      0
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2

Tactic:
linarith
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 = -(‖x‖ * ‖y‖)

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
by : ⟪x, y⟫ = (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2
by₁ : (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2) / 2 = -(‖x‖ * ‖y‖)
⊢ ⟪x, y⟫ = -(‖x‖ * ‖y‖)

Tactic:
calc
    ⟪x, y⟫ = (‖x‖ ^ 2 + ‖y‖ ^ 2 - (‖x‖ + ‖y‖) ^ 2) / 2 := by linarith
    _ = -(‖x‖ * ‖y‖) := by ring

Premises used: Norm.norm, HMul.hMul, HSub.hSub, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ angle x y = 0

Tactic:
⟨?_, norm_add_eq_add_norm_of_angle_eq_zero⟩

Premises used: InnerProductGeometry.norm_add_eq_add_norm_of_angle_eq_zero, Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
refine : ‖x + y‖ = ‖x‖ + ‖y‖ → angle x y = 0
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ angle x y = 0

Tactic:
refine ⟨?_, norm_add_eq_add_norm_of_angle_eq_zero⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ → angle x y = 0

Tactic:
grind [inner_eq_mul_norm_iff_angle_eq_zero hx hy, norm_add_pow_two_real]

Premises used: norm_add_pow_two_real, InnerProductGeometry.inner_eq_mul_norm_iff_angle_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x - y‖ = |‖x‖ - ‖y‖| ↔ angle x y = 0

Tactic:
⟨fun h => ?_, norm_sub_eq_abs_sub_norm_of_angle_eq_zero⟩

Premises used: Iff.intro, InnerProductGeometry.norm_sub_eq_abs_sub_norm_of_angle_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
refine : ∀ (h : ‖x - y‖ = |‖x‖ - ‖y‖|), angle x y = 0
⊢ ‖x - y‖ = |‖x‖ - ‖y‖| ↔ angle x y = 0

Tactic:
refine ⟨fun h => ?_, norm_sub_eq_abs_sub_norm_of_angle_eq_zero⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
rw : ⟪x, y⟫ = ‖x‖ * ‖y‖
⊢ angle x y = 0

Tactic:
rw [← inner_eq_mul_norm_iff_angle_eq_zero hx hy]

Premises used: InnerProductGeometry.inner_eq_mul_norm_iff_angle_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
rw : HPow.hPow (β := ℕ) |‖x‖ - ‖y‖| 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
⊢ HPow.hPow (β := ℕ) ‖x - y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2

Tactic:
rw [h]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
⊢ HPow.hPow (β := ℕ) |‖x‖ - ‖y‖| 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2

Tactic:
sq_abs (‖x‖ - ‖y‖)

Premises used: Norm.norm, HSub.hSub, sq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
⊢ HPow.hPow (β := ℕ) |‖x‖ - ‖y‖| 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2

Tactic:
exact sq_abs (‖x‖ - ‖y‖)

Premises used: Norm.norm, HSub.hSub, sq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
⊢ HPow.hPow (β := ℕ) ‖x - y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2

Tactic:
have h1 : ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2 := by
    rw [h]
    exact sq_abs (‖x‖ - ‖y‖)
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x - y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2

Tactic:
rw [norm_sub_pow_two_real] at h1

Premises used: norm_sub_pow_two_real
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
linarith linarith₁ linarith₂ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₃ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 → 2 / 2 = 1
linarith₄ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    GT.gt (α := ℝ) 2 0
linarith₆ :
  ⟪x, y⟫ < (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 →
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2 +
        (2 * ⟪x, y⟫ -
          (1 * HPow.hPow (β := ℕ) (1 * ‖x‖ + 1 * ‖y‖) 2 - 1 * HPow.hPow (β := ℕ) (1 * ‖x‖) 2 -
            1 * HPow.hPow (β := ℕ) (1 * ‖y‖) 2)) =
      0
linarith₇ linarith₈ linarith₉ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁₀ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ → 2 / 2 = 1
linarith₁₁ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₂ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
    GT.gt (α := ℝ) 2 0
linarith₁₃ :
  (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 < ⟪x, y⟫ →
    -(HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2) +
        (1 * HPow.hPow (β := ℕ) (1 * ‖x‖ + 1 * ‖y‖) 2 - 1 * HPow.hPow (β := ℕ) (1 * ‖x‖) 2 -
            1 * HPow.hPow (β := ℕ) (1 * ‖y‖) 2 -
          2 * ⟪x, y⟫) =
      0
⊢ ⟪x, y⟫ = (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2

Tactic:
linarith
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
⊢ (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 = ‖x‖ * ‖y‖

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ - ‖y‖) 2
by : ⟪x, y⟫ = (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2
by₁ : (HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 - HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖y‖ 2) / 2 = ‖x‖ * ‖y‖
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖

Tactic:
calc
    ⟪x, y⟫ = ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2 := by linarith
    _ = ‖x‖ * ‖y‖ := by ring

Premises used: Norm.norm, HSub.hSub, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw :
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 ↔
    ⟪x, y⟫ = 0
⊢ ‖x + y‖ = ‖x - y‖ ↔ angle x y = π / 2

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg (x + y)) (norm_nonneg (x - y)),
    ← inner_eq_zero_iff_angle_eq_pi_div_two x y, norm_add_pow_two_real, norm_sub_pow_two_real]

Premises used: norm_add_pow_two_real, norm_sub_pow_two_real, HSub.hSub, HAdd.hAdd, sq_eq_sq₀, InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, norm_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
mp :
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
    ⟪x, y⟫ = 0
mpr :
  ⟪x, y⟫ = 0 →
    HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 ↔
    ⟪x, y⟫ = 0

Tactic:
constructor
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h :
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2
linarith :
  ⟪x, y⟫ < 0 →
    -(HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
            (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2)) +
        4 * (⟪x, y⟫ - 0) =
      0
linarith₁ : ⟪x, y⟫ < 0 → GT.gt (α := ℝ) 4 0
linarith₂ :
  0 < ⟪x, y⟫ →
    HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
          (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2) +
        4 * (0 - ⟪x, y⟫) =
      0
linarith₃ : 0 < ⟪x, y⟫ → GT.gt (α := ℝ) 4 0
⊢ ⟪x, y⟫ = 0

Tactic:
linarith
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
linarith :
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 <
      HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
    4 * -(⟪x, y⟫ - 0) +
        (HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
          (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2)) =
      0
linarith₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 <
      HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
    GT.gt (α := ℝ) 4 0
linarith₂ :
  HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 <
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
    4 * (⟪x, y⟫ - 0) +
        (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 -
          (HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2)) =
      0
linarith₃ :
  HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 <
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 →
    GT.gt (α := ℝ) 4 0
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫ + HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
linarith
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : cos (angle x y) = cos 0 ↔ angle x y = 0
⊢ cos (angle x y) = 1 ↔ angle x y = 0

Tactic:
rw [← cos_zero]

Premises used: Real.cos_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = cos 0 ↔ angle x y = 0

Tactic:
injOn_cos.eq_iff ⟨angle_nonneg x y, angle_le_pi x y⟩ (left_mem_Icc.2 pi_pos.le)

Premises used: Iff.mpr, Set.InjOn.eq_iff, InnerProductGeometry.angle_le_pi, Real.pi_pos, LT.lt.le, InnerProductGeometry.angle_nonneg, Set.left_mem_Icc, And.intro, Real.injOn_cos
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = cos 0 ↔ angle x y = 0

Tactic:
exact injOn_cos.eq_iff ⟨angle_nonneg x y, angle_le_pi x y⟩ (left_mem_Icc.2 pi_pos.le)

Premises used: Iff.mpr, Set.InjOn.eq_iff, InnerProductGeometry.angle_le_pi, Real.pi_pos, LT.lt.le, InnerProductGeometry.angle_nonneg, Set.left_mem_Icc, And.intro, Real.injOn_cos
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : cos (angle x y) = cos (π / 2) ↔ angle x y = π / 2
⊢ cos (angle x y) = 0 ↔ angle x y = π / 2

Tactic:
rw [← cos_pi_div_two]

Premises used: Real.cos_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
apply : π / 2 ∈ Icc 0 π
⊢ cos (angle x y) = cos (π / 2) ↔ angle x y = π / 2

Tactic:
apply injOn_cos.eq_iff ⟨angle_nonneg x y, angle_le_pi x y⟩

Premises used: Set.InjOn.eq_iff, InnerProductGeometry.angle_le_pi, InnerProductGeometry.angle_nonneg, And.intro, Real.injOn_cos
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
left : 0 ≤ π / 2
right : π / 2 ≤ π
⊢ π / 2 ∈ Icc 0 π

Tactic:
constructor
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
linarith : π / 2 < 0 → 2 / 2 = 1
linarith₁ : π / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 < 0 → 1 * π - HMul.hMul (α := ℝ) 2 0 + (0 - π) = 0
⊢ 0 ≤ π / 2

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
linarith : π < π / 2 → 2 / 2 = 1
linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < π / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : π < π / 2 → 2 * π - 1 * π + (0 - π) = 0
⊢ π / 2 ≤ π

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : cos (angle x y) = cos π ↔ angle x y = π
⊢ cos (angle x y) = -1 ↔ angle x y = π

Tactic:
rw [← cos_pi]

Premises used: Real.cos_pi
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = cos π ↔ angle x y = π

Tactic:
injOn_cos.eq_iff ⟨angle_nonneg x y, angle_le_pi x y⟩ (right_mem_Icc.2 pi_pos.le)

Premises used: Iff.mpr, Set.right_mem_Icc, Set.InjOn.eq_iff, InnerProductGeometry.angle_le_pi, Real.pi_pos, LT.lt.le, InnerProductGeometry.angle_nonneg, And.intro, Real.injOn_cos
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = cos π ↔ angle x y = π

Tactic:
exact injOn_cos.eq_iff ⟨angle_nonneg x y, angle_le_pi x y⟩ (right_mem_Icc.2 pi_pos.le)

Premises used: Iff.mpr, Set.right_mem_Icc, Set.InjOn.eq_iff, InnerProductGeometry.angle_le_pi, Real.pi_pos, LT.lt.le, InnerProductGeometry.angle_nonneg, And.intro, Real.injOn_cos
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : cos (angle x y) = 1 ∨ cos (angle x y) = -1 ↔ angle x y = 0 ∨ angle x y = π
rw₁ : angle x y = 0 ∨ cos (angle x y) = -1 ↔ angle x y = 0 ∨ angle x y = π
rw₂ rw₃ : angle x y = 0 ∨ angle x y = π ↔ angle x y = 0 ∨ angle x y = π
⊢ sin (angle x y) = 0 ↔ angle x y = 0 ∨ angle x y = π

Tactic:
rw [sin_eq_zero_iff_cos_eq, cos_eq_one_iff_angle_eq_zero, cos_eq_neg_one_iff_angle_eq_pi]

Premises used: Real.sin_eq_zero_iff_cos_eq, InnerProductGeometry.cos_eq_neg_one_iff_angle_eq_pi, InnerProductGeometry.cos_eq_one_iff_angle_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : angle x y = π / 2
rw : sin (π / 2) = 1
rw₁ rw₂ : Eq (α := ℝ) 1 1
⊢ sin (angle x y) = 1

Tactic:
rw [h, sin_pi_div_two]

Premises used: Real.sin_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
refine : ∀ (h : sin (angle x y) = 1), angle x y = π / 2
⊢ sin (angle x y) = 1 ↔ angle x y = π / 2

Tactic:
refine ⟨fun h => ?_, fun h => by rw [h, sin_pi_div_two]⟩