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 y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
this : Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z)
H0 : 0 ≤ angle x y + angle y z
⊢ angle x z ≤ angle x y + angle y z
have rwa : ∀ (this : angle x z ≤ angle x y + angle y z) (H0 : 0 ≤ angle x y + angle y z), angle x z ≤ angle x y + angle y z
Tactic: rwa [Real.strictAntiOn_cos.le_iff_ge ⟨H0, H⟩ ⟨angle_nonneg x z, angle_le_pi x z⟩] at this
Cleared hypotheses: this, H0
-- 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 y + angle y z ≤ π
⊢ angle x z ≤ angle x y + angle y z
have inr : Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z)
Tactic: suffices Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z) by
    have H0 : 0 ≤ angle x y + angle y z :=
      add_nonneg (angle_nonneg x y) (angle_nonneg y z)
    rwa [Real.strictAntiOn_cos.le_iff_ge ⟨H0, H⟩ ⟨angle_nonneg x z, angle_le_pi x z⟩] at this
-- 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 y + angle y z ≤ π
⊢ Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z)
have H1 : ⟪x, z⟫ = ⟪x, z⟫
Tactic: have H1 : ⟪x, z⟫ = ⟪x, z⟫ := rfl
-- 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 y + angle y z ≤ π
H1 : ⟪x, z⟫ = ⟪x, z⟫
⊢ Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z)
have H1₁ : ⟪x, z⟫ =
  ⟪Real.cos (angle x y) • y + Real.sin (angle x y) • NormedSpace.normalize (ortho y x),
    Real.cos (angle z y) • y + Real.sin (angle z y) • NormedSpace.normalize (ortho y z)⟫
Tactic: nth_rw 2 [angle_le_angle_add_angle_aux hx hy, angle_le_angle_add_angle_aux hz hy] at H1
Cleared hypotheses: H1
-- 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 y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    ⟪Real.cos (angle x y) • y + Real.sin (angle x y) • NormedSpace.normalize (ortho y x),
      Real.cos (angle z y) • y + Real.sin (angle z y) • NormedSpace.normalize (ortho y z)⟫
⊢ Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z)
have H1₁ : ⟪x, z⟫ =
  Real.cos (angle y z) * (Real.cos (angle x y) * HPow.hPow (α := ℝ) (β := ℕ) 1 2) +
      Real.cos (angle y z) * (Real.sin (angle x y) * 0) +
    (Real.sin (angle y z) * (Real.cos (angle x y) * 0) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫))
Tactic: simp only [inner_add_left, inner_add_right, real_inner_smul_left, real_inner_smul_right,
    real_inner_comm y (normalize _), real_inner_self_eq_norm_sq, hy, angle_comm z y,
    inner_normalize_ortho] at H1
Cleared hypotheses: H1
-- 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 y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle y z) * (Real.cos (angle x y) * HPow.hPow (α := ℝ) (β := ℕ) 1 2) +
        Real.cos (angle y z) * (Real.sin (angle x y) * 0) +
      (Real.sin (angle y z) * (Real.cos (angle x y) * 0) +
        Real.sin (angle y z) *
          (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫))
⊢ Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z)
have H1₁ : ⟪x, z⟫ =
  Real.cos (angle y z) * Real.cos (angle x y) +
    Real.sin (angle y z) *
      (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
Tactic: simp only [one_pow, mul_one, mul_zero, add_zero, zero_add] at H1
Cleared hypotheses: H1
-- 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 y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle y z) * Real.cos (angle x y) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
⊢ Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z)
have H1₁ : ⟪x, z⟫ =
  Real.cos (angle x y) * Real.cos (angle y z) +
    Real.sin (angle y z) *
      (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
Tactic: rw [mul_comm (Real.cos (angle y z))] at H1
Cleared hypotheses: H1
-- 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 y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
⊢ Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z)
have inr : Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) ≤
  Real.cos (angle x y) * Real.cos (angle y z) +
    Real.sin (angle y z) *
      (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
Tactic: rw [Real.cos_add, ← inner_eq_cos_angle_of_norm_eq_one hx hz, H1]
-- 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 y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
⊢ -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
have pos : ∀ (H3 : ortho y x = 0), -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
Tactic: by_cases H3 : ortho y 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‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
pos : ∀ (H3 : ortho y x = 0), -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
⊢ -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
have neg : ∀ (H3 : ¬ortho y x = 0), -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
Tactic: by_cases H3 : ortho y 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‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H3 : ¬ortho y x = 0
⊢ -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
have pos : ∀ (H4 : ortho y z = 0), -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
Tactic: by_cases H4 : ortho y 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‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H3 : ¬ortho y x = 0
pos : ∀ (H4 : ortho y z = 0), -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
⊢ -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
have neg : ∀ (H4 : ¬ortho y z = 0), -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
Tactic: by_cases H4 : ortho y 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
⊢ Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) ≤
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
have H2 : -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
Tactic: have H2 : -1 ≤ ⟪normalize (ortho y x), normalize (ortho y z)⟫ := by
    by_cases H3 : ortho y x = 0
    · simp [*]
    by_cases H4 : ortho y z = 0
    · simp [*]
    exact neg_one_le_real_inner_of_norm_eq_one
      (norm_normalize_eq_one_iff.mpr H3) (norm_normalize_eq_one_iff.mpr H4)
-- 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 y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H2 : -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
⊢ Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) ≤
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
have this : 0 ≤ Real.sin (angle x y)
Tactic: have := sin_angle_nonneg x y
-- 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 y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H2 : -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
this : 0 ≤ Real.sin (angle x y)
⊢ Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) ≤
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
have this₁ : 0 ≤ Real.sin (angle y z)
Tactic: have := sin_angle_nonneg y 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H2 : -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
this_1 : 0 ≤ Real.sin (angle x y)
this : 0 ≤ Real.sin (angle y z)
⊢ Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) ≤
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
have inr : Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) ≤
  Real.cos (angle x y) * Real.cos (angle y z) + Real.sin (angle y z) * (Real.sin (angle x y) * -1)
Tactic: grw [← H2]
-- 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 y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
H2 : -1 ≤ ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
this_1 : 0 ≤ Real.sin (angle x y)
this : 0 ≤ Real.sin (angle y z)
⊢ Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) ≤
    Real.cos (angle x y) * Real.cos (angle y z) + Real.sin (angle y z) * (Real.sin (angle x y) * -1)
have inr : Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) =
  Real.cos (angle x y) * Real.cos (angle y z) + Real.sin (angle y z) * (Real.sin (angle x y) * -1)
Tactic: apply le_of_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
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy1 : angle x y ≠ 0
hxy2 : angle x y ≠ π
h : ortho x y = 0
⊢ False
have h₁ : y = ⟪x, y⟫ • x
Tactic: rw [ortho_eq_sub_inner _ hx, sub_eq_zero] 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have pos : ∀ (H1 : angle x z = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Tactic: by_cases H1 : angle x z = 0
-- 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
pos : ∀ (H1 : angle x z = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have neg : ∀ (H1 : ¬angle x z = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Tactic: by_cases H1 : angle x z = 0
-- 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
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have Hxz : Real.sin (angle x z) ≠ 0
Tactic: have Hxz : Real.sin (angle x z) ≠ 0 := by
    grind [sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi]
-- 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
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have pos : ∀ (H2 : angle x y = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Tactic: by_cases H2 : angle x y = 0
-- 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
pos : ∀ (H2 : angle x y = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have neg : ∀ (H2 : ¬angle x y = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Tactic: by_cases H2 : angle x y = 0
-- 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
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have pos : ∀ (H3 : angle y z = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Tactic: by_cases H3 : angle y z = 0
-- 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
pos : ∀ (H3 : angle y z = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have neg : ∀ (H3 : ¬angle y z = 0), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Tactic: by_cases H3 : angle y z = 0
-- 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
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have pos : ∀ (H4 : angle x y = π), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Tactic: by_cases H4 : angle x y = π
-- 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
pos : ∀ (H4 : angle x y = π), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have neg : ∀ (H4 : ¬angle x y = π), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Tactic: by_cases H4 : angle x y = π
-- 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 = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have pos : ∀ (H5 : angle y z = π), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Tactic: by_cases H5 : angle y z = π
-- 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 = π
pos : ∀ (H5 : angle y z = π), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have neg : ∀ (H5 : ¬angle y z = π), Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Tactic: by_cases H5 : angle y z = π
-- 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 = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
have H6 : ⟪x, z⟫ = ⟪x, z⟫
Tactic: have H6 : ⟪x, z⟫ = ⟪x, z⟫ := rfl
-- 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⟫ = ⟪x, 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 x y) • y + Real.sin (angle x y) • NormedSpace.normalize (ortho y x),
    Real.cos (angle z y) • y + Real.sin (angle z y) • NormedSpace.normalize (ortho y z)⟫
Tactic: nth_rw 2 [angle_le_angle_add_angle_aux hx hy, angle_le_angle_add_angle_aux hz hy] at H6
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 x y) • y + Real.sin (angle x y) • NormedSpace.normalize (ortho y x),
      Real.cos (angle z y) • y + Real.sin (angle z y) • NormedSpace.normalize (ortho y z)⟫
⊢ 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) * HPow.hPow (α := ℝ) (β := ℕ) 1 2) +
      Real.cos (angle y z) * (Real.sin (angle x y) * 0) +
    (Real.sin (angle y z) * (Real.cos (angle x y) * 0) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫))
Tactic: simp only [inner_add_left, inner_add_right, real_inner_smul_left, real_inner_smul_right,
             real_inner_comm y (normalize _), real_inner_self_eq_norm_sq, hy, angle_comm z y,
             inner_normalize_ortho] at H6
Cleared hypotheses: H6