awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : arccos (⟪x, y⟫ / (‖-x‖ * ‖-y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₁ : arccos (⟪x, y⟫ / (‖x‖ * ‖-y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₂ rw₃ : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
⊢ arccos (⟪-x, -y⟫ / (‖-x‖ * ‖-y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))

Tactic:
rw [inner_neg_neg, norm_neg, norm_neg]

Premises used: inner_neg_neg, norm_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ 0 ≤ angle x y

Tactic:
Real.arccos_nonneg _

Premises used: InnerProductGeometry.angle, Real.arccos_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ angle x y ≤ π

Tactic:
Real.arccos_le_pi _

Premises used: InnerProductGeometry.angle, Real.arccos_le_pi
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ 0 ≤ sin (angle x y)

Tactic:
sin_nonneg_of_nonneg_of_le_pi (angle_nonneg x y) (angle_le_pi x y)

Premises used: InnerProductGeometry.angle_le_pi, Real.sin_nonneg_of_nonneg_of_le_pi, InnerProductGeometry.angle_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : arccos (⟪x, -y⟫ / (‖x‖ * ‖-y‖)) = arccos (-(⟪x, y⟫ / (‖x‖ * ‖y‖)))
rw₁ : arccos (⟪x, -y⟫ / (‖x‖ * ‖y‖)) = arccos (-(⟪x, y⟫ / (‖x‖ * ‖y‖)))
rw₂ : arccos (-⟪x, y⟫ / (‖x‖ * ‖y‖)) = arccos (-(⟪x, y⟫ / (‖x‖ * ‖y‖)))
rw₃ rw₄ : arccos (-(⟪x, y⟫ / (‖x‖ * ‖y‖))) = arccos (-(⟪x, y⟫ / (‖x‖ * ‖y‖)))
⊢ arccos (⟪x, -y⟫ / (‖x‖ * ‖-y‖)) = π - arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))

Tactic:
rw [← Real.arccos_neg, norm_neg, inner_neg_right, neg_div]

Premises used: neg_div, inner_neg_right, Real.arccos_neg, norm_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : angle (- -x) (-y) = π - angle x y
rw₁ : angle x (-y) = π - angle x y
rw₂ rw₃ : π - angle x y = π - angle x y
⊢ angle (-x) y = π - angle x y

Tactic:
rw [← angle_neg_neg, neg_neg, angle_neg_right]

Premises used: InnerProductGeometry.angle_neg_right, neg_neg, InnerProductGeometry.angle_neg_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
rw : arccos (0 / (Norm.norm.{u_1} (E := V) 0 * ‖x‖)) = π / 2
rw₁ : arccos 0 = π / 2
rw₂ rw₃ : π / 2 = π / 2
⊢ arccos (⟪0, x⟫ / (Norm.norm.{u_1} (E := V) 0 * ‖x‖)) = π / 2

Tactic:
rw [inner_zero_left, zero_div, Real.arccos_zero]

Premises used: zero_div, inner_zero_left, Real.arccos_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
rw : arccos (0 / (‖x‖ * Norm.norm.{u_1} (E := V) 0)) = π / 2
rw₁ : arccos 0 = π / 2
rw₂ rw₃ : π / 2 = π / 2
⊢ arccos (⟪x, 0⟫ / (‖x‖ * Norm.norm.{u_1} (E := V) 0)) = π / 2

Tactic:
rw [inner_zero_right, zero_div, Real.arccos_zero]

Premises used: zero_div, inner_zero_right, Real.arccos_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
rw : arccos (⟪x, x⟫ / ⟪x, x⟫) = 0
rw₁ : arccos 1 = 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ arccos (⟪x, x⟫ / (‖x‖ * ‖x‖)) = 0

Tactic:
rw [← real_inner_self_eq_norm_mul_norm, div_self (inner_self_ne_zero.2 hx : ⟪x, x⟫ ≠ 0),
    Real.arccos_one]

Premises used: Iff.mpr, Real.arccos_one, inner_self_ne_zero, real_inner_self_eq_norm_mul_norm, div_self
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
rw : π - angle x x = π
rw₁ : π - 0 = π
rw₂ rw₃ : π = π
⊢ angle x (-x) = π

Tactic:
rw [angle_neg_right, angle_self hx, sub_zero]

Premises used: sub_zero, InnerProductGeometry.angle_neg_right, InnerProductGeometry.angle_self
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
rw : angle x (-x) = π
rw₁ rw₂ : π = π
⊢ angle (-x) x = π

Tactic:
rw [angle_comm, angle_self_neg_of_nonzero hx]

Premises used: InnerProductGeometry.angle_self_neg_of_nonzero, InnerProductGeometry.angle_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : 0 < r
rw : arccos (r * ⟪x, y⟫ / (‖x‖ * ‖r • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₁ : arccos (r * ⟪x, y⟫ / (‖x‖ * (‖r‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₂ : arccos (r * ⟪x, y⟫ / (‖x‖ * (|r| * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₃ : arccos (r * ⟪x, y⟫ / (‖x‖ * (r * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₄ : arccos (r * ⟪x, y⟫ / (‖x‖ * r * ‖y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₅ : arccos (r * ⟪x, y⟫ / (r * ‖x‖ * ‖y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₆ : arccos (r * ⟪x, y⟫ / (r * (‖x‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₇ rw₈ : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
⊢ arccos (⟪x, r • y⟫ / (‖x‖ * ‖r • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))

Tactic:
rw [inner_smul_right, norm_smul, Real.norm_eq_abs, abs_of_nonneg (le_of_lt hr), ← mul_assoc,
    mul_comm _ r, mul_assoc, mul_div_mul_left _ _ (ne_of_gt hr)]

Premises used: norm_smul, mul_assoc, le_of_lt, ne_of_gt, inner_smul_right, mul_div_mul_left, mul_comm, abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : 0 < r
rw : angle y (r • x) = angle x y
rw₁ : angle y x = angle x y
rw₂ rw₃ : angle x y = angle x y
⊢ angle (r • x) y = angle x y

Tactic:
rw [angle_comm, angle_smul_right_of_pos y x hr, angle_comm]

Premises used: InnerProductGeometry.angle_smul_right_of_pos, InnerProductGeometry.angle_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : r < 0
rw : angle x (- -r • y) = angle x (-y)
rw₁ : angle x (-(-r • y)) = angle x (-y)
rw₂ : π - angle x (-r • y) = angle x (-y)
rw₃ : π - angle x y = angle x (-y)
rw₄ rw₅ : π - angle x y = π - angle x y
⊢ angle x (r • y) = angle x (-y)

Tactic:
rw [← neg_neg r, neg_smul, angle_neg_right, angle_smul_right_of_pos x y (neg_pos_of_neg hr),
    angle_neg_right]

Premises used: neg_smul, InnerProductGeometry.angle_smul_right_of_pos, InnerProductGeometry.angle_neg_right, neg_pos_of_neg, neg_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : r < 0
rw : angle y (r • x) = angle (-x) y
rw₁ : angle y (-x) = angle (-x) y
rw₂ rw₃ : angle (-x) y = angle (-x) y
⊢ angle (r • x) y = angle (-x) y

Tactic:
rw [angle_comm, angle_smul_right_of_neg y x hr, angle_comm]

Premises used: InnerProductGeometry.angle_smul_right_of_neg, InnerProductGeometry.angle_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : ‖x‖ * ‖y‖ = 0 → ⟪x, y⟫ = 0
⊢ cos (angle x y) * (‖x‖ * ‖y‖) = ⟪x, y⟫

Tactic:
rw [cos_angle, div_mul_cancel_of_imp]

Premises used: div_mul_cancel_of_imp, InnerProductGeometry.cos_angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ ‖x‖ * ‖y‖ = 0 → ⟪x, y⟫ = 0

Tactic:
simp +contextual [or_imp]

Premises used: or_imp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : √(1 - HPow.hPow (β := ℕ) (⟪x, y⟫ / (‖x‖ * ‖y‖)) 2) * (‖x‖ * ‖y‖) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
⊢ sin (arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
rw [Real.sin_arccos]

Premises used: Real.sin_arccos
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
nth_rw :
  √(1 - HPow.hPow (β := ℕ) (⟪x, y⟫ / (‖x‖ * ‖y‖)) 2) * √(HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
⊢ √(1 - HPow.hPow (β := ℕ) (⟪x, y⟫ / (‖x‖ * ‖y‖)) 2) * (‖x‖ * ‖y‖) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
nth_rw 2 [← Real.sqrt_sq (mul_nonneg (norm_nonneg x) (norm_nonneg y))]

Premises used: mul_nonneg, Real.sqrt_sq, norm_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ 0 ≤ HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw :
  √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
⊢ √(1 - HPow.hPow (β := ℕ) (⟪x, y⟫ / (‖x‖ * ‖y‖)) 2) * √(HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
rw [← Real.sqrt_mul' _ (by positivity), sq]

Premises used: sq, Real.sqrt_mul'
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
inl :
  √((1 - ⟪0, y⟫ / (Norm.norm.{u_1} (E := V) 0 * ‖y‖) * (⟪0, y⟫ / (Norm.norm.{u_1} (E := V) 0 * ‖y‖))) *
        HPow.hPow (β := ℕ) (Norm.norm.{u_1} (E := V) 0 * ‖y‖) 2) =
    √(inner.{0, u_1} ℝ (E := V) 0 0 * ⟪y, y⟫ - ⟪0, y⟫ * ⟪0, y⟫)
inr :
  ∀ (hx : x ≠ 0),
    √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
      √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, 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.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
y : V
⊢ √((1 - ⟪0, y⟫ / (Norm.norm.{u_1} (E := V) 0 * ‖y‖) * (⟪0, y⟫ / (Norm.norm.{u_1} (E := V) 0 * ‖y‖))) *
        HPow.hPow (β := ℕ) (Norm.norm.{u_1} (E := V) 0 * ‖y‖) 2) =
    √(inner.{0, u_1} ℝ (E := V) 0 0 * ⟪y, y⟫ - ⟪0, y⟫ * ⟪0, y⟫)

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
inr :
  √((1 - ⟪x, 0⟫ / (‖x‖ * Norm.norm.{u_1} (E := V) 0) * (⟪x, 0⟫ / (‖x‖ * Norm.norm.{u_1} (E := V) 0))) *
        HPow.hPow (β := ℕ) (‖x‖ * Norm.norm.{u_1} (E := V) 0) 2) =
    √(⟪x, x⟫ * inner.{0, u_1} ℝ (E := V) 0 0 - ⟪x, 0⟫ * ⟪x, 0⟫)
inr₁ :
  ∀ (hy : y ≠ 0),
    √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
      √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
rcases eq_or_ne y 0 with (rfl | hy)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ √((1 - ⟪x, 0⟫ / (‖x‖ * Norm.norm.{u_1} (E := V) 0) * (⟪x, 0⟫ / (‖x‖ * Norm.norm.{u_1} (E := V) 0))) *
        HPow.hPow (β := ℕ) (‖x‖ * Norm.norm.{u_1} (E := V) 0) 2) =
    √(⟪x, x⟫ * inner.{0, u_1} ℝ (E := V) 0 0 - ⟪x, 0⟫ * ⟪x, 0⟫)

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
inr :
  √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
    √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - ⟪x, y⟫ * ⟪x, y⟫)
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
simp only [real_inner_self_eq_norm_mul_norm]

Premises used: real_inner_self_eq_norm_mul_norm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
    √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
field_simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
rw : sin (angle x y) = sin (angle x y) * (‖x‖ * ‖y‖) / (‖x‖ * ‖y‖)
⊢ sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)

Tactic:
rw [← sin_angle_mul_norm_mul_norm]

Premises used: InnerProductGeometry.sin_angle_mul_norm_mul_norm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ sin (angle x y) = sin (angle x y) * (‖x‖ * ‖y‖) / (‖x‖ * ‖y‖)

Tactic:
field
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : x + y ≠ 0
rw :
  √(⟪x, x⟫ * ⟪x + y, x + y⟫ - ⟪x, x + y⟫ * ⟪x, x + y⟫) / (‖x‖ * ‖x + y‖) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖)
⊢ sin (angle x (x + y)) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖)

Tactic:
rw [sin_angle hx hy]

Premises used: InnerProductGeometry.sin_angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : x + y ≠ 0
field_simp :
  √(⟪x, x⟫ * ⟪x + y, x + y⟫ - HPow.hPow (β := ℕ) ⟪x, x + y⟫ 2) = √(⟪x, x⟫ * ⟪y, y⟫ - HPow.hPow (β := ℕ) ⟪x, y⟫ 2)
⊢ √(⟪x, x⟫ * ⟪x + y, x + y⟫ - ⟪x, x + y⟫ * ⟪x, x + y⟫) / (‖x‖ * ‖x + y‖) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖)

Tactic:
field_simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : x + y ≠ 0
simp :
  √(⟪x, x⟫ * (⟪x, x⟫ + ⟪x, y⟫ + (⟪x, y⟫ + ⟪y, y⟫)) - HPow.hPow (β := ℕ) (⟪x, x⟫ + ⟪x, y⟫) 2) =
    √(⟪x, x⟫ * ⟪y, y⟫ - HPow.hPow (β := ℕ) ⟪x, y⟫ 2)
⊢ √(⟪x, x⟫ * ⟪x + y, x + y⟫ - HPow.hPow (β := ℕ) ⟪x, x + y⟫ 2) = √(⟪x, x⟫ * ⟪y, y⟫ - HPow.hPow (β := ℕ) ⟪x, y⟫ 2)

Tactic:
simp only [inner_add_left, inner_add_right, real_inner_comm]

Premises used: inner_add_left, inner_add_right, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : x + y ≠ 0
⊢ √(⟪x, x⟫ * (⟪x, x⟫ + ⟪x, y⟫ + (⟪x, y⟫ + ⟪y, y⟫)) - HPow.hPow (β := ℕ) (⟪x, x⟫ + ⟪x, y⟫) 2) =
    √(⟪x, x⟫ * ⟪y, y⟫ - HPow.hPow (β := ℕ) ⟪x, y⟫ 2)

Tactic:
ring_nf
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : ⟪x, y⟫ / (‖x‖ * ‖y‖) ≤ 1
⊢ angle x y = 0 ↔ x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x

Tactic:
rw [angle, ← real_inner_div_norm_mul_norm_eq_one_iff, Real.arccos_eq_zero, LE.le.ge_iff_eq',
    eq_comm]

Premises used: Real.arccos_eq_zero, InnerProductGeometry.angle, real_inner_div_norm_mul_norm_eq_one_iff, eq_comm, LE.le.ge_iff_eq'
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ ⟪x, y⟫ / (‖x‖ * ‖y‖) ≤ 1

Tactic:
(abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2

Premises used: abs_le, abs_real_inner_div_norm_mul_norm_le_one, And.right, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ ⟪x, y⟫ / (‖x‖ * ‖y‖) ≤ 1

Tactic:
exact (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2

Premises used: abs_le, abs_real_inner_div_norm_mul_norm_le_one, And.right, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : -1 ≤ ⟪x, y⟫ / (‖x‖ * ‖y‖)
⊢ angle x y = π ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x

Tactic:
rw [angle, ← real_inner_div_norm_mul_norm_eq_neg_one_iff, Real.arccos_eq_pi, LE.le.ge_iff_eq']

Premises used: real_inner_div_norm_mul_norm_eq_neg_one_iff, InnerProductGeometry.angle, Real.arccos_eq_pi, LE.le.ge_iff_eq'
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ -1 ≤ ⟪x, y⟫ / (‖x‖ * ‖y‖)

Tactic:
(abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1

Premises used: abs_le, abs_real_inner_div_norm_mul_norm_le_one, And.left, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ -1 ≤ ⟪x, y⟫ / (‖x‖ * ‖y‖)

Tactic:
exact (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1

Premises used: abs_le, abs_real_inner_div_norm_mul_norm_le_one, And.left, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y z : V
h : angle x y = π
rcases : x ≠ 0 → ∀ (r : ℝ) (hr : r < 0) (h : angle x (r • x) = π), angle x z + angle (r • x) z = π
⊢ angle x z + angle y z = π

Tactic:
rcases angle_eq_pi_iff.1 h with ⟨_, ⟨r, ⟨hr, rfl⟩⟩⟩

Premises used: Iff.mp, InnerProductGeometry.angle_eq_pi_iff, rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x z : V
left : x ≠ 0
r : ℝ
hr : r < 0
h : angle x (r • x) = π
rw : angle x z + angle (-x) z = π
rw₁ : angle x z + (π - angle x z) = π
rw₂ rw₃ : π = π
⊢ angle x z + angle (r • x) z = π

Tactic:
rw [angle_smul_left_of_neg x z hr, angle_neg_left, add_sub_cancel]

Premises used: InnerProductGeometry.angle_smul_left_of_neg, add_sub_cancel, InnerProductGeometry.angle_neg_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ angle x y = π / 2 ↔ ⟪x, y⟫ = 0

Tactic:
simp +contextual [angle, or_imp]

Premises used: InnerProductGeometry.angle, or_imp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : angle x y = π
⊢ ⟪x, y⟫ = -(‖x‖ * ‖y‖)

Tactic:
simp [← cos_angle_mul_norm_mul_norm, h]

Premises used: InnerProductGeometry.cos_angle_mul_norm_mul_norm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖

Tactic:
simp [← cos_angle_mul_norm_mul_norm, h]

Premises used: InnerProductGeometry.cos_angle_mul_norm_mul_norm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ⟪x, y⟫ = -(‖x‖ * ‖y‖) ↔ angle x y = π

Tactic:
⟨fun h => ?_, inner_eq_neg_mul_norm_of_angle_eq_pi⟩

Premises used: InnerProductGeometry.inner_eq_neg_mul_norm_of_angle_eq_pi, Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
refine : ∀ (h : ⟪x, y⟫ = -(‖x‖ * ‖y‖)), angle x y = π
⊢ ⟪x, y⟫ = -(‖x‖ * ‖y‖) ↔ angle x y = π

Tactic:
refine ⟨fun h => ?_, inner_eq_neg_mul_norm_of_angle_eq_pi⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ⟪x, y⟫ = -(‖x‖ * ‖y‖)
⊢ ‖x‖ * ‖y‖ ≠ 0

Tactic:
have h₁ : ‖x‖ * ‖y‖ ≠ 0 := (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy)).ne'
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ⟪x, y⟫ = -(‖x‖ * ‖y‖)
h₁ : ‖x‖ * ‖y‖ ≠ 0
rw : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = π
rw₁ : arccos (-(‖x‖ * ‖y‖) / (‖x‖ * ‖y‖)) = π
rw₂ : arccos (-(‖x‖ * ‖y‖ / (‖x‖ * ‖y‖))) = π
rw₃ : arccos (-1) = π
rw₄ rw₅ : π = π
⊢ angle x y = π

Tactic:
rw [angle, h, neg_div, div_self h₁, Real.arccos_neg_one]

Premises used: neg_div, InnerProductGeometry.angle, Real.arccos_neg_one, div_self
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ ↔ angle x y = 0

Tactic:
⟨fun h => ?_, inner_eq_mul_norm_of_angle_eq_zero⟩

Premises used: Iff.intro, InnerProductGeometry.inner_eq_mul_norm_of_angle_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
refine : ∀ (h : ⟪x, y⟫ = ‖x‖ * ‖y‖), angle x y = 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ ↔ angle x y = 0

Tactic:
refine ⟨fun h => ?_, inner_eq_mul_norm_of_angle_eq_zero⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ⟪x, y⟫ = ‖x‖ * ‖y‖
⊢ ‖x‖ * ‖y‖ ≠ 0

Tactic:
have h₁ : ‖x‖ * ‖y‖ ≠ 0 := (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy)).ne'
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ⟪x, y⟫ = ‖x‖ * ‖y‖
h₁ : ‖x‖ * ‖y‖ ≠ 0
rw : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = 0
rw₁ : arccos (‖x‖ * ‖y‖ / (‖x‖ * ‖y‖)) = 0
rw₂ : arccos 1 = 0
rw₃ rw₄ : Eq (α := ℝ) 0 0
⊢ angle x y = 0

Tactic:
rw [angle, h, div_self h₁, Real.arccos_one]

Premises used: Real.arccos_one, InnerProductGeometry.angle, div_self
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : angle x y = π
rw : HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * -(‖x‖ * ‖y‖) + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
⊢ ‖x - y‖ = ‖x‖ + ‖y‖

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg (x - y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
    norm_sub_pow_two_real, inner_eq_neg_mul_norm_of_angle_eq_pi h]

Premises used: norm_sub_pow_two_real, HSub.hSub, InnerProductGeometry.inner_eq_neg_mul_norm_of_angle_eq_pi, add_nonneg, sq_eq_sq₀, norm_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : angle x y = π
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * -(‖x‖ * ‖y‖) + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
rw : HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * (‖x‖ * ‖y‖) + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
⊢ ‖x + y‖ = ‖x‖ + ‖y‖

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg (x + y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
    norm_add_pow_two_real, inner_eq_mul_norm_of_angle_eq_zero h]

Premises used: norm_add_pow_two_real, add_nonneg, HAdd.hAdd, InnerProductGeometry.inner_eq_mul_norm_of_angle_eq_zero, sq_eq_sq₀, norm_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : angle x y = 0
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * (‖x‖ * ‖y‖) + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2

Tactic:
ring