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 z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
⊢ ⟪x, z⟫ = ⟪x, z⟫

Tactic:
have H1 : ⟪x, z⟫ = ⟪x, z⟫ := rfl
-- 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 ≤ π
H1 : ⟪x, z⟫ = ⟪x, z⟫
⊢ ⟪x, z⟫ =
    ⟪Real.cos (angle x y) • y + Real.sin (angle x y) • NormedSpace.normalize (ortho y x),
      Real.cos (angle z y) • y + Real.sin (angle z y) • NormedSpace.normalize (ortho y z)⟫

Tactic:
nth_rw 2 [angle_le_angle_add_angle_aux hx hy, angle_le_angle_add_angle_aux hz hy] at H1

Premises used: _private.0.InnerProductGeometry.angle_le_angle_add_angle_aux
-- 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 ≤ π
H1 :
  ⟪x, z⟫ =
    ⟪Real.cos (angle x y) • y + Real.sin (angle x y) • NormedSpace.normalize (ortho y x),
      Real.cos (angle z y) • y + Real.sin (angle z y) • NormedSpace.normalize (ortho y z)⟫
⊢ ⟪x, z⟫ =
    Real.cos (angle y z) * (Real.cos (angle x y) * HPow.hPow (α := ℝ) (β := ℕ) 1 2) +
        Real.cos (angle y z) * (Real.sin (angle x y) * 0) +
      (Real.sin (angle y z) * (Real.cos (angle x y) * 0) +
        Real.sin (angle y z) *
          (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫))

Tactic:
simp only [inner_add_left, inner_add_right, real_inner_smul_left, real_inner_smul_right,
    real_inner_comm y (normalize _), real_inner_self_eq_norm_sq, hy, angle_comm z y,
    inner_normalize_ortho] at H1

Premises used: inner_add_left, real_inner_smul_right, real_inner_self_eq_norm_sq, inner_add_right, InnerProductGeometry.angle_comm, _private.0.InnerProductGeometry.inner_normalize_ortho, real_inner_smul_left, NormedSpace.normalize, real_inner_comm
-- 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 ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle y z) * (Real.cos (angle x y) * HPow.hPow (α := ℝ) (β := ℕ) 1 2) +
        Real.cos (angle y z) * (Real.sin (angle x y) * 0) +
      (Real.sin (angle y z) * (Real.cos (angle x y) * 0) +
        Real.sin (angle y z) *
          (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫))
⊢ ⟪x, z⟫ =
    Real.cos (angle y z) * Real.cos (angle x y) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)

Tactic:
simp only [one_pow, mul_one, mul_zero, add_zero, zero_add] at H1

Premises used: one_pow, zero_add, MulZeroClass.mul_zero, mul_one, add_zero
-- 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 ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle y z) * Real.cos (angle x y) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
⊢ ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)

Tactic:
rw [mul_comm (Real.cos (angle y z))] at H1

Premises used: Real.cos, InnerProductGeometry.angle, mul_comm
-- 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 ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
inr :
  Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) ≤
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
⊢ Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z)

Tactic:
rw [Real.cos_add, ← inner_eq_cos_angle_of_norm_eq_one hx hz, H1]

Premises used: Real.cos_add, 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 z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
pos : ∀ (H3 : ortho y x = 0), -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
neg : ∀ (H3 : ¬ortho y x = 0), -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
⊢ -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫

Tactic:
by_cases H3 : ortho y x = 0

Premises used: _private.0.InnerProductGeometry.ortho
-- 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 ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H3 : ortho y x = 0
⊢ -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫

Tactic:
simp [*]
-- 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 ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H3 : ¬ortho y x = 0
pos : ∀ (H4 : ortho y z = 0), -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
neg : ∀ (H4 : ¬ortho y z = 0), -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
⊢ -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫

Tactic:
by_cases H4 : ortho y z = 0

Premises used: _private.0.InnerProductGeometry.ortho
-- 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 ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H3 : ¬ortho y x = 0
H4 : ortho y z = 0
⊢ -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫

Tactic:
simp [*]
-- 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 ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H3 : ¬ortho y x = 0
H4 : ¬ortho y z = 0
⊢ -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫

Tactic:
neg_one_le_real_inner_of_norm_eq_one
      (norm_normalize_eq_one_iff.mpr H3) (norm_normalize_eq_one_iff.mpr H4)

Premises used: Iff.mpr, neg_one_le_real_inner_of_norm_eq_one, NormedSpace.norm_normalize_eq_one_iff
-- 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 ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H3 : ¬ortho y x = 0
H4 : ¬ortho y z = 0
⊢ -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫

Tactic:
exact neg_one_le_real_inner_of_norm_eq_one
      (norm_normalize_eq_one_iff.mpr H3) (norm_normalize_eq_one_iff.mpr H4)

Premises used: Iff.mpr, neg_one_le_real_inner_of_norm_eq_one, NormedSpace.norm_normalize_eq_one_iff
-- 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 ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
⊢ -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫

Tactic:
have H2 : -1 ≤ ⟪normalize (ortho y x), normalize (ortho y z)⟫ := by
    by_cases H3 : ortho y x = 0
    · simp [*]
    by_cases H4 : ortho y z = 0
    · simp [*]
    exact neg_one_le_real_inner_of_norm_eq_one
      (norm_normalize_eq_one_iff.mpr H3) (norm_normalize_eq_one_iff.mpr H4)
-- 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 ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H2 : -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
⊢ 0 ≤ Real.sin (angle x y)

Tactic:
have := sin_angle_nonneg x y
-- 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 ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H2 : -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
this : 0 ≤ Real.sin (angle x y)
⊢ 0 ≤ Real.sin (angle y z)

Tactic:
have := sin_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 ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H2 : -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
this_1 : 0 ≤ Real.sin (angle x y)
this : 0 ≤ Real.sin (angle y z)
inr :
  Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) ≤
    Real.cos (angle x y) * Real.cos (angle y z) + Real.sin (angle y z) * (Real.sin (angle x y) * -1)
⊢ Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) ≤
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)

Tactic:
grw [← H2]
-- 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 ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H2 : -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
this_1 : 0 ≤ Real.sin (angle x y)
this : 0 ≤ Real.sin (angle y z)
inr :
  Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) =
    Real.cos (angle x y) * Real.cos (angle y z) + Real.sin (angle y z) * (Real.sin (angle x y) * -1)
⊢ Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) ≤
    Real.cos (angle x y) * Real.cos (angle y z) + Real.sin (angle y z) * (Real.sin (angle x y) * -1)

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- 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 ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H2 : -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
this_1 : 0 ≤ Real.sin (angle x y)
this : 0 ≤ Real.sin (angle y z)
⊢ Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) =
    Real.cos (angle x y) * Real.cos (angle y z) + Real.sin (angle y z) * (Real.sin (angle x y) * -1)

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
hxy1 : angle x y ≠ 0
hxy2 : angle x y ≠ π
h : ortho x y = 0
⊢ y = ⟪x, y⟫ • x

Tactic:
rw [ortho_eq_sub_inner _ hx, sub_eq_zero] at h

Premises used: sub_eq_zero, _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
hxy1 : angle x y ≠ 0
hxy2 : angle x y ≠ π
h : y = ⟪x, y⟫ • x
⊢ False

Tactic:
grind [abs, norm_smul, Real.norm_eq_abs, norm_zero, inner_eq_mul_norm_iff_angle_eq_zero,
    inner_eq_neg_mul_norm_iff_angle_eq_pi]

Premises used: norm_smul, abs, norm_zero, InnerProductGeometry.inner_eq_neg_mul_norm_iff_angle_eq_pi, Real.norm_eq_abs, InnerProductGeometry.inner_eq_mul_norm_iff_angle_eq_zero
-- 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 : angle x y = 0
⊢ x = y

Tactic:
grind [eq_of_angle_eq_zero_of_norm_eq]

Premises used: InnerProductGeometry.eq_of_angle_eq_zero_of_norm_eq
-- 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 z ≠ π
H0 : angle x z = angle x y + angle y z
pos : ∀ (H1 : angle x z = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
neg : ∀ (H1 : ¬angle x z = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
by_cases H1 : angle x z = 0

Premises used: InnerProductGeometry.angle
-- 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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : angle x z = 0
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
grind [angle_nonneg, Real.sin_zero, zero_smul]

Premises used: Real.sin_zero, InnerProductGeometry.angle_nonneg, zero_smul
-- 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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
⊢ Real.sin (angle x z) ≠ 0

Tactic:
grind [sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi]

Premises used: InnerProductGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
⊢ Real.sin (angle x z) ≠ 0

Tactic:
have Hxz : Real.sin (angle x z) ≠ 0 := by
    grind [sin_eq_zero_iff_angle_eq_zero_or_angle_eq_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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
pos : ∀ (H2 : angle x y = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
neg : ∀ (H2 : ¬angle x y = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
by_cases H2 : angle x y = 0

Premises used: InnerProductGeometry.angle
-- 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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : angle x y = 0
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
grind [Real.sin_zero, zero_smul, eq_of_angle_eq_zero]

Premises used: _private.0.InnerProductGeometry.eq_of_angle_eq_zero, Real.sin_zero, zero_smul
-- 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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
pos : ∀ (H3 : angle y z = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
neg : ∀ (H3 : ¬angle y z = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
by_cases H3 : angle y z = 0

Premises used: InnerProductGeometry.angle
-- 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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : angle y z = 0
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
grind [Real.sin_zero, zero_smul, smul_right_inj, eq_of_angle_eq_zero]

Premises used: _private.0.InnerProductGeometry.eq_of_angle_eq_zero, Real.sin_zero, zero_smul, smul_right_inj
-- 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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
pos : ∀ (H4 : angle x y = π), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
neg : ∀ (H4 : ¬angle x y = π), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
by_cases H4 : angle x y = π

Premises used: InnerProductGeometry.angle
-- 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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : angle x y = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
grind [angle_le_pi, angle_nonneg]

Premises used: InnerProductGeometry.angle_le_pi, InnerProductGeometry.angle_nonneg
-- 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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
pos : ∀ (H5 : angle y z = π), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
neg : ∀ (H5 : ¬angle y z = π), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
by_cases H5 : angle y z = π

Premises used: InnerProductGeometry.angle
-- 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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : angle y z = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
grind [angle_le_pi, angle_nonneg]

Premises used: InnerProductGeometry.angle_le_pi, InnerProductGeometry.angle_nonneg
-- 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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : ¬angle y z = π
⊢ ⟪x, z⟫ = ⟪x, z⟫

Tactic:
have H6 : ⟪x, z⟫ = ⟪x, z⟫ := rfl
-- 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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : ¬angle y z = π
H6 : ⟪x, z⟫ = ⟪x, z⟫
⊢ ⟪x, z⟫ =
    ⟪Real.cos (angle x y) • y + Real.sin (angle x y) • NormedSpace.normalize (ortho y x),
      Real.cos (angle z y) • y + Real.sin (angle z y) • NormedSpace.normalize (ortho y z)⟫

Tactic:
nth_rw 2 [angle_le_angle_add_angle_aux hx hy, angle_le_angle_add_angle_aux hz hy] at H6

Premises used: _private.0.InnerProductGeometry.angle_le_angle_add_angle_aux