awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ‖x‖ = ‖y‖
rw : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = Real.cos (angle y (y - x))
rw₁ : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₂ : ⟪x, x - y⟫ / (‖y‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₃ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖-(y - x)‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₄ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₅ : ⟪x, x - y⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₆ : (⟪x, x⟫ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₇ : (⟪x, x⟫ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (⟪y, y⟫ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
⊢ Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
have rw₈ : (‖x‖ * ‖x‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (⟪y, y⟫ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
Tactic: rw [cos_angle, cos_angle, h, ← neg_sub, norm_neg, neg_sub, inner_sub_right, inner_sub_right,
    real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm, h, real_inner_comm x y]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ‖x‖ = ‖y‖
rw : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = Real.cos (angle y (y - x))
rw₁ : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₂ : ⟪x, x - y⟫ / (‖y‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₃ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖-(y - x)‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₄ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₅ : ⟪x, x - y⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₆ : (⟪x, x⟫ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₇ : (⟪x, x⟫ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (⟪y, y⟫ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
rw₈ : (‖x‖ * ‖x‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (⟪y, y⟫ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
⊢ Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
have rw₉ : (‖x‖ * ‖x‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (‖y‖ * ‖y‖ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
Tactic: rw [cos_angle, cos_angle, h, ← neg_sub, norm_neg, neg_sub, inner_sub_right, inner_sub_right,
    real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm, h, real_inner_comm x y]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ‖x‖ = ‖y‖
rw : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = Real.cos (angle y (y - x))
rw₁ : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₂ : ⟪x, x - y⟫ / (‖y‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₃ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖-(y - x)‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₄ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₅ : ⟪x, x - y⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₆ : (⟪x, x⟫ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₇ : (⟪x, x⟫ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (⟪y, y⟫ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
rw₈ : (‖x‖ * ‖x‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (⟪y, y⟫ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
rw₉ : (‖x‖ * ‖x‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (‖y‖ * ‖y‖ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
⊢ Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
have rw₁₀ : (‖y‖ * ‖y‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (‖y‖ * ‖y‖ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
Tactic: rw [cos_angle, cos_angle, h, ← neg_sub, norm_neg, neg_sub, inner_sub_right, inner_sub_right,
    real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm, h, real_inner_comm x y]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ‖x‖ = ‖y‖
rw : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = Real.cos (angle y (y - x))
rw₁ : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₂ : ⟪x, x - y⟫ / (‖y‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₃ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖-(y - x)‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₄ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₅ : ⟪x, x - y⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₆ : (⟪x, x⟫ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₇ : (⟪x, x⟫ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (⟪y, y⟫ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
rw₈ : (‖x‖ * ‖x‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (⟪y, y⟫ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
rw₉ : (‖x‖ * ‖x‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (‖y‖ * ‖y‖ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
rw₁₀ : (‖y‖ * ‖y‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (‖y‖ * ‖y‖ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
⊢ Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
have rw₁₁ : (‖y‖ * ‖y‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (‖y‖ * ‖y‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖)
Tactic: rw [cos_angle, cos_angle, h, ← neg_sub, norm_neg, neg_sub, inner_sub_right, inner_sub_right,
    real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm, h, real_inner_comm x y]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : angle x (x - y) = angle y (y - x)
hpi : angle x y ≠ π
⊢ ‖x‖ = ‖y‖
have h₁ : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
Tactic: replace h := Real.arccos_injOn (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x (x - y)))
    (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one y (y - x))) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
⊢ ‖x‖ = ‖y‖
have pos : ∀ (hxy : x = y), ‖x‖ = ‖y‖
Tactic: by_cases hxy : x = y
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
pos : ∀ (hxy : x = y), ‖x‖ = ‖y‖
⊢ ‖x‖ = ‖y‖
have neg : ∀ (hxy : ¬x = y), ‖x‖ = ‖y‖
Tactic: by_cases hxy : x = y
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
hxy : x = y
⊢ ‖x‖ = ‖y‖
have pos : ‖y‖ = ‖y‖
Tactic: rw [hxy]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
hxy : ¬x = y
⊢ ‖x‖ = ‖y‖
have h₁ : ⟪x, x - y⟫ * ‖x‖⁻¹ * ‖x - y‖⁻¹ = ⟪y, y - x⟫ * ‖y‖⁻¹ * ‖x - y‖⁻¹
Tactic: rw [← norm_neg (y - x), neg_sub, mul_comm, mul_comm ‖y‖, div_eq_mul_inv, div_eq_mul_inv,
      mul_inv_rev, mul_inv_rev, ← mul_assoc, ← mul_assoc] at h
Cleared hypotheses: h, hxy
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : ⟪x, x - y⟫ * ‖x‖⁻¹ * ‖x - y‖⁻¹ = ⟪y, y - x⟫ * ‖y‖⁻¹ * ‖x - y‖⁻¹
hxy : ¬x = y
⊢ ‖x‖ = ‖y‖
have h₁ : ⟪x, x - y⟫ * ‖x‖⁻¹ = ⟪y, y - x⟫ * ‖y‖⁻¹
Tactic: replace h :=
      mul_right_cancel₀ (inv_ne_zero fun hz => hxy (eq_of_sub_eq_zero (norm_eq_zero.1 hz))) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ⟪x, x - y⟫ * ‖x‖⁻¹ = ⟪y, y - x⟫ * ‖y‖⁻¹
⊢ ‖x‖ = ‖y‖
have h₁ : ‖x‖ - ‖y‖ = ⟪x, y⟫ * (‖x‖⁻¹ - ‖y‖⁻¹)
Tactic: rw [inner_sub_right, inner_sub_right, real_inner_comm x y, real_inner_self_eq_norm_mul_norm,
      real_inner_self_eq_norm_mul_norm, mul_sub_right_distrib, mul_sub_right_distrib,
      mul_self_mul_inv, mul_self_mul_inv, sub_eq_sub_iff_sub_eq_sub, ← mul_sub_left_distrib] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = ⟪x, y⟫ * (‖x‖⁻¹ - ‖y‖⁻¹)
⊢ ‖x‖ = ‖y‖
have pos : ∀ (hx0 : x = 0), ‖x‖ = ‖y‖
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = ⟪x, y⟫ * (‖x‖⁻¹ - ‖y‖⁻¹)
pos : ∀ (hx0 : x = 0), ‖x‖ = ‖y‖
⊢ ‖x‖ = ‖y‖
have neg : ∀ (hx0 : ¬x = 0), ‖x‖ = ‖y‖
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = ⟪x, y⟫ * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : x = 0
⊢ ‖x‖ = ‖y‖
have h₁ : ‖y‖ = 0
Tactic: rw [hx0, norm_zero, inner_zero_left, zero_mul, zero_sub, neg_eq_zero] at h
Cleared hypotheses: h, hx0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖y‖ = 0
hx0 : x = 0
⊢ ‖x‖ = ‖y‖
have pos : norm.{u_1} (E := V) 0 = ‖y‖
Tactic: rw [hx0, norm_zero, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖y‖ = 0
hx0 : x = 0
pos : norm.{u_1} (E := V) 0 = ‖y‖
⊢ ‖x‖ = ‖y‖
have pos₁ : 0 = ‖y‖
Tactic: rw [hx0, norm_zero, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖y‖ = 0
hx0 : x = 0
pos : norm.{u_1} (E := V) 0 = ‖y‖
pos₁ : 0 = ‖y‖
⊢ ‖x‖ = ‖y‖
have pos₂ : Eq (α := ℝ) 0 0
Tactic: rw [hx0, norm_zero, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = ⟪x, y⟫ * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : ¬x = 0
⊢ ‖x‖ = ‖y‖
have pos : ∀ (hy0 : y = 0), ‖x‖ = ‖y‖
Tactic: by_cases hy0 : y = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = ⟪x, y⟫ * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : ¬x = 0
pos : ∀ (hy0 : y = 0), ‖x‖ = ‖y‖
⊢ ‖x‖ = ‖y‖
have neg : ∀ (hy0 : ¬y = 0), ‖x‖ = ‖y‖
Tactic: by_cases hy0 : y = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = ⟪x, y⟫ * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : ¬x = 0
hy0 : y = 0
⊢ ‖x‖ = ‖y‖
have h₁ : ‖x‖ = 0
Tactic: rw [hy0, norm_zero, inner_zero_right, zero_mul, sub_zero] at h
Cleared hypotheses: h, hx0, hy0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ = 0
hx0 : ¬x = 0
hy0 : y = 0
⊢ ‖x‖ = ‖y‖
have pos : ‖x‖ = norm.{u_1} (E := V) 0
Tactic: rw [hy0, norm_zero, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ = 0
hx0 : ¬x = 0
hy0 : y = 0
pos : ‖x‖ = norm.{u_1} (E := V) 0
pos₁ : ‖x‖ = 0
⊢ ‖x‖ = ‖y‖
have pos₂ : Eq (α := ℝ) 0 0
Tactic: rw [hy0, norm_zero, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = ⟪x, y⟫ * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖x‖ = ‖y‖
have h₁ : (‖y‖ - ‖x‖) * -1 = (‖y‖ - ‖x‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))
Tactic: rw [inv_sub_inv (fun hz => hx0 (norm_eq_zero.1 hz)) fun hz => hy0 (norm_eq_zero.1 hz), ←
          neg_sub, ← mul_div_assoc, mul_comm, mul_div_assoc, ← mul_neg_one] at h
Cleared hypotheses: h, hx0, hy0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : (‖y‖ - ‖x‖) * -1 = (‖y‖ - ‖x‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖x‖ = ‖y‖
have neg : ‖y‖ = ‖x‖
Tactic: symm
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : (‖y‖ - ‖x‖) * -1 = (‖y‖ - ‖x‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖y‖ = ‖x‖
have neg : ∀ (hyx : ¬‖y‖ = ‖x‖), False
Tactic: by_contra hyx
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : (‖y‖ - ‖x‖) * -1 = (‖y‖ - ‖x‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))
hx0 : ¬x = 0
hy0 : ¬y = 0
hyx : ¬‖y‖ = ‖x‖
⊢ False
have h₁ : ⟪x, y⟫ / (‖x‖ * ‖y‖) = -1
Tactic: replace h := (mul_left_cancel₀ (sub_ne_zero_of_ne hyx) h).symm
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
hx0 : ¬x = 0
hy0 : ¬y = 0
hyx : ¬‖y‖ = ‖x‖
h : ⟪x, y⟫ / (‖x‖ * ‖y‖) = -1
⊢ False
have h₁ : angle x y = π
Tactic: rw [real_inner_div_norm_mul_norm_eq_neg_one_iff, ← angle_eq_pi_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ Real.cos (angle x y) = Real.cos (angle x (x + y) + angle y (y + x))
have inl : ∀ (hx : -y ≠ 0), Real.cos (angle (-y) y) = Real.cos (angle (-y) (-y + y) + angle y (y + -y))
Tactic: rcases eq_or_ne x (-y) with (rfl | hxy)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
inl : ∀ (hx : -y ≠ 0), Real.cos (angle (-y) y) = Real.cos (angle (-y) (-y + y) + angle y (y + -y))
⊢ Real.cos (angle x y) = Real.cos (angle x (x + y) + angle y (y + x))
have inr : ∀ (hxy : x ≠ -y), Real.cos (angle x y) = Real.cos (angle x (x + y) + angle y (y + x))
Tactic: rcases eq_or_ne x (-y) with (rfl | hxy)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
⊢ Real.cos (angle x y) = Real.cos (angle x (x + y) + angle y (y + x))
have inr : ⟪x, y⟫ / (‖x‖ * ‖y‖) =
  ⟪x, x + y⟫ / (‖x‖ * ‖x + y‖) * (⟪y, x + y⟫ / (‖y‖ * ‖x + y‖)) -
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖) * (√(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖y‖ * ‖x + y‖))
Tactic: rw [Real.cos_add, cos_angle, cos_angle, cos_angle, sin_angle_add hx (by grind),
      sin_angle_add hy (by grind), mul_comm ⟪y, y⟫ ⟪x, x⟫, real_inner_comm x y, add_comm y x]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
⊢ ⟪x, y⟫ / (‖x‖ * ‖y‖) =
    ⟪x, x + y⟫ / (‖x‖ * ‖x + y‖) * (⟪y, x + y⟫ / (‖y‖ * ‖x + y‖)) -
      √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖) * (√(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖y‖ * ‖x + y‖))
have this : x + y ≠ 0
Tactic: have : x + y ≠ 0 := by grind
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
this : x + y ≠ 0
⊢ ⟪x, y⟫ / (‖x‖ * ‖y‖) =
    ⟪x, x + y⟫ / (‖x‖ * ‖x + y‖) * (⟪y, x + y⟫ / (‖y‖ * ‖x + y‖)) -
      √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖) * (√(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖y‖ * ‖x + y‖))
have inr : ⟪x, y⟫ * HPow.hPow (β := ℕ) ‖x + y‖ 2 =
  ⟪x, x + y⟫ * ⟪y, x + y⟫ - HPow.hPow (β := ℕ) (√(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)) 2
Tactic: simp only [field]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
this : x + y ≠ 0
⊢ ⟪x, y⟫ * HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    ⟪x, x + y⟫ * ⟪y, x + y⟫ - HPow.hPow (β := ℕ) (√(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)) 2
have inr : ⟪x, y⟫ * HPow.hPow (β := ℕ) ‖x + y‖ 2 = ⟪x, x + y⟫ * ⟪y, x + y⟫ - (⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
Tactic: rw [Real.sq_sqrt (sub_nonneg_of_le (real_inner_mul_inner_self_le x y))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
this : x + y ≠ 0
⊢ ⟪x, y⟫ * HPow.hPow (β := ℕ) ‖x + y‖ 2 = ⟪x, x + y⟫ * ⟪y, x + y⟫ - (⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
have inr : ⟪x, y⟫ * (⟪x, x⟫ + ⟪x, y⟫ + (⟪x, y⟫ + ⟪y, y⟫)) =
  (⟪x, x⟫ + ⟪x, y⟫) * (⟪x, y⟫ + ⟪y, y⟫) - (⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
Tactic: simp only [← real_inner_self_eq_norm_sq, inner_add_right, inner_add_left, real_inner_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ Real.sin (angle x y) = Real.sin (angle x (x + y) + angle y (y + x))
have inl : ∀ (hx : -y ≠ 0), Real.sin (angle (-y) y) = Real.sin (angle (-y) (-y + y) + angle y (y + -y))
Tactic: rcases eq_or_ne x (-y) with (rfl | hxy)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
inl : ∀ (hx : -y ≠ 0), Real.sin (angle (-y) y) = Real.sin (angle (-y) (-y + y) + angle y (y + -y))
⊢ Real.sin (angle x y) = Real.sin (angle x (x + y) + angle y (y + x))
have inr : ∀ (hxy : x ≠ -y), Real.sin (angle x y) = Real.sin (angle x (x + y) + angle y (y + x))
Tactic: rcases eq_or_ne x (-y) with (rfl | hxy)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
⊢ Real.sin (angle x y) = Real.sin (angle x (x + y) + angle y (y + x))
have inr : √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) =
  √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖) * (⟪y, x + y⟫ / (‖y‖ * ‖x + y‖)) +
    ⟪x, x + y⟫ / (‖x‖ * ‖x + y‖) * (√(⟪y, y⟫ * ⟪x, x⟫ - ⟪y, x⟫ * ⟪y, x⟫) / (‖y‖ * ‖x + y‖))
Tactic: rw [Real.sin_add, cos_angle, cos_angle, sin_angle_add hx (by grind),
      sin_angle_add hy (by grind), sin_angle hx hy, add_comm y x]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
⊢ √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖) * (⟪y, x + y⟫ / (‖y‖ * ‖x + y‖)) +
      ⟪x, x + y⟫ / (‖x‖ * ‖x + y‖) * (√(⟪y, y⟫ * ⟪x, x⟫ - ⟪y, x⟫ * ⟪y, x⟫) / (‖y‖ * ‖x + y‖))
have this : x + y ≠ 0
Tactic: have : x + y ≠ 0 := by grind
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
this : x + y ≠ 0
⊢ √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖) * (⟪y, x + y⟫ / (‖y‖ * ‖x + y‖)) +
      ⟪x, x + y⟫ / (‖x‖ * ‖x + y‖) * (√(⟪y, y⟫ * ⟪x, x⟫ - ⟪y, x⟫ * ⟪y, x⟫) / (‖y‖ * ‖x + y‖))
have inr : √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) * HPow.hPow (β := ℕ) ‖x + y‖ 2 =
  √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) * ⟪y, x + y⟫ + ⟪x, x + y⟫ * √(⟪y, y⟫ * ⟪x, x⟫ - ⟪y, x⟫ * ⟪y, x⟫)
Tactic: simp only [field]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
this : x + y ≠ 0
⊢ √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) * HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) * ⟪y, x + y⟫ + ⟪x, x + y⟫ * √(⟪y, y⟫ * ⟪x, x⟫ - ⟪y, x⟫ * ⟪y, x⟫)
have inr : √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) * (⟪x, x⟫ + ⟪x, y⟫ + (⟪x, y⟫ + ⟪y, y⟫)) =
  √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) * (⟪x, y⟫ + ⟪y, y⟫) + (⟪x, x⟫ + ⟪x, y⟫) * √(⟪y, y⟫ * ⟪x, x⟫ - ⟪x, y⟫ * ⟪x, y⟫)
Tactic: simp only [← real_inner_self_eq_norm_sq, inner_add_right, inner_add_left, real_inner_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
⊢ angle x y = angle x (x + y) + angle y (x + y)
have inl : angle 0 y = angle 0 (0 + y) + angle y (0 + y)
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
inl : angle 0 y = angle 0 (0 + y) + angle y (0 + y)
⊢ angle x y = angle x (x + y) + angle y (x + y)
have inr : ∀ (hx : x ≠ 0), angle x y = angle x (x + y) + angle y (x + y)
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
⊢ angle x y = angle x (x + y) + angle y (x + y)
have h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (y + x)) : Real.Angle)
Tactic: have h := Real.Angle.cos_sin_inj
    (cos_angle_eq_cos_angle_add_add_angle_add hx hy)
    (sin_angle_eq_sin_angle_add_add_angle_add hx hy)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 y) : Real.Angle) = (↑(angle x (x + y) + angle y (y + x)) : Real.Angle)
⊢ angle x y = angle x (x + y) + angle y (x + y)
have h₁ : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
Tactic: rw [add_comm y x] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
⊢ angle x y = angle x (x + y) + angle y (x + y)
have inr : ∀ (n : ℤ) (h : angle x y + (fun (x : ℤ) ↦ x • (2 * π)) n = angle x (x + y) + angle y (x + y)),
  angle x y = angle x (x + y) + angle y (x + y)
Tactic: obtain ⟨_, ⟨n, rfl⟩, h⟩ := (QuotientAddGroup.mk'_eq_mk' _).mp h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
⊢ -1 < n
have h₁ : angle x (x + y) + angle y (x + y) ≤ angle x y + n • (2 * π)
Tactic: replace h := h.ge
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x (x + y) + angle y (x + y) ≤ angle x y + n • (2 * π)
⊢ -1 < n
have contrapose! : ∀ (h : n ≤ -1), angle x y + n • (2 * π) < angle x (x + y) + angle y (x + y)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : n ≤ -1
⊢ angle x y + n • (2 * π) < angle x (x + y) + angle y (x + y)
have grw : π + -(2 * π) < HAdd.hAdd (α := ℝ) 0 0
Tactic: grw [h, neg_smul, one_smul, angle_le_pi, ← angle_nonneg, ← angle_nonneg]