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
y z : V
hy : y ≠ 0
h : angle 0 z = angle 0 y + angle y z
hxz₁ : ¬angle 0 z = π
hxz₂ : ¬angle 0 z = 0
h_sin_xz : Real.sin (angle 0 z) ≠ 0
⊢ angle y z = 0

Tactic:
simp only [angle_zero_left, left_eq_add] at h

Premises used: left_eq_add, InnerProductGeometry.angle_zero_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
y z : V
hy : y ≠ 0
hxz₁ : ¬angle 0 z = π
hxz₂ : ¬angle 0 z = 0
h_sin_xz : Real.sin (angle 0 z) ≠ 0
h : angle y z = 0
⊢ y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ z = r • y

Tactic:
rw [angle_eq_zero_iff] at h

Premises used: InnerProductGeometry.angle_eq_zero_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
y z : V
hy : y ≠ 0
hxz₁ : ¬angle 0 z = π
hxz₂ : ¬angle 0 z = 0
h_sin_xz : Real.sin (angle 0 z) ≠ 0
h : y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ z = r • y
pos :
  y ≠ 0 →
    ∀ (r : ℝ) (hr : 0 < r) (hxz₁ : ¬angle 0 (r • y) = π) (hxz₂ : ¬angle 0 (r • y) = 0)
      (h_sin_xz : Real.sin (angle 0 (r • y)) ≠ 0),
      Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {0, r • y}) y
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {0, z}) y

Tactic:
obtain ⟨_, ⟨r, ⟨hr, rfl⟩⟩⟩ := h

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
y : V
hy left : y ≠ 0
r : ℝ
hr : 0 < r
hxz₁ : ¬angle 0 (r • y) = π
hxz₂ : ¬angle 0 (r • y) = 0
h_sin_xz : Real.sin (angle 0 (r • y)) ≠ 0
⊢ 0 ≤ r

Tactic:
hr.le

Premises used: LT.lt.le
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
y : V
hy left : y ≠ 0
r : ℝ
hr : 0 < r
hxz₁ : ¬angle 0 (r • y) = π
hxz₂ : ¬angle 0 (r • y) = 0
h_sin_xz : Real.sin (angle 0 (r • y)) ≠ 0
pos :
  ∀ (r : ℝ≥0) (hr : 0 < (↑r : ℝ)) (hxz₁ : ¬angle 0 ((↑r : ℝ) • y) = π) (hxz₂ : ¬angle 0 ((↑r : ℝ) • y) = 0)
    (h_sin_xz : Real.sin (angle 0 ((↑r : ℝ) • y)) ≠ 0),
    Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {0, (↑r : ℝ) • y}) y
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {0, r • y}) y

Tactic:
lift r to ℝ≥0 using hr.le

Premises used: LT.lt.le
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
y : V
hy left : y ≠ 0
r : ℝ≥0
hr : 0 < (↑r : ℝ)
hxz₁ : ¬angle 0 ((↑r : ℝ) • y) = π
hxz₂ : ¬angle 0 ((↑r : ℝ) • y) = 0
h_sin_xz : Real.sin (angle 0 ((↑r : ℝ) • y)) ≠ 0
pos : Membership.mem (γ := Submodule ℝ≥0 V) (ℝ≥0 ∙ y) y
pos₁ : IsUnit r
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {0, (↑r : ℝ) • y}) y

Tactic:
rw [← NNReal.smul_def, Submodule.span_insert_zero, Submodule.span_singleton_smul_eq]

Premises used: NNReal.smul_def, Submodule.span_singleton_smul_eq, Submodule.span_insert_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
y : V
hy left : y ≠ 0
r : ℝ≥0
hr : 0 < (↑r : ℝ)
hxz₁ : ¬angle 0 ((↑r : ℝ) • y) = π
hxz₂ : ¬angle 0 ((↑r : ℝ) • y) = 0
h_sin_xz : Real.sin (angle 0 ((↑r : ℝ) • y)) ≠ 0
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (ℝ≥0 ∙ y) y

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
y : V
hy left : y ≠ 0
r : ℝ≥0
hr : 0 < (↑r : ℝ)
hxz₁ : ¬angle 0 ((↑r : ℝ) • y) = π
hxz₂ : ¬angle 0 ((↑r : ℝ) • y) = 0
h_sin_xz : Real.sin (angle 0 ((↑r : ℝ) • y)) ≠ 0
⊢ 0 < r

Tactic:
norm_cast at hr
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
y : V
hy left : y ≠ 0
r : ℝ≥0
hxz₁ : ¬angle 0 ((↑r : ℝ) • y) = π
hxz₂ : ¬angle 0 ((↑r : ℝ) • y) = 0
h_sin_xz : Real.sin (angle 0 ((↑r : ℝ) • y)) ≠ 0
hr : 0 < r
⊢ IsUnit r

Tactic:
grind [isUnit_iff_ne_zero]

Premises used: isUnit_iff_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
pos : ∀ (hz : z = 0), Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
neg : ∀ (hz : ¬z = 0), Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y

Tactic:
by_cases hz : z = 0
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : z = 0
pos :
  ∀ (h : angle x 0 = angle x y + angle y 0) (hxz₁ : ¬angle x 0 = π) (hxz₂ : ¬angle x 0 = 0)
    (h_sin_xz : Real.sin (angle x 0) ≠ 0), Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, 0}) y
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y

Tactic:
subst z
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : ¬x = 0
h : angle x 0 = angle x y + angle y 0
hxz₁ : ¬angle x 0 = π
hxz₂ : ¬angle x 0 = 0
h_sin_xz : Real.sin (angle x 0) ≠ 0
⊢ angle x y = 0

Tactic:
simp only [angle_zero_right, right_eq_add] at h

Premises used: InnerProductGeometry.angle_zero_right, right_eq_add
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : ¬x = 0
hxz₁ : ¬angle x 0 = π
hxz₂ : ¬angle x 0 = 0
h_sin_xz : Real.sin (angle x 0) ≠ 0
h : angle x y = 0
⊢ x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x

Tactic:
rw [angle_eq_zero_iff] at h

Premises used: InnerProductGeometry.angle_eq_zero_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : ¬x = 0
hxz₁ : ¬angle x 0 = π
hxz₂ : ¬angle x 0 = 0
h_sin_xz : Real.sin (angle x 0) ≠ 0
h : x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x
pos :
  x ≠ 0 →
    ∀ (r : ℝ) (hr : 0 < r) (hy : r • x ≠ 0), Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, 0}) (r • x)
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, 0}) y

Tactic:
obtain ⟨_, ⟨r, ⟨hr, rfl⟩⟩⟩ := h

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : ¬x = 0
hxz₁ : ¬angle x 0 = π
hxz₂ : ¬angle x 0 = 0
h_sin_xz : Real.sin (angle x 0) ≠ 0
left : x ≠ 0
r : ℝ
hr : 0 < r
hy : r • x ≠ 0
⊢ 0 ≤ r

Tactic:
hr.le

Premises used: LT.lt.le
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : ¬x = 0
hxz₁ : ¬angle x 0 = π
hxz₂ : ¬angle x 0 = 0
h_sin_xz : Real.sin (angle x 0) ≠ 0
left : x ≠ 0
r : ℝ
hr : 0 < r
hy : r • x ≠ 0
pos :
  ∀ (r : ℝ≥0) (hr : 0 < (↑r : ℝ)) (hy : (↑r : ℝ) • x ≠ 0),
    Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, 0}) ((↑r : ℝ) • x)
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, 0}) (r • x)

Tactic:
lift r to ℝ≥0 using hr.le

Premises used: LT.lt.le
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : ¬x = 0
hxz₁ : ¬angle x 0 = π
hxz₂ : ¬angle x 0 = 0
h_sin_xz : Real.sin (angle x 0) ≠ 0
left : x ≠ 0
r : ℝ≥0
hr : 0 < (↑r : ℝ)
hy : (↑r : ℝ) • x ≠ 0
⊢ Membership.mem (γ := Set V) {x, 0} x

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : ¬x = 0
hxz₁ : ¬angle x 0 = π
hxz₂ : ¬angle x 0 = 0
h_sin_xz : Real.sin (angle x 0) ≠ 0
left : x ≠ 0
r : ℝ≥0
hr : 0 < (↑r : ℝ)
hy : (↑r : ℝ) • x ≠ 0
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, 0}) ((↑r : ℝ) • x)

Tactic:
exact Submodule.smul_mem _ _ (Submodule.mem_span_of_mem (by simp))

Premises used: Submodule.mem_span_of_mem, Submodule.smul_mem
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
⊢ 0 ≤ Real.sin (angle y z) / ‖x‖

Tactic:
grind [sin_angle_nonneg, norm_nonneg, div_nonneg_iff, mul_nonneg_iff]

Premises used: mul_nonneg_iff, InnerProductGeometry.sin_angle_nonneg, div_nonneg_iff, norm_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
⊢ 0 ≤ Real.sin (angle y z) / ‖x‖

Tactic:
have hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖ := by
      grind [sin_angle_nonneg, norm_nonneg, div_nonneg_iff, mul_nonneg_iff]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
⊢ 0 ≤ Real.sin (angle x y) / ‖z‖

Tactic:
grind [sin_angle_nonneg, norm_nonneg, div_nonneg_iff, mul_nonneg_iff]

Premises used: mul_nonneg_iff, InnerProductGeometry.sin_angle_nonneg, div_nonneg_iff, norm_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
⊢ 0 ≤ Real.sin (angle x y) / ‖z‖

Tactic:
have hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖ := by
      grind [sin_angle_nonneg, norm_nonneg, div_nonneg_iff, mul_nonneg_iff]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
⊢ 0 ≤ Real.sin (angle x z) / ‖y‖

Tactic:
grind [sin_angle_nonneg, norm_nonneg, div_nonneg_iff, mul_nonneg_iff]

Premises used: mul_nonneg_iff, InnerProductGeometry.sin_angle_nonneg, div_nonneg_iff, norm_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
⊢ 0 ≤ Real.sin (angle x z) / ‖y‖

Tactic:
have hnneg₃ : 0 ≤ Real.sin (angle x z) / ‖y‖ := by
      grind [sin_angle_nonneg, norm_nonneg, div_nonneg_iff, mul_nonneg_iff]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
hnneg₃ : 0 ≤ Real.sin (angle x z) / ‖y‖
simp : ¬Real.sin (angle x z) = 0 ∧ ¬y = 0
⊢ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ ≠ 0

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
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
hnneg₃ : 0 ≤ Real.sin (angle x z) / ‖y‖
⊢ ¬Real.sin (angle x z) = 0 ∧ ¬y = 0

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
hnneg₃ : 0 ≤ Real.sin (angle x z) / ‖y‖
⊢ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ ≠ 0

Tactic:
have hnonzero : (⟨Real.sin (angle x z) / ‖y‖, hnneg₃⟩ : ℝ≥0) ≠ 0 := by
      simp; grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
hnneg₃ : 0 ≤ Real.sin (angle x z) / ‖y‖
hnonzero : Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ ≠ 0
⊢ angle (NormedSpace.normalize x) (NormedSpace.normalize z) ≠ π →
    angle (NormedSpace.normalize x) (NormedSpace.normalize z) =
        angle (NormedSpace.normalize x) (NormedSpace.normalize y) +
          angle (NormedSpace.normalize y) (NormedSpace.normalize z) →
      Real.sin (angle (NormedSpace.normalize x) (NormedSpace.normalize z)) • NormedSpace.normalize y =
        Real.sin (angle (NormedSpace.normalize y) (NormedSpace.normalize z)) • NormedSpace.normalize x +
          Real.sin (angle (NormedSpace.normalize x) (NormedSpace.normalize y)) • NormedSpace.normalize z

Tactic:
have h₁ := angle_expression_of_angle_eq_angle_sum (norm_normalize_eq_one_iff.mpr hx)
        (norm_normalize_eq_one_iff.mpr hy) (norm_normalize_eq_one_iff.mpr hz)
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
hnneg₃ : 0 ≤ Real.sin (angle x z) / ‖y‖
hnonzero : Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ ≠ 0
h₁ :
  angle (NormedSpace.normalize x) (NormedSpace.normalize z) ≠ π →
    angle (NormedSpace.normalize x) (NormedSpace.normalize z) =
        angle (NormedSpace.normalize x) (NormedSpace.normalize y) +
          angle (NormedSpace.normalize y) (NormedSpace.normalize z) →
      Real.sin (angle (NormedSpace.normalize x) (NormedSpace.normalize z)) • NormedSpace.normalize y =
        Real.sin (angle (NormedSpace.normalize y) (NormedSpace.normalize z)) • NormedSpace.normalize x +
          Real.sin (angle (NormedSpace.normalize x) (NormedSpace.normalize y)) • NormedSpace.normalize z
⊢ angle x z ≠ π →
    angle x z = angle x y + angle y z →
      Real.sin (angle x z) • NormedSpace.normalize y =
        Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z

Tactic:
simp only [angle_normalize_right, angle_normalize_left] at h₁

Premises used: InnerProductGeometry.angle_normalize_left, InnerProductGeometry.angle_normalize_right
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
hnneg₃ : 0 ≤ Real.sin (angle x z) / ‖y‖
hnonzero : Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ ≠ 0
h₁ :
  angle x z ≠ π →
    angle x z = angle x y + angle y z →
      Real.sin (angle x z) • NormedSpace.normalize y =
        Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z
⊢ Real.sin (angle x z) • NormedSpace.normalize y =
    Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z

Tactic:
have h₂ := h₁ hxz₁ h
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
hnneg₃ : 0 ≤ Real.sin (angle x z) / ‖y‖
hnonzero : Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ ≠ 0
h₁ :
  angle x z ≠ π →
    angle x z = angle x y + angle y z →
      Real.sin (angle x z) • NormedSpace.normalize y =
        Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z
h₂ :
  Real.sin (angle x z) • NormedSpace.normalize y =
    Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z
simp :
  ∀ (h₂ : (Real.sin (angle x z) * ‖y‖⁻¹) • y = (Real.sin (angle y z) * ‖x‖⁻¹) • x + (Real.sin (angle x y) * ‖z‖⁻¹) • z),
    (Real.sin (angle x z) / ‖y‖) • y = (Real.sin (angle y z) / ‖x‖) • x + (Real.sin (angle x y) / ‖z‖) • z
⊢ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ • y =
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle y z) / ‖x‖) hnneg₁ • x +
      Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x y) / ‖z‖) hnneg₂ • z

Tactic:
simp only [NormedSpace.normalize, ← smul_assoc, smul_eq_mul, Nonneg.mk_smul] at h₂ ⊢

Premises used: smul_assoc, Nonneg.mk_smul, smul_eq_mul, NormedSpace.normalize
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
hnneg₃ : 0 ≤ Real.sin (angle x z) / ‖y‖
hnonzero : Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ ≠ 0
h₁ :
  angle x z ≠ π →
    angle x z = angle x y + angle y z →
      Real.sin (angle x z) • NormedSpace.normalize y =
        Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z
h₂ : (Real.sin (angle x z) * ‖y‖⁻¹) • y = (Real.sin (angle y z) * ‖x‖⁻¹) • x + (Real.sin (angle x y) * ‖z‖⁻¹) • z
⊢ (Real.sin (angle x z) / ‖y‖) • y = (Real.sin (angle y z) / ‖x‖) • x + (Real.sin (angle x y) / ‖z‖) • z

Tactic:
h₂

Premises used: DivInvMonoid.div'
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
hnneg₃ : 0 ≤ Real.sin (angle x z) / ‖y‖
hnonzero : Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ ≠ 0
h₁ :
  angle x z ≠ π →
    angle x z = angle x y + angle y z →
      Real.sin (angle x z) • NormedSpace.normalize y =
        Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z
h₂ : (Real.sin (angle x z) * ‖y‖⁻¹) • y = (Real.sin (angle y z) * ‖x‖⁻¹) • x + (Real.sin (angle x y) * ‖z‖⁻¹) • z
⊢ (Real.sin (angle x z) / ‖y‖) • y = (Real.sin (angle y z) / ‖x‖) • x + (Real.sin (angle x y) / ‖z‖) • z

Tactic:
exact h₂
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
hnneg₃ : 0 ≤ Real.sin (angle x z) / ‖y‖
hnonzero : Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ ≠ 0
h₁ :
  angle x z ≠ π →
    angle x z = angle x y + angle y z →
      Real.sin (angle x z) • NormedSpace.normalize y =
        Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z
h₂ :
  Real.sin (angle x z) • NormedSpace.normalize y =
    Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z
⊢ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ • y =
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle y z) / ‖x‖) hnneg₁ • x +
      Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x y) / ‖z‖) hnneg₂ • z

Tactic:
have h₃ : (⟨_, hnneg₃⟩ : ℝ≥0) • y = (⟨_, hnneg₁⟩ : ℝ≥0) • x + (⟨_, hnneg₂⟩ : ℝ≥0) • z := by
      simp only [NormedSpace.normalize, ← smul_assoc, smul_eq_mul, Nonneg.mk_smul] at h₂ ⊢
      exact h₂
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
hnneg₃ : 0 ≤ Real.sin (angle x z) / ‖y‖
hnonzero : Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ ≠ 0
h₁ :
  angle x z ≠ π →
    angle x z = angle x y + angle y z →
      Real.sin (angle x z) • NormedSpace.normalize y =
        Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z
h₂ :
  Real.sin (angle x z) • NormedSpace.normalize y =
    Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z
h₃ :
  Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x z) / ‖y‖) hnneg₃ • y =
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle y z) / ‖x‖) hnneg₁ • x +
      Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (Real.sin (angle x y) / ‖z‖) hnneg₂ • z
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y

Tactic:
mem_span_of_linear_combination hnonzero h₃

Premises used: _private.0.InnerProductGeometry.mem_span_of_linear_combination