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 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 :
  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 x y) * Real.sin (angle y z) *
        ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
Hw : Real.sin (angle x y) * Real.sin (angle y z) ≠ 0
H8 : NormedSpace.normalize (ortho y x) = -NormedSpace.normalize (ortho y z)
H9 : ortho y x ≠ 0
H10 : ortho y z ≠ 0
H11 : ‖NormedSpace.normalize (ortho y x)‖ = 1
H12 : ‖NormedSpace.normalize (ortho y z)‖ = 1
match_scalars :
  Real.sin (angle x z) * 1 =
    Real.sin (angle y z) * (Real.cos (angle x y) * 1) + Real.sin (angle x y) * (Real.cos (angle z y) * 1)
match_scalars₁ :
  0 = Real.sin (angle y z) * (Real.sin (angle x y) * -1) + Real.sin (angle x y) * (Real.sin (angle z y) * 1)
⊢ Real.sin (angle x z) • y =
    Real.sin (angle y z) • (Real.cos (angle x y) • y + Real.sin (angle x y) • -NormedSpace.normalize (ortho y z)) +
      Real.sin (angle x y) • (Real.cos (angle z y) • y + Real.sin (angle z y) • NormedSpace.normalize (ortho y z))

Tactic:
match_scalars
-- 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 :
  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 x y) * Real.sin (angle y z) *
        ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
Hw : Real.sin (angle x y) * Real.sin (angle y z) ≠ 0
H8 : NormedSpace.normalize (ortho y x) = -NormedSpace.normalize (ortho y z)
H9 : ortho y x ≠ 0
H10 : ortho y z ≠ 0
H11 : ‖NormedSpace.normalize (ortho y x)‖ = 1
H12 : ‖NormedSpace.normalize (ortho y z)‖ = 1
⊢ Real.sin (angle x z) * 1 =
    Real.sin (angle y z) * (Real.cos (angle x y) * 1) + Real.sin (angle x y) * (Real.cos (angle z y) * 1)

Tactic:
grind [Real.sin_add, angle_comm]

Premises used: Real.sin_add, InnerProductGeometry.angle_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 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 :
  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 x y) * Real.sin (angle y z) *
        ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
Hw : Real.sin (angle x y) * Real.sin (angle y z) ≠ 0
H8 : NormedSpace.normalize (ortho y x) = -NormedSpace.normalize (ortho y z)
H9 : ortho y x ≠ 0
H10 : ortho y z ≠ 0
H11 : ‖NormedSpace.normalize (ortho y x)‖ = 1
H12 : ‖NormedSpace.normalize (ortho y z)‖ = 1
⊢ 0 = Real.sin (angle y z) * (Real.sin (angle x y) * -1) + Real.sin (angle x y) * (Real.sin (angle z y) * 1)

Tactic:
grind [Real.sin_add, angle_comm]

Premises used: Real.sin_add, InnerProductGeometry.angle_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
pos : ∀ (hx : x = 0), angle x z ≤ angle x y + angle y z
neg : ∀ (hx : ¬x = 0), angle x z ≤ angle x y + angle y z
⊢ angle x z ≤ angle x y + angle y z

Tactic:
by_cases hx : x = 0
-- 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 = 0
⊢ angle x z ≤ angle x y + angle y z

Tactic:
simpa [hx] using angle_nonneg y z

Premises used: 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 = 0
pos : ∀ (hy : y = 0), angle x z ≤ angle x y + angle y z
neg : ∀ (hy : ¬y = 0), angle x z ≤ angle x y + angle y z
⊢ angle x z ≤ angle x y + angle y z

Tactic:
by_cases hy : y = 0
-- 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 = 0
hy : y = 0
⊢ angle x z ≤ angle x y + angle y z

Tactic:
simpa [hy] using 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 = 0
hy : ¬y = 0
pos : ∀ (hz : z = 0), angle x z ≤ angle x y + angle y z
neg : ∀ (hz : ¬z = 0), angle x z ≤ angle x y + angle y z
⊢ angle x z ≤ angle x y + angle y z

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
hx : ¬x = 0
hy : ¬y = 0
hz : z = 0
⊢ angle x z ≤ angle x y + angle y z

Tactic:
simpa [hz] using angle_nonneg x y

Premises used: 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 = 0
hy : ¬y = 0
hz : ¬z = 0
⊢ angle x z ≤ angle x y + angle y z

Tactic:
simpa using angle_le_angle_add_angle_of_norm_eq_one (norm_normalize_eq_one_iff.mpr hx)
    (norm_normalize_eq_one_iff.mpr hy) (norm_normalize_eq_one_iff.mpr hz)

Premises used: Iff.mpr, _private.0.InnerProductGeometry.angle_le_angle_add_angle_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
hy : y ≠ 0
h_mem : Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
⊢ ∃ (a : ℝ≥0) (b : ℝ≥0), a • x + b • z = y

Tactic:
rw [Submodule.mem_span_pair] at h_mem

Premises used: Submodule.mem_span_pair
-- 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_mem : ∃ (a : ℝ≥0) (b : ℝ≥0), a • x + b • z = y
obtain : ∀ (kx kz : ℝ≥0) (hy : kx • x + kz • z ≠ 0), angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z
⊢ angle x z = angle x y + angle y z

Tactic:
obtain ⟨kx, kz, rfl⟩ := h_mem

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
inl :
  ∀ (hy : HSMul.hSMul (α := ℝ≥0) 0 x + kz • z ≠ 0),
    angle x z = angle x (HSMul.hSMul (α := ℝ≥0) 0 x + kz • z) + angle (HSMul.hSMul (α := ℝ≥0) 0 x + kz • z) z
inr : ∀ (hkx : 0 < kx), angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z
⊢ angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z

Tactic:
rcases eq_zero_or_pos kx with rfl | hkx

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
kz : ℝ≥0
hy : HSMul.hSMul (α := ℝ≥0) 0 x + kz • z ≠ 0
inl :
  ∀ (hy : HSMul.hSMul (α := ℝ≥0) 0 x + HSMul.hSMul (α := ℝ≥0) 0 z ≠ 0),
    angle x z =
      angle x (HSMul.hSMul (α := ℝ≥0) 0 x + HSMul.hSMul (α := ℝ≥0) 0 z) +
        angle (HSMul.hSMul (α := ℝ≥0) 0 x + HSMul.hSMul (α := ℝ≥0) 0 z) z
inl₁ :
  ∀ (hkz : 0 < kz),
    angle x z = angle x (HSMul.hSMul (α := ℝ≥0) 0 x + kz • z) + angle (HSMul.hSMul (α := ℝ≥0) 0 x + kz • z) z
⊢ angle x z = angle x (HSMul.hSMul (α := ℝ≥0) 0 x + kz • z) + angle (HSMul.hSMul (α := ℝ≥0) 0 x + kz • z) z

Tactic:
rcases eq_zero_or_pos kz with rfl | hkz

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
inr :
  ∀ (hy : kx • x + HSMul.hSMul (α := ℝ≥0) 0 z ≠ 0),
    angle x z = angle x (kx • x + HSMul.hSMul (α := ℝ≥0) 0 z) + angle (kx • x + HSMul.hSMul (α := ℝ≥0) 0 z) z
inr₁ : ∀ (hkz : 0 < kz), angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z
⊢ angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z

Tactic:
rcases eq_zero_or_pos kz with rfl | hkz

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
hy : HSMul.hSMul (α := ℝ≥0) 0 x + HSMul.hSMul (α := ℝ≥0) 0 z ≠ 0
⊢ angle x z =
    angle x (HSMul.hSMul (α := ℝ≥0) 0 x + HSMul.hSMul (α := ℝ≥0) 0 z) +
      angle (HSMul.hSMul (α := ℝ≥0) 0 x + HSMul.hSMul (α := ℝ≥0) 0 z) z

Tactic:
simp at hy
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
kz : ℝ≥0
hy : HSMul.hSMul (α := ℝ≥0) 0 x + kz • z ≠ 0
hkz : 0 < kz
⊢ angle x z = angle x (HSMul.hSMul (α := ℝ≥0) 0 x + kz • z) + angle (HSMul.hSMul (α := ℝ≥0) 0 x + kz • z) z

Tactic:
simp_all [NNReal.smul_def]

Premises used: NNReal.smul_def
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
kx : ℝ≥0
hkx : 0 < kx
hy : kx • x + HSMul.hSMul (α := ℝ≥0) 0 z ≠ 0
⊢ angle x z = angle x (kx • x + HSMul.hSMul (α := ℝ≥0) 0 z) + angle (kx • x + HSMul.hSMul (α := ℝ≥0) 0 z) z

Tactic:
simp_all [NNReal.smul_def]

Premises used: NNReal.smul_def
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
inr : angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)
⊢ angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z

Tactic:
rw [angle_comm (_ + _) z]

Premises used: InnerProductGeometry.angle_comm, HAdd.hAdd
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
pos : ∀ (hz : z ≠ 0), angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)
neg : ∀ (hz : z = 0), angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)
⊢ angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)

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 z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z ≠ 0
⊢ angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)

Tactic:
simpa [hkx, hkz, NNReal.smul_def] using
        angle_eq_angle_add_add_angle_add (kx • x) (smul_ne_zero hkz.ne' hz)

Premises used: smul_ne_zero, LT.lt.ne', NNReal.smul_def, HSMul.hSMul, InnerProductGeometry.angle_eq_angle_add_add_angle_add
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z = 0
⊢ x ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z = 0
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := by simp_all
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z = 0
hx : x ≠ 0
neg : angle z x = angle z (kz • z + kx • x) + angle x (kz • z + kx • x)
⊢ angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)

Tactic:
rw [angle_comm, add_comm, add_comm (kx • x)]

Premises used: add_comm, InnerProductGeometry.angle_comm, HSMul.hSMul
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z = 0
hx : x ≠ 0
⊢ angle z x = angle z (kz • z + kx • x) + angle x (kz • z + kx • x)

Tactic:
simpa [hkx, hkz, NNReal.smul_def] using
        angle_eq_angle_add_add_angle_add (kz • z) (smul_ne_zero hkx.ne' hx)

Premises used: smul_ne_zero, LT.lt.ne', NNReal.smul_def, HSMul.hSMul, InnerProductGeometry.angle_eq_angle_add_add_angle_add
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
kx ky kz : ℝ≥0
hy : ky ≠ 0
hlincomb : ky • y = kx • x + kz • z
rw : ∃ (a : ℝ≥0) (b : ℝ≥0), a • x + b • z = ky • y
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) (ky • y)

Tactic:
rw [Submodule.mem_span_pair]

Premises used: Submodule.mem_span_pair
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
kx ky kz : ℝ≥0
hy : ky ≠ 0
hlincomb : ky • y = kx • x + kz • z
⊢ ∃ (a : ℝ≥0) (b : ℝ≥0), a • x + b • z = ky • y

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
kx ky kz : ℝ≥0
hy : ky ≠ 0
hlincomb : ky • y = kx • x + kz • z
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) (ky • y)

Tactic:
have h₁ : ky • y ∈ Submodule.span ℝ≥0 {x, z} := by
    rw [Submodule.mem_span_pair]; grind
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
kx ky kz : ℝ≥0
hy : ky ≠ 0
hlincomb : ky • y = kx • x + kz • z
h₁ : Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) (ky • y)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h₁ : Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y),
    Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y

Tactic:
rwa [Submodule.smul_mem_iff _ hy] at h₁

Premises used: Submodule.smul_mem_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
mp :
  angle x z = angle x y + angle y z →
    angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
mpr :
  angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y →
    angle x z = angle x y + angle y z
⊢ angle x z = angle x y + angle y z ↔
    angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y

Tactic:
constructor
-- 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
pos : ∀ (hxz₁ : angle x z = π), angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
neg : ∀ (hxz₁ : ¬angle x z = π), angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
⊢ angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y

Tactic:
by_cases hxz₁ : angle x 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
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : angle x z = π
pos : ¬angle x z = π → Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
pos₁ :
  ¬angle x z = π →
    ∀ (t : Set V),
      Membership.mem (γ := Set (Set V))
          (Set.range fun (s : Submodule ℝ≥0 V) ↦
            ⋂ (_ : Membership.mem (γ := Set (Submodule ℝ≥0 V)) {p : Submodule ℝ≥0 V | {x, z} ⊆ (↑p : Set V)} s),
              (↑s : Set V))
          t →
        y ∈ t
⊢ angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y

Tactic:
tauto
-- 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 = π
neg : Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
⊢ angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y

Tactic:
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 = π
pos : ∀ (hxz₂ : angle x z = 0), Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
neg : ∀ (hxz₂ : ¬angle x 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 hxz₂ : 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
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : angle x z = 0
⊢ angle x y = 0

Tactic:
grind [angle_nonneg]

Premises used: 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
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : angle x z = 0
⊢ angle x y = 0

Tactic:
have hxy : angle x y = 0 := by grind [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
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : angle x z = 0
hxy : angle x y = 0
⊢ x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ z = r • x

Tactic:
rw [angle_eq_zero_iff] at hxy hxz₂

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 z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : angle x z = 0
hxy : angle x y = 0
hxz₃ : x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ z = r • x
⊢ x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x

Tactic:
rw [angle_eq_zero_iff] at hxy hxz₂

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 z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ z = r • x
hxy : x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x
pos :
  x ≠ 0 →
    ∀ (r2 : ℝ) (hr2 : 0 < r2) (hy : r2 • x ≠ 0) (h : angle x z = angle x (r2 • x) + angle (r2 • x) z),
      Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) (r2 • x)
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y

Tactic:
obtain ⟨_, ⟨r2, ⟨hr2, rfl⟩⟩⟩ := hxy

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
hxz₁ : ¬angle x z = π
hxz₂ : x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ z = r • x
left : x ≠ 0
r2 : ℝ
hr2 : 0 < r2
hy : r2 • x ≠ 0
h : angle x z = angle x (r2 • x) + angle (r2 • x) z
⊢ 0 ≤ r2

Tactic:
hr2.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 z : V
hxz₁ : ¬angle x z = π
hxz₂ : x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ z = r • x
left : x ≠ 0
r2 : ℝ
hr2 : 0 < r2
hy : r2 • x ≠ 0
h : angle x z = angle x (r2 • x) + angle (r2 • x) z
pos :
  ∀ (r2 : ℝ≥0) (hr2 : 0 < (↑r2 : ℝ)) (hy : (↑r2 : ℝ) • x ≠ 0)
    (h : angle x z = angle x ((↑r2 : ℝ) • x) + angle ((↑r2 : ℝ) • x) z),
    Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) ((↑r2 : ℝ) • x)
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) (r2 • x)

Tactic:
lift r2 to ℝ≥0 using hr2.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 z : V
hxz₁ : ¬angle x z = π
hxz₂ : x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ z = r • x
left : x ≠ 0
r2 : ℝ≥0
hr2 : 0 < (↑r2 : ℝ)
hy : (↑r2 : ℝ) • x ≠ 0
h : angle x z = angle x ((↑r2 : ℝ) • x) + angle ((↑r2 : ℝ) • x) z
⊢ Membership.mem (γ := Set V) {x, z} x

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
hxz₁ : ¬angle x z = π
hxz₂ : x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ z = r • x
left : x ≠ 0
r2 : ℝ≥0
hr2 : 0 < (↑r2 : ℝ)
hy : (↑r2 : ℝ) • x ≠ 0
h : angle x z = angle x ((↑r2 : ℝ) • x) + angle ((↑r2 : ℝ) • x) z
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) ((↑r2 : ℝ) • 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
⊢ 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
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
⊢ Real.sin (angle x z) ≠ 0

Tactic:
have h_sin_xz : 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
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
pos : ∀ (hx : x = 0), Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
neg : ∀ (hx : ¬x = 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 hx : x = 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
pos :
  ∀ (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), Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {0, z}) y
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y

Tactic:
subst x