awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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⟫ =
    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)⟫))
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have H6₁ : ⟪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 H6
Cleared hypotheses: H6
-- 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
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⟫ =
    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)⟫)
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have H6₁ : Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y 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: rw [inner_eq_cos_angle_of_norm_eq_one hx hz, H0, Real.cos_add] at H6
Cleared hypotheses: H6
-- 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
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 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)⟫)
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have 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)⟫
Tactic: ring_nf at H6
Cleared hypotheses: H6
-- 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
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)⟫
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have Hw : Real.sin (angle x y) * Real.sin (angle y z) ≠ 0
Tactic: have Hw : Real.sin (angle x y) * Real.sin (angle y 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 (hypothesis)
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
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have H8 : ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫ = -1
Tactic: have H8 : ⟪normalize (ortho y x), normalize (ortho y z)⟫ = -1 := by
    grind
-- 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
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)⟫ = -1
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have H9 : ortho y x ≠ 0
Tactic: have H9 : ortho y x ≠ 0 := by
    grind [ortho_ne_zero_of_not_collinear, angle_comm]
-- 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
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)⟫ = -1
H9 : ortho y x ≠ 0
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have H10 : ortho y z ≠ 0
Tactic: have H10 : ortho y z ≠ 0 := by
    grind [ortho_ne_zero_of_not_collinear]
-- 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
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)⟫ = -1
H9 : ortho y x ≠ 0
H10 : ortho y z ≠ 0
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have H11 : ‖NormedSpace.normalize (ortho y x)‖ = 1
Tactic: have H11 : ‖normalize (ortho y x)‖ = 1 := norm_normalize_eq_one_iff.mpr H9
-- 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
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)⟫ = -1
H9 : ortho y x ≠ 0
H10 : ortho y z ≠ 0
H11 : ‖NormedSpace.normalize (ortho y x)‖ = 1
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have H12 : ‖NormedSpace.normalize (ortho y z)‖ = 1
Tactic: have H12 : ‖normalize (ortho y z)‖ = 1 := norm_normalize_eq_one_iff.mpr H10
-- 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
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)⟫ = -1
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) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have H8₁ : NormedSpace.normalize (ortho y x) = -NormedSpace.normalize (ortho y z)
Tactic: rw [inner_eq_neg_one_iff_of_norm_eq_one H11 H12] at H8
Cleared hypotheses: H8, H9, H10, H11, H12
-- 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
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) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have neg : 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 x)) +
    Real.sin (angle x y) • z
Tactic: nth_rw 2 [angle_le_angle_add_angle_aux hx hy]
-- 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
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) • y =
    Real.sin (angle y z) • (Real.cos (angle x y) • y + Real.sin (angle x y) • NormedSpace.normalize (ortho y x)) +
      Real.sin (angle x y) • z
have neg : 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 x)) +
    Real.sin (angle x y) • (Real.cos (angle z y) • y + Real.sin (angle z y) • NormedSpace.normalize (ortho y z))
Tactic: nth_rw 3 [angle_le_angle_add_angle_aux hz hy]
-- 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
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) • y =
    Real.sin (angle y z) • (Real.cos (angle x y) • y + Real.sin (angle x y) • NormedSpace.normalize (ortho y x)) +
      Real.sin (angle x y) • (Real.cos (angle z y) • y + Real.sin (angle z y) • NormedSpace.normalize (ortho y z))
have neg : 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: rw [H8]
-- 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
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) • 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))
have 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)
Tactic: match_scalars
-- 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
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)
⊢ 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))
have 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)
Tactic: match_scalars
-- 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
⊢ angle x z ≤ angle x y + angle y z
have pos : ∀ (hx : x = 0), angle x z ≤ angle x y + angle y z
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
pos : ∀ (hx : x = 0), angle x z ≤ angle x y + angle y z
⊢ angle x z ≤ angle x y + angle y z
have neg : ∀ (hx : ¬x = 0), angle x z ≤ angle x y + angle y z
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
hx : ¬x = 0
⊢ angle x z ≤ angle x y + angle y z
have pos : ∀ (hy : y = 0), angle x z ≤ angle x y + angle y z
Tactic: by_cases hy : y = 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
hx : ¬x = 0
pos : ∀ (hy : y = 0), angle x z ≤ angle x y + angle y z
⊢ angle x z ≤ angle x y + angle y z
have neg : ∀ (hy : ¬y = 0), angle x z ≤ angle x y + angle y z
Tactic: by_cases hy : y = 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
hx : ¬x = 0
hy : ¬y = 0
⊢ angle x z ≤ angle x y + angle y z
have pos : ∀ (hz : z = 0), angle x z ≤ angle x y + angle y 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 y z : V
hx : ¬x = 0
hy : ¬y = 0
pos : ∀ (hz : z = 0), angle x z ≤ angle x y + angle y z
⊢ angle x z ≤ angle x y + angle y z
have neg : ∀ (hz : ¬z = 0), angle x z ≤ angle x y + angle y 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 y z : V
hy : y ≠ 0
h_mem : Membership.mem (γ := Submodule ℝ≥0 V) (Submodule.span ℝ≥0 {x, z}) y
⊢ angle x z = angle x y + angle y z
have h_mem₁ : ∃ (a : ℝ≥0) (b : ℝ≥0), a • x + b • z = y
Tactic: rw [Submodule.mem_span_pair] at h_mem
Cleared hypotheses: h_mem
-- 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_mem : ∃ (a : ℝ≥0) (b : ℝ≥0), a • x + b • z = y
⊢ angle x z = angle x y + angle y z
have 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
Tactic: obtain ⟨kx, kz, rfl⟩ := h_mem
Cleared hypotheses: y, hy, h_mem
-- 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
⊢ angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z
have 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
Tactic: rcases eq_zero_or_pos kx with rfl | hkx
Cleared hypotheses: kx, hy
-- 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
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
⊢ angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z
have inr : ∀ (hkx : 0 < kx), 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
-- 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
kz : ℝ≥0
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
have 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
Tactic: rcases eq_zero_or_pos kz with rfl | hkz
Cleared hypotheses: kz, hy
-- 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
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
⊢ angle x z = angle x (HSMul.hSMul (α := ℝ≥0) 0 x + kz • z) + angle (HSMul.hSMul (α := ℝ≥0) 0 x + kz • z) z
have 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
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
⊢ angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z
have 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
Tactic: rcases eq_zero_or_pos kz with rfl | hkz
Cleared hypotheses: kz, hy