awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z
have inr₁ : ∀ (hkz : 0 < kz), 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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z
have inr : angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)
Tactic: rw [angle_comm (_ + _) z]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)
have pos : ∀ (hz : z ≠ 0), angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)
Tactic: by_cases! hz : z ≠ 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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)
⊢ angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)
have neg : ∀ (hz : z = 0), angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)
Tactic: by_cases! hz : z ≠ 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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)
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := by simp_all
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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 x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)
have neg : angle z x = angle z (kz • z + kx • x) + angle x (kz • z + kx • x)
Tactic: rw [angle_comm, add_comm, add_comm (kx • x)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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)
have rw : ∃ (a : ℝ≥0) (b : ℝ≥0), a • x + b • z = ky • y
Tactic: rw [Submodule.mem_span_pair]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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}) y
have h₁ : 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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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)
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have rwa : ∀ (h₁ : 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₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
⊢ angle x z = angle x y + angle y z ↔
    angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have mp : 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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ angle x z = angle x y + angle y z ↔
    angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have mpr : angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y → angle x z = angle x y + angle y z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have pos : ∀ (hxz₁ : angle x z = π), angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
Tactic: by_cases hxz₁ : angle x z = π
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have neg : ∀ (hxz₁ : ¬angle x z = π), angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
Tactic: by_cases hxz₁ : angle x z = π
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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 = π
⊢ angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have pos : ¬angle x z = π → Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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 = π
⊢ angle x z = π ∨ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have neg : Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
Tactic: right
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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 = π
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have pos : ∀ (hxz₂ : angle x z = 0), Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
Tactic: by_cases hxz₂ : angle x z = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have neg : ∀ (hxz₂ : ¬angle x z = 0), Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
Tactic: by_cases hxz₂ : angle x z = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have hxy : angle x y = 0
Tactic: have hxy : angle x y = 0 := by grind [angle_nonneg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have hxz₃ : x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ z = r • x
Tactic: rw [angle_eq_zero_iff] at hxy hxz₂
Cleared hypotheses: hxz₂, hxy
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have hxy₁ : x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x
Tactic: rw [angle_eq_zero_iff] at hxy hxz₂
Cleared hypotheses: hxz₂, hxy
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have 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)
Tactic: obtain ⟨_, ⟨r2, ⟨hr2, rfl⟩⟩⟩ := hxy
Cleared hypotheses: y, hy, h, hxy
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) (r2 • x)
have 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)
Tactic: lift r2 to ℝ≥0 using hr2.le
Cleared hypotheses: r2, hr2, hy, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have h_sin_xz : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have pos : ∀ (hx : x = 0), Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have neg : ∀ (hx : ¬x = 0), Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have 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
Tactic: subst x
Cleared hypotheses: x, h, hxz₁, hxz₂, h_sin_xz, hx
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {0, z}) y
have h₁ : angle y z = 0
Tactic: simp only [angle_zero_left, left_eq_add] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {0, z}) y
have h₁ : y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ z = r • y
Tactic: rw [angle_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {0, z}) y
have 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
Tactic: obtain ⟨_, ⟨r, ⟨hr, rfl⟩⟩⟩ := h
Cleared hypotheses: z, hxz₁, hxz₂, h_sin_xz, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {0, r • y}) y
have 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
Tactic: lift r to ℝ≥0 using hr.le
Cleared hypotheses: r, hr, hxz₁, hxz₂, h_sin_xz
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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) (Submodule.span ℝ≥0 {0, (↑r : ℝ) • y}) y
have pos : Membership.mem (γ := Submodule ℝ≥0 V) (ℝ≥0 ∙ y) y
Tactic: rw [← NNReal.smul_def, Submodule.span_insert_zero, Submodule.span_singleton_smul_eq]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {0, (↑r : ℝ) • y}) y
have pos₁ : IsUnit r
Tactic: rw [← NNReal.smul_def, Submodule.span_insert_zero, Submodule.span_singleton_smul_eq]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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
⊢ IsUnit r
have hr₁ : 0 < r
Tactic: norm_cast at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have pos : ∀ (hz : z = 0), Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
Tactic: by_cases hz : z = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have neg : ∀ (hz : ¬z = 0), Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
Tactic: by_cases hz : z = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have 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
Tactic: subst z
Cleared hypotheses: z, h, hxz₁, hxz₂, h_sin_xz, hz
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, 0}) y
have h₁ : angle x y = 0
Tactic: simp only [angle_zero_right, right_eq_add] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, 0}) y
have h₁ : x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x
Tactic: rw [angle_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, 0}) y
have pos : x ≠ 0 →
  ∀ (r : ℝ) (hr : 0 < r) (hy : r • x ≠ 0), Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, 0}) (r • x)
Tactic: obtain ⟨_, ⟨r, ⟨hr, rfl⟩⟩⟩ := h
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, 0}) (r • x)
have pos : ∀ (r : ℝ≥0) (hr : 0 < (↑r : ℝ)) (hy : (↑r : ℝ) • x ≠ 0),
  Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, 0}) ((↑r : ℝ) • x)
Tactic: lift r to ℝ≥0 using hr.le
Cleared hypotheses: r, hr, hy
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have hnneg₁ : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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‖
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have hnneg₂ : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (hypothesis)
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‖
⊢ Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
have hnneg₃ : 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]