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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
grw : HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≤ 1
grw₁ : |⟪x, y⟫| ≤ 1
⊢ ⟪x, y⟫ * ⟪x, y⟫ ≤ 1
have grw₂ : ‖x‖ * ‖y‖ ≤ 1
Tactic: grw [← sq, sq_le_one_iff_abs_le_one, abs_real_inner_le_norm, hx, hy, one_mul]
-- 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
grw : HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≤ 1
grw₁ : |⟪x, y⟫| ≤ 1
grw₂ : ‖x‖ * ‖y‖ ≤ 1
⊢ ⟪x, y⟫ * ⟪x, y⟫ ≤ 1
have grw₃ : 1 * ‖y‖ ≤ 1
Tactic: grw [← sq, sq_le_one_iff_abs_le_one, abs_real_inner_le_norm, hx, hy, one_mul]
-- 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
grw : HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≤ 1
grw₁ : |⟪x, y⟫| ≤ 1
grw₂ : ‖x‖ * ‖y‖ ≤ 1
grw₃ : 1 * ‖y‖ ≤ 1
⊢ ⟪x, y⟫ * ⟪x, y⟫ ≤ 1
have grw₄ : HMul.hMul (α := ℝ) 1 1 ≤ 1
Tactic: grw [← sq, sq_le_one_iff_abs_le_one, abs_real_inner_le_norm, hx, hy, one_mul]
-- 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
grw : HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≤ 1
grw₁ : |⟪x, y⟫| ≤ 1
grw₂ : ‖x‖ * ‖y‖ ≤ 1
grw₃ : 1 * ‖y‖ ≤ 1
grw₄ : HMul.hMul (α := ℝ) 1 1 ≤ 1
⊢ ⟪x, y⟫ * ⟪x, y⟫ ≤ 1
have grw₅ : LE.le (α := ℝ) 1 1
Tactic: grw [← sq, sq_le_one_iff_abs_le_one, abs_real_inner_le_norm, hx, hy, one_mul]
-- 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
⊢ ⟪y, NormedSpace.normalize (ortho y x)⟫ = 0
have simp : ortho y x = 0 ∨ ⟪y, ortho y x⟫ = 0
Tactic: simp only [NormedSpace.normalize, real_inner_smul_right, mul_eq_zero, inv_eq_zero, norm_eq_zero]
-- 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
⊢ ortho y x = 0 ∨ ⟪y, ortho y x⟫ = 0
have h : ⟪y, ortho y x⟫ = 0
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 : V
⊢ ⟪y, ortho y x⟫ = 0
have h : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ y) y
Tactic: rw [ortho, real_inner_comm, Submodule.starProjection_inner_eq_zero]
-- 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ HPow.hPow (β := ℕ) ⟪x, NormedSpace.normalize (ortho y x)⟫ 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
have rw : HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
Tactic: rw [NormedSpace.normalize, real_inner_smul_right, ortho_eq_sub_inner _ hy, inner_sub_right,
    real_inner_smul_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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
have pos : ∀ (h₁ : x = y), HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
Tactic: by_cases h₁ : 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
pos :
  ∀ (h₁ : x = y),
    HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
⊢ HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
have neg : ∀ (h₁ : ¬x = y),
  HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
Tactic: by_cases h₁ : 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
⊢ HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
have pos : ∀ (h₂ : x = -y),
  HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
Tactic: by_cases h₂ : 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
pos :
  ∀ (h₂ : x = -y),
    HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
⊢ HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
have neg : ∀ (h₂ : ¬x = -y),
  HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
Tactic: by_cases h₂ : 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
⊢ HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
have neg : HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (HPow.hPow (α := ℝ) (β := ℕ) 1 2 - ⟪y, x⟫ * ⟪x, y⟫)) 2 +
    HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
  1
Tactic: rw [real_inner_self_eq_norm_sq, hx]
-- 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
⊢ ‖x - ⟪y, x⟫ • y‖ ≠ 0
have simp : ¬x = ⟪y, x⟫ • y
Tactic: simp only [ne_eq, norm_eq_zero, sub_eq_zero]
-- 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
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
⊢ False
have hx₁ : |⟪y, x⟫| = 1
Tactic: rw [H2, norm_smul, hy, Real.norm_eq_abs, mul_one] at hx
Cleared hypotheses: hx, hy, h₁, h₂, 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 : V
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
hx : ⟪y, x⟫ = 1 ∨ ⟪y, x⟫ = -1
⊢ False
have inl : ∀ (hx : ⟪y, x⟫ = 1), False
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- 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‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
hx : ⟪y, x⟫ = 1 ∨ ⟪y, x⟫ = -1
inl : ∀ (hx : ⟪y, x⟫ = 1), False
⊢ False
have inr : ∀ (hx : ⟪y, x⟫ = -1), False
Tactic: rcases hx with hx | hx
Cleared hypotheses: 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
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
⊢ HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (HPow.hPow (α := ℝ) (β := ℕ) 1 2 - ⟪y, x⟫ * ⟪x, y⟫)) 2 +
      HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
    1
have H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
Tactic: have H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0 := by
    simp only [ne_eq, norm_eq_zero, sub_eq_zero]
    intro H2
    rw [H2, norm_smul, hy, Real.norm_eq_abs, mul_one] at hx
    apply eq_or_eq_neg_of_abs_eq at hx
    rcases hx with hx | hx <;> simp [*] at 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
⊢ HPow.hPow (β := ℕ) (1 - ⟪y, x⟫ * ⟪x, y⟫) 2 + HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2 * HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
    HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2
have rw : HPow.hPow (β := ℕ) (1 - ⟪x, y⟫ * ⟪x, y⟫) 2 +
    (HPow.hPow (α := ℝ) (β := ℕ) 1 2 - ⟪x, y⟫ * ⟪x, y⟫ -
        (⟪x, y⟫ * ⟪x, y⟫ - ⟪x, y⟫ * (⟪x, y⟫ * HPow.hPow (α := ℝ) (β := ℕ) 1 2))) *
      HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
  HPow.hPow (α := ℝ) (β := ℕ) 1 2 - ⟪x, y⟫ * ⟪x, y⟫ -
    (⟪x, y⟫ * ⟪x, y⟫ - ⟪x, y⟫ * (⟪x, y⟫ * HPow.hPow (α := ℝ) (β := ℕ) 1 2))
Tactic: rw [← real_inner_self_eq_norm_sq, inner_sub_left, inner_sub_right, inner_sub_right,
    real_inner_smul_right, real_inner_smul_left, real_inner_smul_right, real_inner_smul_left,
    real_inner_comm x y, real_inner_self_eq_norm_sq, hx, real_inner_self_eq_norm_sq, 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
⊢ HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (HPow.hPow (α := ℝ) (β := ℕ) 1 2 - ⟪y, x⟫ * ⟪x, y⟫)) 2 +
      HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
    1
have H2 : HPow.hPow (β := ℕ) (1 - ⟪y, x⟫ * ⟪x, y⟫) 2 + HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2 * HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
  HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2
Tactic: have H2 : (1 - ⟪y, x⟫ * ⟪x, y⟫) ^ 2 + ‖x - ⟪y, x⟫ • y‖ ^ 2 * ⟪x, y⟫ ^ 2 =
      ‖x - ⟪y, x⟫ • y‖ ^ 2 := by
    rw [← real_inner_self_eq_norm_sq, inner_sub_left, inner_sub_right, inner_sub_right,
    real_inner_smul_right, real_inner_smul_left, real_inner_smul_right, real_inner_smul_left,
    real_inner_comm x y, real_inner_self_eq_norm_sq, hx, real_inner_self_eq_norm_sq, hy]
    ring
-- 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
⊢ ⟪x, NormedSpace.normalize (ortho y x)⟫ = Real.sin (angle x y)
have H : HPow.hPow (β := ℕ) ⟪x, NormedSpace.normalize (ortho y x)⟫ 2 = HPow.hPow (β := ℕ) (Real.sin (angle x y)) 2
Tactic: have H : ⟪x, normalize (ortho y x)⟫ ^ 2 = Real.sin (angle x y) ^ 2 := by
    simp [Real.sin_sq, ← inner_eq_cos_angle_of_norm_eq_one hx hy,
      ← inner_normalized_ortho_sq_add_inner_sq_eq_one hx 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
H : HPow.hPow (β := ℕ) ⟪x, NormedSpace.normalize (ortho y x)⟫ 2 = HPow.hPow (β := ℕ) (Real.sin (angle x y)) 2
⊢ ⟪x, NormedSpace.normalize (ortho y x)⟫ = Real.sin (angle x y)
have H₁ : |⟪x, NormedSpace.normalize (ortho y x)⟫| = Real.sin (angle x y)
Tactic: rw [sq_eq_sq_iff_abs_eq_abs, abs_of_nonneg (sin_angle_nonneg x y)] 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
H : |⟪x, NormedSpace.normalize (ortho y x)⟫| = Real.sin (angle x y)
⊢ 0 ≤ ⟪x, NormedSpace.normalize (ortho y x)⟫
have rw : 0 ≤ ‖ortho y x‖⁻¹ * ⟪x, ortho y x⟫
Tactic: rw [NormedSpace.normalize, real_inner_smul_right]
-- 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
H : |⟪x, NormedSpace.normalize (ortho y x)⟫| = Real.sin (angle x y)
⊢ ⟪x, NormedSpace.normalize (ortho y x)⟫ = Real.sin (angle x y)
have H0 : 0 ≤ ⟪x, NormedSpace.normalize (ortho y x)⟫
Tactic: have H0 : 0 ≤ ⟪x, normalize (ortho y x)⟫ := by
    rw [NormedSpace.normalize, real_inner_smul_right]
    exact Left.mul_nonneg (inv_nonneg_of_nonneg (norm_nonneg (ortho y x)))
      (inner_ortho_nonneg 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ x = Real.cos (angle x y) • y + Real.sin (angle x y) • NormedSpace.normalize (ortho y x)
have rw : x = ⟪x, y⟫ • y + ⟪x, NormedSpace.normalize (x - ⟪y, x⟫ • y)⟫ • NormedSpace.normalize (x - ⟪y, x⟫ • y)
Tactic: rw [← inner_ortho_right_eq_sin_angle hx hy, ← inner_eq_cos_angle_of_norm_eq_one hx hy,
    ortho_eq_sub_inner _ 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ x = ⟪x, y⟫ • y + ⟪x, NormedSpace.normalize (x - ⟪y, x⟫ • y)⟫ • NormedSpace.normalize (x - ⟪y, x⟫ • y)
have pos : ∀ (hxy : x - ⟪x, y⟫ • y = 0),
  x = ⟪x, y⟫ • y + ⟪x, NormedSpace.normalize (x - ⟪y, x⟫ • y)⟫ • NormedSpace.normalize (x - ⟪y, x⟫ • y)
Tactic: by_cases hxy : x - ⟪x, y⟫ • 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
pos :
  ∀ (hxy : x - ⟪x, y⟫ • y = 0),
    x = ⟪x, y⟫ • y + ⟪x, NormedSpace.normalize (x - ⟪y, x⟫ • y)⟫ • NormedSpace.normalize (x - ⟪y, x⟫ • y)
⊢ x = ⟪x, y⟫ • y + ⟪x, NormedSpace.normalize (x - ⟪y, x⟫ • y)⟫ • NormedSpace.normalize (x - ⟪y, x⟫ • y)
have neg : ∀ (hxy : ¬x - ⟪x, y⟫ • y = 0),
  x = ⟪x, y⟫ • y + ⟪x, NormedSpace.normalize (x - ⟪y, x⟫ • y)⟫ • NormedSpace.normalize (x - ⟪y, x⟫ • y)
Tactic: by_cases hxy : x - ⟪x, y⟫ • 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ x = ⟪x, y⟫ • y + ⟪x, NormedSpace.normalize (x - ⟪y, x⟫ • y)⟫ • NormedSpace.normalize (x - ⟪y, x⟫ • y)
have neg : x =
  ⟪y, x⟫ • y +
    (‖x - ⟪y, x⟫ • y‖⁻¹ • (HPow.hPow (α := ℝ) (β := ℕ) 1 2 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2)) •
      ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)
Tactic: rw [NormedSpace.normalize, real_inner_smul_right, inner_sub_right, real_inner_smul_right,
    real_inner_self_eq_norm_sq, hx, real_inner_comm y, ← sq, mul_smul, ← smul_assoc]
-- 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ x =
    ⟪y, x⟫ • y +
      (‖x - ⟪y, x⟫ • y‖⁻¹ • (HPow.hPow (α := ℝ) (β := ℕ) 1 2 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2)) •
        ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)
have neg : x = ⟪y, x⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * (1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2)) • ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)
Tactic: simp only [one_pow, smul_eq_mul]
-- 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
have rw : ⟪x, y⟫ ≠ 1 ∧ ⟪x, y⟫ ≠ -1
Tactic: rw [sub_ne_zero, ne_comm, sq_ne_one_iff]
-- 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ ⟪x, y⟫ ≠ 1 ∧ ⟪x, y⟫ ≠ -1
have left : ⟪x, y⟫ ≠ 1
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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
left : ⟪x, y⟫ ≠ 1
⊢ ⟪x, y⟫ ≠ 1 ∧ ⟪x, y⟫ ≠ -1
have right : ⟪x, y⟫ ≠ -1
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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ ⟪x, y⟫ ≠ 1
have left : ∀ (hxy : ⟪x, y⟫ = 1), x - ⟪x, y⟫ • y = 0
Tactic: contrapose hxy
Cleared hypotheses: 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ ⟪x, y⟫ ≠ -1
have right : ∀ (hxy : ⟪x, y⟫ = -1), x - ⟪x, y⟫ • y = 0
Tactic: contrapose hxy
Cleared hypotheses: 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ⟪x, y⟫ = 1
⊢ x - ⟪x, y⟫ • y = 0
have hxy₁ : x = y
Tactic: rw [inner_eq_one_iff_of_norm_eq_one hx hy] at hxy
Cleared hypotheses: 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ⟪x, y⟫ = -1
⊢ x - ⟪x, y⟫ • y = 0
have hxy₁ : x = -y
Tactic: rw [inner_eq_neg_one_iff_of_norm_eq_one hx hy] at hxy
Cleared hypotheses: 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ x = ⟪y, x⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * (1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2)) • ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)
have H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
Tactic: have H : 1 - ⟪x, y⟫ ^ 2 ≠ 0 := by
    rw [sub_ne_zero, ne_comm, sq_ne_one_iff]
    constructor <;> contrapose hxy
    · rw [inner_eq_one_iff_of_norm_eq_one hx hy] at hxy
      simp [hy, hxy]
    · rw [inner_eq_neg_one_iff_of_norm_eq_one hx hy] at hxy
      simp [hy, 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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
⊢ x = ⟪y, x⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * (1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2)) • ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)
have neg : x = ⟪y, x⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * (1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2) * ‖x - ⟪y, x⟫ • y‖⁻¹) • (x - ⟪y, x⟫ • y)
Tactic: rw [← smul_assoc, smul_eq_mul]
-- 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
⊢ x = ⟪y, x⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * (1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2) * ‖x - ⟪y, x⟫ • y‖⁻¹) • (x - ⟪y, x⟫ • y)
have neg : x = ⟪y, x⟫ • y + ((1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2) / HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2) • (x - ⟪y, x⟫ • y)
Tactic: field_simp
-- 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
⊢ x = ⟪y, x⟫ • y + ((1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2) / HPow.hPow (β := ℕ) ‖x - ⟪y, x⟫ • y‖ 2) • (x - ⟪y, x⟫ • y)
have neg : x = ⟪y, x⟫ • y + ((1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2) / ⟪x - ⟪y, x⟫ • y, x - ⟪y, x⟫ • y⟫) • (x - ⟪y, x⟫ • y)
Tactic: rw [← real_inner_self_eq_norm_sq]
-- 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
⊢ ⟪x - ⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2
have rw : 1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2 - (⟪y, x⟫ * ⟪y, x⟫ - ⟪y, x⟫ * (⟪y, x⟫ * 1)) = 1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2
Tactic: rw [inner_sub_left, inner_sub_right, inner_sub_right, inner_self_eq_one_of_norm_eq_one hx,
      real_inner_smul_right, ← sq, real_inner_smul_left, real_inner_smul_left,
      real_inner_smul_right, inner_self_eq_one_of_norm_eq_one hy, real_inner_comm y x]
-- 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
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
⊢ x = ⟪y, x⟫ • y + ((1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2) / ⟪x - ⟪y, x⟫ • y, x - ⟪y, x⟫ • y⟫) • (x - ⟪y, x⟫ • y)
have H0 : ⟪x - ⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2
Tactic: have H0 : ⟪x - ⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - ⟪x, y⟫ ^ 2 := by
    rw [inner_sub_left, inner_sub_right, inner_sub_right, inner_self_eq_one_of_norm_eq_one hx,
      real_inner_smul_right, ← sq, real_inner_smul_left, real_inner_smul_left,
      real_inner_smul_right, inner_self_eq_one_of_norm_eq_one hy, real_inner_comm y x]
    ring
-- 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
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≠ 0
H0 : ⟪x - ⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2
⊢ x = ⟪y, x⟫ • y + ((1 - HPow.hPow (β := ℕ) ⟪y, x⟫ 2) / ⟪x - ⟪y, x⟫ • y, x - ⟪y, x⟫ • y⟫) • (x - ⟪y, x⟫ • y)
have neg : x = ⟪x, y⟫ • y + ((1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2) / (1 - HPow.hPow (β := ℕ) ⟪x, y⟫ 2)) • (x - ⟪x, y⟫ • y)
Tactic: rw [real_inner_comm x, 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
⊢ angle x z ≤ angle x y + angle y z
have inl : ∀ (H : π < angle x y + angle y z), angle x z ≤ angle x y + angle y z
Tactic: rcases lt_or_ge π (angle x y + angle y z) with H | 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
inl : ∀ (H : π < angle x y + angle y z), angle x z ≤ angle x y + angle y z
⊢ angle x z ≤ angle x y + angle y z
have inr : ∀ (H : angle x y + angle y z ≤ π), angle x z ≤ angle x y + angle y z
Tactic: rcases lt_or_ge π (angle x y + angle y z) with H | 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 y + angle y z
⊢ angle x z ≤ angle x y + angle y z
have linarith : angle x y + angle y z < angle x z →
  π - (angle x y + angle y z) + (angle x y + angle y z - angle x z) + (angle x z - π) = 0
Tactic: linarith [angle_le_pi x 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 y + angle y z ≤ π
this : Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z)
⊢ angle x z ≤ angle x y + angle y z
have H0 : 0 ≤ angle x y + angle y z
Tactic: have H0 : 0 ≤ angle x y + angle y z :=
      add_nonneg (angle_nonneg x y) (angle_nonneg y z)