awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
hxy : x ≠ y
h_sin : ∀ (x y : V) (hx : x ≠ 0) (hy : y ≠ 0), Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)
hsub : x - y ≠ 0
⊢ √(⟪x, x⟫ * ⟪y, y⟫ - HPow.hPow (β := ℕ) ⟪x, y⟫ 2) =
    √(⟪y, y⟫ * (⟪x, x⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪y, y⟫)) - HPow.hPow (β := ℕ) (⟪x, y⟫ - ⟪y, y⟫) 2)

Tactic:
ring_nf
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hxy : x - y ≠ 0
⊢ Real.sin (angle x y) / ‖x - y‖ = Real.sin (angle y (x - y)) / ‖x‖

Tactic:
simp [field, sin_angle_mul_norm_eq_sin_angle_mul_norm x y]

Premises used: InnerProductGeometry.sin_angle_mul_norm_eq_sin_angle_mul_norm
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ‖x‖ = ‖y‖
⊢ angle x (x - y) = angle y (y - x)

Tactic:
Real.injOn_cos ⟨angle_nonneg _ _, angle_le_pi _ _⟩ ⟨angle_nonneg _ _, angle_le_pi _ _⟩ ?_

Premises used: InnerProductGeometry.angle_le_pi, InnerProductGeometry.angle_nonneg, And.intro, Real.injOn_cos
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ‖x‖ = ‖y‖
refine : Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
⊢ angle x (x - y) = angle y (y - x)

Tactic:
refine Real.injOn_cos ⟨angle_nonneg _ _, angle_le_pi _ _⟩ ⟨angle_nonneg _ _, angle_le_pi _ _⟩ ?_

Premises used: InnerProductGeometry.angle_le_pi, InnerProductGeometry.angle_nonneg, And.intro, Real.injOn_cos
-- Module: Mathlib.Geometry.Euclidean.Triangle
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‖)
rw₁₁ rw₁₂ : (‖y‖ * ‖y‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (‖y‖ * ‖y‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖)
⊢ Real.cos (angle x (x - y)) = Real.cos (angle 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]

Premises used: neg_sub, InnerProductGeometry.cos_angle, real_inner_self_eq_norm_mul_norm, inner_sub_right, norm_neg, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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, 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
-- Module: Mathlib.Geometry.Euclidean.Triangle
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‖
neg : ∀ (hxy : ¬x = y), ‖x‖ = ‖y‖
⊢ ‖x‖ = ‖y‖

Tactic:
by_cases hxy : x = y
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
pos pos₁ : ‖y‖ = ‖y‖
⊢ ‖x‖ = ‖y‖

Tactic:
rw [hxy]
-- Module: Mathlib.Geometry.Euclidean.Triangle
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, 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

Premises used: Norm.norm, neg_sub, mul_assoc, HSub.hSub, div_eq_mul_inv, norm_neg, mul_comm, mul_inv_rev
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
h₁ : ⟪x, x - y⟫ * ‖x‖⁻¹ * ‖x - y‖⁻¹ = ⟪y, y - x⟫ * ‖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

Premises used: Norm.norm, neg_sub, mul_assoc, HSub.hSub, div_eq_mul_inv, norm_neg, mul_comm, mul_inv_rev
-- Module: Mathlib.Geometry.Euclidean.Triangle
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, 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
-- Module: Mathlib.Geometry.Euclidean.Triangle
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‖ = ⟪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

Premises used: sub_eq_sub_iff_sub_eq_sub, mul_sub_left_distrib, mul_sub_right_distrib, mul_self_mul_inv, real_inner_self_eq_norm_mul_norm, inner_sub_right, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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‖
neg : ∀ (hx0 : ¬x = 0), ‖x‖ = ‖y‖
⊢ ‖x‖ = ‖y‖

Tactic:
by_cases hx0 : x = 0
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
⊢ ‖y‖ = 0

Tactic:
rw [hx0, norm_zero, inner_zero_left, zero_mul, zero_sub, neg_eq_zero] at h

Premises used: MulZeroClass.zero_mul, norm_zero, neg_eq_zero, inner_zero_left, zero_sub
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
h₁ : ‖y‖ = 0
⊢ x = 0

Tactic:
rw [hx0, norm_zero, inner_zero_left, zero_mul, zero_sub, neg_eq_zero] at h

Premises used: MulZeroClass.zero_mul, norm_zero, neg_eq_zero, inner_zero_left, zero_sub
-- Module: Mathlib.Geometry.Euclidean.Triangle
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‖
pos₂ pos₃ : Eq (α := ℝ) 0 0
⊢ ‖x‖ = ‖y‖

Tactic:
rw [hx0, norm_zero, h]

Premises used: norm_zero
-- Module: Mathlib.Geometry.Euclidean.Triangle
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‖
neg : ∀ (hy0 : ¬y = 0), ‖x‖ = ‖y‖
⊢ ‖x‖ = ‖y‖

Tactic:
by_cases hy0 : y = 0
-- Module: Mathlib.Geometry.Euclidean.Triangle
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‖ = 0

Tactic:
rw [hy0, norm_zero, inner_zero_right, zero_mul, sub_zero] at h

Premises used: sub_zero, MulZeroClass.zero_mul, norm_zero, inner_zero_right
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
h₁ : ‖x‖ = 0
⊢ ¬x = 0

Tactic:
rw [hy0, norm_zero, inner_zero_right, zero_mul, sub_zero] at h

Premises used: sub_zero, MulZeroClass.zero_mul, norm_zero, inner_zero_right
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
h₁ : ‖x‖ = 0
hx0₁ : ¬x = 0
⊢ y = 0

Tactic:
rw [hy0, norm_zero, inner_zero_right, zero_mul, sub_zero] at h

Premises used: sub_zero, MulZeroClass.zero_mul, norm_zero, inner_zero_right
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
pos₂ pos₃ : Eq (α := ℝ) 0 0
⊢ ‖x‖ = ‖y‖

Tactic:
rw [hy0, norm_zero, h]

Premises used: norm_zero
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
⊢ (‖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

Premises used: norm_eq_zero, neg_sub, mul_div_assoc, inv_sub_inv, Iff.mp, mul_comm, mul_neg_one
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
h₁ : (‖y‖ - ‖x‖) * -1 = (‖y‖ - ‖x‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))
⊢ ¬x = 0

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

Premises used: norm_eq_zero, neg_sub, mul_div_assoc, inv_sub_inv, Iff.mp, mul_comm, mul_neg_one
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
h₁ : (‖y‖ - ‖x‖) * -1 = (‖y‖ - ‖x‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))
hx0₁ : ¬x = 0
⊢ ¬y = 0

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

Premises used: norm_eq_zero, neg_sub, mul_div_assoc, inv_sub_inv, Iff.mp, mul_comm, mul_neg_one
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
neg : ‖y‖ = ‖x‖
⊢ ‖x‖ = ‖y‖

Tactic:
symm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
neg : ∀ (hyx : ¬‖y‖ = ‖x‖), False
⊢ ‖y‖ = ‖x‖

Tactic:
by_contra hyx
-- Module: Mathlib.Geometry.Euclidean.Triangle
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‖
⊢ ⟪x, y⟫ / (‖x‖ * ‖y‖) = -1

Tactic:
replace h := (mul_left_cancel₀ (sub_ne_zero_of_ne hyx) h).symm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
⊢ angle x y = π

Tactic:
rw [real_inner_div_norm_mul_norm_eq_neg_one_iff, ← angle_eq_pi_iff] at h

Premises used: real_inner_div_norm_mul_norm_eq_neg_one_iff, InnerProductGeometry.angle_eq_pi_iff
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : angle x y = π
⊢ False

Tactic:
hpi h
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 : angle x y = π
⊢ False

Tactic:
exact hpi h
-- Module: Mathlib.Geometry.Euclidean.Triangle
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))
inr : ∀ (hxy : x ≠ -y), Real.cos (angle x y) = Real.cos (angle x (x + y) + angle y (y + x))
⊢ 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)

Premises used: eq_or_ne, Neg.neg, rfl
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
y : V
hy : y ≠ 0
hx : -y ≠ 0
⊢ Real.cos (angle (-y) y) = Real.cos (angle (-y) (-y + y) + angle y (y + -y))

Tactic:
simp [hy]
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 ≠ 0

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
⊢ y + x ≠ 0

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
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‖))
⊢ Real.cos (angle x y) = Real.cos (angle x (x + y) + angle y (y + x))

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]

Premises used: Real, Inner.inner, InnerProductGeometry.cos_angle, Real.cos_add, add_comm, mul_comm, InnerProductGeometry.sin_angle_add, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 ≠ 0

Tactic:
have : x + y ≠ 0 := by grind
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
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
⊢ ⟪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:
simp only [field]
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
inr : ⟪x, y⟫ * HPow.hPow (β := ℕ) ‖x + y‖ 2 = ⟪x, x + y⟫ * ⟪y, x + y⟫ - (⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
⊢ ⟪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:
rw [Real.sq_sqrt (sub_nonneg_of_le (real_inner_mul_inner_self_le x y))]

Premises used: real_inner_mul_inner_self_le, sub_nonneg_of_le, Real.sq_sqrt
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
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⟫)
⊢ ⟪x, y⟫ * HPow.hPow (β := ℕ) ‖x + y‖ 2 = ⟪x, x + y⟫ * ⟪y, x + 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]

Premises used: inner_add_left, real_inner_self_eq_norm_sq, inner_add_right, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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, x⟫ + ⟪x, y⟫ + (⟪x, y⟫ + ⟪y, y⟫)) =
    (⟪x, x⟫ + ⟪x, y⟫) * (⟪x, y⟫ + ⟪y, y⟫) - (⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Triangle
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))
inr : ∀ (hxy : x ≠ -y), Real.sin (angle x y) = Real.sin (angle x (x + y) + angle y (y + x))
⊢ 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)

Premises used: eq_or_ne, Neg.neg, rfl
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
y : V
hy : y ≠ 0
hx : -y ≠ 0
⊢ Real.sin (angle (-y) y) = Real.sin (angle (-y) (-y + y) + angle y (y + -y))

Tactic:
simp [hy]
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
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‖))
⊢ Real.sin (angle x y) = Real.sin (angle x (x + y) + angle y (y + x))

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]

Premises used: InnerProductGeometry.sin_angle, InnerProductGeometry.cos_angle, Real.sin_add, add_comm, InnerProductGeometry.sin_angle_add
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
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⟫)
⊢ √(⟪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:
simp only [field]
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
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⟫)
⊢ √(⟪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 [← real_inner_self_eq_norm_sq, inner_add_right, inner_add_left, real_inner_comm]

Premises used: inner_add_left, real_inner_self_eq_norm_sq, inner_add_right, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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, 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:
ring_nf
-- Module: Mathlib.Geometry.Euclidean.Triangle
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)
inr : ∀ (hx : x ≠ 0), angle x y = angle x (x + y) + angle y (x + y)
⊢ angle x y = angle x (x + y) + angle y (x + y)

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
y : V
hy : y ≠ 0
⊢ angle 0 y = angle 0 (0 + y) + angle y (0 + y)

Tactic:
simp [hy]
-- Module: Mathlib.Geometry.Euclidean.Triangle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
⊢ (↑(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)
-- Module: Mathlib.Geometry.Euclidean.Triangle
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) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)

Tactic:
rw [add_comm y x] at h

Premises used: add_comm
-- Module: Mathlib.Geometry.Euclidean.Triangle
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)
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)
⊢ angle x y = angle x (x + y) + angle y (x + y)

Tactic:
obtain ⟨_, ⟨n, rfl⟩, h⟩ := (QuotientAddGroup.mk'_eq_mk' _).mp h

Premises used: QuotientAddGroup.mk'_eq_mk', Iff.mp, rfl
-- Module: Mathlib.Geometry.Euclidean.Triangle
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)
⊢ angle x (x + y) + angle y (x + y) ≤ angle x y + n • (2 * π)

Tactic:
replace h := h.ge
-- Module: Mathlib.Geometry.Euclidean.Triangle
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 * π)
contrapose! : ∀ (h : n ≤ -1), angle x y + n • (2 * π) < angle x (x + y) + angle y (x + y)
⊢ -1 < n

Tactic:
contrapose! h
-- Module: Mathlib.Geometry.Euclidean.Triangle
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
grw : π + -(2 * π) < HAdd.hAdd (α := ℝ) 0 0
⊢ angle x y + n • (2 * π) < angle x (x + y) + angle y (x + y)

Tactic:
grw [h, neg_smul, one_smul, angle_le_pi, ← angle_nonneg, ← angle_nonneg]

Premises used: neg_smul, InnerProductGeometry.angle_le_pi, one_smul, InnerProductGeometry.angle_nonneg