awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
hx₁ : |⟪y, x⟫| = 1
hy₁ : ‖y‖ = 1
h₃ : ¬x = y
⊢ ¬x = -y

Tactic:
rw [H2, norm_smul, hy, Real.norm_eq_abs, mul_one] at hx

Premises used: norm_smul, mul_one, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
hx₁ : |⟪y, x⟫| = 1
hy₁ : ‖y‖ = 1
h₃ : ¬x = y
h₄ : ¬x = -y
⊢ x = ⟪y, x⟫ • y

Tactic:
rw [H2, norm_smul, hy, Real.norm_eq_abs, mul_one] at hx

Premises used: norm_smul, mul_one, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
hx : ⟪y, x⟫ = 1 ∨ ⟪y, x⟫ = -1
inl : ∀ (hx : ⟪y, x⟫ = 1), False
inr : ∀ (hx : ⟪y, x⟫ = -1), False
⊢ False

Tactic:
rcases hx with hx | hx
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
hx : ⟪y, x⟫ = 1
⊢ False

Tactic:
simp [*] at H2
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
hx : ⟪y, x⟫ = -1
⊢ False

Tactic:
simp [*] at H2
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
⊢ ‖x - ⟪y, x⟫ • y‖ ≠ 0

Tactic:
have H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0 := by
    simp only [ne_eq, norm_eq_zero, sub_eq_zero]
    intro H2
    rw [H2, norm_smul, hy, Real.norm_eq_abs, mul_one] at hx
    apply eq_or_eq_neg_of_abs_eq at hx
    rcases hx with hx | hx <;> simp [*] at H2
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
rw :
  HPow.hPow (β := ℕ) (1 - ⟪x, y⟫ * ⟪x, y⟫) 2 +
      (HPow.hPow (α := ℝ) (β := ℕ) 1 2 - ⟪x, y⟫ * ⟪x, y⟫ -
          (⟪x, y⟫ * ⟪x, y⟫ - ⟪x, y⟫ * (⟪x, y⟫ * HPow.hPow (α := ℝ) (β := ℕ) 1 2))) *
        HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) 1 2 - ⟪x, y⟫ * ⟪x, y⟫ -
      (⟪x, y⟫ * ⟪x, y⟫ - ⟪x, y⟫ * (⟪x, y⟫ * HPow.hPow (α := ℝ) (β := ℕ) 1 2))
⊢ HPow.hPow (β := ℕ) (1 - ⟪y, x⟫ * ⟪x, y⟫) 2 + HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2 * HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
    HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2

Tactic:
rw [← real_inner_self_eq_norm_sq, inner_sub_left, inner_sub_right, inner_sub_right,
    real_inner_smul_right, real_inner_smul_left, real_inner_smul_right, real_inner_smul_left,
    real_inner_comm x y, real_inner_self_eq_norm_sq, hx, real_inner_self_eq_norm_sq, hy]

Premises used: real_inner_smul_right, real_inner_self_eq_norm_sq, inner_sub_left, inner_sub_right, real_inner_smul_left, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
⊢ HPow.hPow (β := ℕ) (1 - ⟪x, y⟫ * ⟪x, y⟫) 2 +
      (HPow.hPow (α := ℝ) (β := ℕ) 1 2 - ⟪x, y⟫ * ⟪x, y⟫ -
          (⟪x, y⟫ * ⟪x, y⟫ - ⟪x, y⟫ * (⟪x, y⟫ * HPow.hPow (α := ℝ) (β := ℕ) 1 2))) *
        HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) 1 2 - ⟪x, y⟫ * ⟪x, y⟫ -
      (⟪x, y⟫ * ⟪x, y⟫ - ⟪x, y⟫ * (⟪x, y⟫ * HPow.hPow (α := ℝ) (β := ℕ) 1 2))

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

Tactic:
have H2 : (1 - ⟪y, x⟫ * ⟪x, y⟫) ^ 2 + ‖x - ⟪y, x⟫ • y‖ ^ 2 * ⟪x, y⟫ ^ 2 =
      ‖x - ⟪y, x⟫ • y‖ ^ 2 := by
    rw [← real_inner_self_eq_norm_sq, inner_sub_left, inner_sub_right, inner_sub_right,
    real_inner_smul_right, real_inner_smul_left, real_inner_smul_right, real_inner_smul_left,
    real_inner_comm x y, real_inner_self_eq_norm_sq, hx, real_inner_self_eq_norm_sq, hy]
    ring
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
H2 :
  HPow.hPow (β := ℕ) (1 - ⟪y, x⟫ * ⟪x, y⟫) 2 + HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2 * HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
    HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2
neg :
  HPow.hPow (β := ℕ) (1 - ⟪y, x⟫ * ⟪x, y⟫) 2 + HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2 * HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
    HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2
⊢ HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (HPow.hPow (α := ℝ) (β := ℕ) 1 2 - ⟪y, x⟫ * ⟪x, y⟫)) 2 +
      HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
    1

Tactic:
field_simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
H2 :
  HPow.hPow (β := ℕ) (1 - ⟪y, x⟫ * ⟪x, y⟫) 2 + HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2 * HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
    HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2
⊢ HPow.hPow (β := ℕ) (1 - ⟪y, x⟫ * ⟪x, y⟫) 2 + HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2 * HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
    HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2

Tactic:
H2
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
H2 :
  HPow.hPow (β := ℕ) (1 - ⟪y, x⟫ * ⟪x, y⟫) 2 + HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2 * HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
    HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2
⊢ HPow.hPow (β := ℕ) (1 - ⟪y, x⟫ * ⟪x, y⟫) 2 + HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2 * HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
    HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2

Tactic:
exact H2
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ HPow.hPow (β := ℕ) ⟪x, NormedSpace.normalize (ortho y x)⟫ 2 = HPow.hPow (β := ℕ) (Real.sin (angle x y)) 2

Tactic:
simp [Real.sin_sq, ← inner_eq_cos_angle_of_norm_eq_one hx hy,
      ← inner_normalized_ortho_sq_add_inner_sq_eq_one hx hy]

Premises used: Real.sin_sq, _private.0.InnerProductGeometry.inner_normalized_ortho_sq_add_inner_sq_eq_one, InnerProductGeometry.inner_eq_cos_angle_of_norm_eq_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ HPow.hPow (β := ℕ) ⟪x, NormedSpace.normalize (ortho y x)⟫ 2 = HPow.hPow (β := ℕ) (Real.sin (angle x y)) 2

Tactic:
have H : ⟪x, normalize (ortho y x)⟫ ^ 2 = Real.sin (angle x y) ^ 2 := by
    simp [Real.sin_sq, ← inner_eq_cos_angle_of_norm_eq_one hx hy,
      ← inner_normalized_ortho_sq_add_inner_sq_eq_one hx hy]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
H : HPow.hPow (β := ℕ) ⟪x, NormedSpace.normalize (ortho y x)⟫ 2 = HPow.hPow (β := ℕ) (Real.sin (angle x y)) 2
⊢ |⟪x, NormedSpace.normalize (ortho y x)⟫| = Real.sin (angle x y)

Tactic:
rw [sq_eq_sq_iff_abs_eq_abs, abs_of_nonneg (sin_angle_nonneg x y)] at H

Premises used: InnerProductGeometry.sin_angle_nonneg, sq_eq_sq_iff_abs_eq_abs, abs_of_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
H : |⟪x, NormedSpace.normalize (ortho y x)⟫| = Real.sin (angle x y)
rw : 0 ≤ ‖ortho y x‖⁻¹ * ⟪x, ortho y x⟫
⊢ 0 ≤ ⟪x, NormedSpace.normalize (ortho y x)⟫

Tactic:
rw [NormedSpace.normalize, real_inner_smul_right]

Premises used: real_inner_smul_right, NormedSpace.normalize
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
H : |⟪x, NormedSpace.normalize (ortho y x)⟫| = Real.sin (angle x y)
⊢ 0 ≤ ‖ortho y x‖⁻¹ * ⟪x, ortho y x⟫

Tactic:
Left.mul_nonneg (inv_nonneg_of_nonneg (norm_nonneg (ortho y x)))
      (inner_ortho_nonneg hx hy)

Premises used: inv_nonneg_of_nonneg, _private.0.InnerProductGeometry.ortho, Left.mul_nonneg, _private.0.InnerProductGeometry.inner_ortho_nonneg, norm_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
H : |⟪x, NormedSpace.normalize (ortho y x)⟫| = Real.sin (angle x y)
⊢ 0 ≤ ‖ortho y x‖⁻¹ * ⟪x, ortho y x⟫

Tactic:
exact Left.mul_nonneg (inv_nonneg_of_nonneg (norm_nonneg (ortho y x)))
      (inner_ortho_nonneg hx hy)

Premises used: inv_nonneg_of_nonneg, _private.0.InnerProductGeometry.ortho, Left.mul_nonneg, _private.0.InnerProductGeometry.inner_ortho_nonneg, norm_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
H : |⟪x, NormedSpace.normalize (ortho y x)⟫| = Real.sin (angle x y)
⊢ 0 ≤ ⟪x, NormedSpace.normalize (ortho y x)⟫

Tactic:
have H0 : 0 ≤ ⟪x, normalize (ortho y x)⟫ := by
    rw [NormedSpace.normalize, real_inner_smul_right]
    exact Left.mul_nonneg (inv_nonneg_of_nonneg (norm_nonneg (ortho y x)))
      (inner_ortho_nonneg hx hy)
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
H : |⟪x, NormedSpace.normalize (ortho y x)⟫| = Real.sin (angle x y)
H0 : 0 ≤ ⟪x, NormedSpace.normalize (ortho y x)⟫
⊢ ⟪x, NormedSpace.normalize (ortho y x)⟫ = Real.sin (angle x y)

Tactic:
simp_all [abs_of_nonneg H0]

Premises used: abs_of_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
rw : x = ⟪x, y⟫ • y + ⟪x, NormedSpace.normalize (x - ⟪y, x⟫ • y)⟫ • NormedSpace.normalize (x - ⟪y, x⟫ • y)
⊢ x = Real.cos (angle x y) • y + Real.sin (angle x y) • NormedSpace.normalize (ortho y x)

Tactic:
rw [← inner_ortho_right_eq_sin_angle hx hy, ← inner_eq_cos_angle_of_norm_eq_one hx hy,
    ortho_eq_sub_inner _ hy]

Premises used: _private.0.InnerProductGeometry.inner_ortho_right_eq_sin_angle, InnerProductGeometry.inner_eq_cos_angle_of_norm_eq_one, _private.0.InnerProductGeometry.ortho_eq_sub_inner
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
pos :
  ∀ (hxy : x - ⟪x, y⟫ • y = 0),
    x = ⟪x, y⟫ • y + ⟪x, NormedSpace.normalize (x - ⟪y, x⟫ • y)⟫ • NormedSpace.normalize (x - ⟪y, x⟫ • y)
neg :
  ∀ (hxy : ¬x - ⟪x, y⟫ • y = 0),
    x = ⟪x, y⟫ • y + ⟪x, NormedSpace.normalize (x - ⟪y, x⟫ • y)⟫ • NormedSpace.normalize (x - ⟪y, x⟫ • y)
⊢ x = ⟪x, y⟫ • y + ⟪x, NormedSpace.normalize (x - ⟪y, x⟫ • y)⟫ • NormedSpace.normalize (x - ⟪y, x⟫ • y)

Tactic:
by_cases hxy : x - ⟪x, y⟫ • y = 0
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : x - ⟪x, y⟫ • y = 0
⊢ x = ⟪x, y⟫ • y + ⟪x, NormedSpace.normalize (x - ⟪y, x⟫ • y)⟫ • NormedSpace.normalize (x - ⟪y, x⟫ • y)

Tactic:
simp [hxy, real_inner_comm, ← sub_eq_zero]

Premises used: sub_eq_zero, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
neg :
  x =
    ⟪y, x⟫ • y +
      (‖x - ⟪y, x⟫ • y‖⁻¹ • (HPow.hPow (α := ℝ) (β := ℕ) 1 2 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2)) •
        ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)
⊢ x = ⟪x, y⟫ • y + ⟪x, NormedSpace.normalize (x - ⟪y, x⟫ • y)⟫ • NormedSpace.normalize (x - ⟪y, x⟫ • y)

Tactic:
rw [NormedSpace.normalize, real_inner_smul_right, inner_sub_right, real_inner_smul_right,
    real_inner_self_eq_norm_sq, hx, real_inner_comm y, ← sq, mul_smul, ← smul_assoc]

Premises used: smul_assoc, sq, real_inner_smul_right, real_inner_self_eq_norm_sq, inner_sub_right, NormedSpace.normalize, real_inner_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
neg : x = ⟪y, x⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * (1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2)) • ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)
⊢ x =
    ⟪y, x⟫ • y +
      (‖x - ⟪y, x⟫ • y‖⁻¹ • (HPow.hPow (α := ℝ) (β := ℕ) 1 2 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2)) •
        ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)

Tactic:
simp only [one_pow, smul_eq_mul]

Premises used: one_pow, smul_eq_mul
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
rw : ⟪x, y⟫ ≠ 1 ∧ ⟪x, y⟫ ≠ -1
⊢ 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0

Tactic:
rw [sub_ne_zero, ne_comm, sq_ne_one_iff]

Premises used: sq_ne_one_iff, sub_ne_zero, ne_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
left : ⟪x, y⟫ ≠ 1
right : ⟪x, y⟫ ≠ -1
⊢ ⟪x, y⟫ ≠ 1 ∧ ⟪x, y⟫ ≠ -1

Tactic:
constructor
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
left : ∀ (hxy : ⟪x, y⟫ = 1), x - ⟪x, y⟫ • y = 0
⊢ ⟪x, y⟫ ≠ 1

Tactic:
contrapose hxy
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
right : ∀ (hxy : ⟪x, y⟫ = -1), x - ⟪x, y⟫ • y = 0
⊢ ⟪x, y⟫ ≠ -1

Tactic:
contrapose hxy
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ⟪x, y⟫ = 1
⊢ x = y

Tactic:
rw [inner_eq_one_iff_of_norm_eq_one hx hy] at hxy

Premises used: inner_eq_one_iff_of_norm_eq_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : x = y
⊢ x - ⟪x, y⟫ • y = 0

Tactic:
simp [hy, hxy]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ⟪x, y⟫ = -1
⊢ x = -y

Tactic:
rw [inner_eq_neg_one_iff_of_norm_eq_one hx hy] at hxy

Premises used: inner_eq_neg_one_iff_of_norm_eq_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : x = -y
⊢ x - ⟪x, y⟫ • y = 0

Tactic:
simp [hy, hxy]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0

Tactic:
have H : 1 - ⟪x, y⟫ ^ 2 ≠ 0 := by
    rw [sub_ne_zero, ne_comm, sq_ne_one_iff]
    constructor <;> contrapose hxy
    · rw [inner_eq_one_iff_of_norm_eq_one hx hy] at hxy
      simp [hy, hxy]
    · rw [inner_eq_neg_one_iff_of_norm_eq_one hx hy] at hxy
      simp [hy, hxy]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
neg : x = ⟪y, x⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * (1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2) * ‖x - ⟪y, x⟫ • y‖⁻¹) • (x - ⟪y, x⟫ • y)
⊢ x = ⟪y, x⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * (1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2)) • ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)

Tactic:
rw [← smul_assoc, smul_eq_mul]

Premises used: smul_assoc, smul_eq_mul
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
neg : x = ⟪y, x⟫ • y + ((1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2) / HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2) • (x - ⟪y, x⟫ • y)
⊢ x = ⟪y, x⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * (1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2) * ‖x - ⟪y, x⟫ • y‖⁻¹) • (x - ⟪y, x⟫ • y)

Tactic:
field_simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
neg : x = ⟪y, x⟫ • y + ((1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2) / ⟪x - ⟪y, x⟫ • y, x - ⟪y, x⟫ • y⟫) • (x - ⟪y, x⟫ • y)
⊢ x = ⟪y, x⟫ • y + ((1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2) / HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2) • (x - ⟪y, x⟫ • y)

Tactic:
rw [← real_inner_self_eq_norm_sq]

Premises used: real_inner_self_eq_norm_sq
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
rw : 1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2 - (⟪y, x⟫ * ⟪y, x⟫ - ⟪y, x⟫ * (⟪y, x⟫ * 1)) = 1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2
⊢ ⟪x - ⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2

Tactic:
rw [inner_sub_left, inner_sub_right, inner_sub_right, inner_self_eq_one_of_norm_eq_one hx,
      real_inner_smul_right, ← sq, real_inner_smul_left, real_inner_smul_left,
      real_inner_smul_right, inner_self_eq_one_of_norm_eq_one hy, real_inner_comm y x]

Premises used: inner_self_eq_one_of_norm_eq_one, sq, real_inner_smul_right, inner_sub_left, inner_sub_right, real_inner_smul_left, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
⊢ 1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2 - (⟪y, x⟫ * ⟪y, x⟫ - ⟪y, x⟫ * (⟪y, x⟫ * 1)) = 1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
⊢ ⟪x - ⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2

Tactic:
have H0 : ⟪x - ⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - ⟪x, y⟫ ^ 2 := by
    rw [inner_sub_left, inner_sub_right, inner_sub_right, inner_self_eq_one_of_norm_eq_one hx,
      real_inner_smul_right, ← sq, real_inner_smul_left, real_inner_smul_left,
      real_inner_smul_right, inner_self_eq_one_of_norm_eq_one hy, real_inner_comm y x]
    ring
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
H0 : ⟪x - ⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2
neg : x = ⟪x, y⟫ • y + ((1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2) / (1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2)) • (x - ⟪x, y⟫ • y)
⊢ x = ⟪y, x⟫ • y + ((1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2) / ⟪x - ⟪y, x⟫ • y, x - ⟪y, x⟫ • y⟫) • (x - ⟪y, x⟫ • y)

Tactic:
rw [real_inner_comm x, H0]

Premises used: real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
H0 : ⟪x - ⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2
⊢ x = ⟪x, y⟫ • y + ((1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2) / (1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2)) • (x - ⟪x, y⟫ • y)

Tactic:
simp [H]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
inl : ∀ (H : π < angle x y + angle y z), angle x z ≤ angle x y + angle y z
inr : ∀ (H : angle x y + angle y z ≤ π), angle x z ≤ angle x y + angle y z
⊢ angle x z ≤ angle x y + angle y z

Tactic:
rcases lt_or_ge π (angle x y + angle y z) with H | H

Premises used: Real.pi, InnerProductGeometry.angle, HAdd.hAdd, lt_or_ge
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : π < angle x y + angle y z
linarith :
  angle x y + angle y z < angle x z →
    π - (angle x y + angle y z) + (angle x y + angle y z - angle x z) + (angle x z - π) = 0
⊢ angle x z ≤ angle x y + angle y z

Tactic:
linarith [angle_le_pi x z]

Premises used: InnerProductGeometry.angle_le_pi
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
this : Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z)
⊢ 0 ≤ angle x y + angle y z

Tactic:
have H0 : 0 ≤ angle x y + angle y z :=
      add_nonneg (angle_nonneg x y) (angle_nonneg y z)
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
this : Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z)
H0 : 0 ≤ angle x y + angle y z
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : angle x z ≤ angle x y + angle y z) (H0 : 0 ≤ angle x y + angle y z), angle x z ≤ angle x y + angle y z
⊢ angle x z ≤ angle x y + angle y z

Tactic:
rwa [Real.strictAntiOn_cos.le_iff_ge ⟨H0, H⟩ ⟨angle_nonneg x z, angle_le_pi x z⟩] at this

Premises used: InnerProductGeometry.angle_le_pi, StrictAntiOn.le_iff_ge, InnerProductGeometry.angle_nonneg, And.intro, Real.strictAntiOn_cos
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
inr : Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z)
⊢ angle x z ≤ angle x y + angle y z

Tactic:
suffices Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z) by
    have H0 : 0 ≤ angle x y + angle y z :=
      add_nonneg (angle_nonneg x y) (angle_nonneg y z)
    rwa [Real.strictAntiOn_cos.le_iff_ge ⟨H0, H⟩ ⟨angle_nonneg x z, angle_le_pi x z⟩] at this