awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ arccos (⟪-x, -y⟫ / (‖-x‖ * ‖-y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw : arccos (⟪x, y⟫ / (‖-x‖ * ‖-y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Tactic: rw [inner_neg_neg, norm_neg, norm_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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‖))
⊢ arccos (⟪-x, -y⟫ / (‖-x‖ * ‖-y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw₁ : arccos (⟪x, y⟫ / (‖x‖ * ‖-y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Tactic: rw [inner_neg_neg, norm_neg, norm_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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‖))
⊢ arccos (⟪-x, -y⟫ / (‖-x‖ * ‖-y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw₂ : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Tactic: rw [inner_neg_neg, norm_neg, norm_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ arccos (⟪x, -y⟫ / (‖x‖ * ‖-y‖)) = π - arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw : arccos (⟪x, -y⟫ / (‖x‖ * ‖-y‖)) = arccos (-(⟪x, y⟫ / (‖x‖ * ‖y‖)))
Tactic: rw [← Real.arccos_neg, norm_neg, inner_neg_right, neg_div]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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‖)))
⊢ arccos (⟪x, -y⟫ / (‖x‖ * ‖-y‖)) = π - arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw₁ : arccos (⟪x, -y⟫ / (‖x‖ * ‖y‖)) = arccos (-(⟪x, y⟫ / (‖x‖ * ‖y‖)))
Tactic: rw [← Real.arccos_neg, norm_neg, inner_neg_right, neg_div]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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‖)))
⊢ arccos (⟪x, -y⟫ / (‖x‖ * ‖-y‖)) = π - arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw₂ : arccos (-⟪x, y⟫ / (‖x‖ * ‖y‖)) = arccos (-(⟪x, y⟫ / (‖x‖ * ‖y‖)))
Tactic: rw [← Real.arccos_neg, norm_neg, inner_neg_right, neg_div]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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‖)))
⊢ arccos (⟪x, -y⟫ / (‖x‖ * ‖-y‖)) = π - arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw₃ : arccos (-(⟪x, y⟫ / (‖x‖ * ‖y‖))) = arccos (-(⟪x, y⟫ / (‖x‖ * ‖y‖)))
Tactic: rw [← Real.arccos_neg, norm_neg, inner_neg_right, neg_div]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ angle (-x) y = π - angle x y
have rw : angle (- -x) (-y) = π - angle x y
Tactic: rw [← angle_neg_neg, neg_neg, angle_neg_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : angle (- -x) (-y) = π - angle x y
⊢ angle (-x) y = π - angle x y
have rw₁ : angle x (-y) = π - angle x y
Tactic: rw [← angle_neg_neg, neg_neg, angle_neg_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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
⊢ angle (-x) y = π - angle x y
have rw₂ : π - angle x y = π - angle x y
Tactic: rw [← angle_neg_neg, neg_neg, angle_neg_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
⊢ arccos (⟪0, x⟫ / (Norm.norm.{u_1} (E := V) 0 * ‖x‖)) = π / 2
have rw : arccos (0 / (Norm.norm.{u_1} (E := V) 0 * ‖x‖)) = π / 2
Tactic: rw [inner_zero_left, zero_div, Real.arccos_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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
⊢ arccos (⟪0, x⟫ / (Norm.norm.{u_1} (E := V) 0 * ‖x‖)) = π / 2
have rw₁ : arccos 0 = π / 2
Tactic: rw [inner_zero_left, zero_div, Real.arccos_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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
⊢ arccos (⟪0, x⟫ / (Norm.norm.{u_1} (E := V) 0 * ‖x‖)) = π / 2
have rw₂ : π / 2 = π / 2
Tactic: rw [inner_zero_left, zero_div, Real.arccos_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
⊢ arccos (⟪x, 0⟫ / (‖x‖ * Norm.norm.{u_1} (E := V) 0)) = π / 2
have rw : arccos (0 / (‖x‖ * Norm.norm.{u_1} (E := V) 0)) = π / 2
Tactic: rw [inner_zero_right, zero_div, Real.arccos_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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
⊢ arccos (⟪x, 0⟫ / (‖x‖ * Norm.norm.{u_1} (E := V) 0)) = π / 2
have rw₁ : arccos 0 = π / 2
Tactic: rw [inner_zero_right, zero_div, Real.arccos_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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
⊢ arccos (⟪x, 0⟫ / (‖x‖ * Norm.norm.{u_1} (E := V) 0)) = π / 2
have rw₂ : π / 2 = π / 2
Tactic: rw [inner_zero_right, zero_div, Real.arccos_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ arccos (⟪x, x⟫ / (‖x‖ * ‖x‖)) = 0
have rw : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
rw : arccos (⟪x, x⟫ / ⟪x, x⟫) = 0
⊢ arccos (⟪x, x⟫ / (‖x‖ * ‖x‖)) = 0
have rw₁ : arccos 1 = 0
Tactic: rw [← real_inner_self_eq_norm_mul_norm, div_self (inner_self_ne_zero.2 hx : ⟪x, x⟫ ≠ 0),
    Real.arccos_one]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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
⊢ arccos (⟪x, x⟫ / (‖x‖ * ‖x‖)) = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [← real_inner_self_eq_norm_mul_norm, div_self (inner_self_ne_zero.2 hx : ⟪x, x⟫ ≠ 0),
    Real.arccos_one]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ angle x (-x) = π
have rw : π - angle x x = π
Tactic: rw [angle_neg_right, angle_self hx, sub_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
rw : π - angle x x = π
⊢ angle x (-x) = π
have rw₁ : π - 0 = π
Tactic: rw [angle_neg_right, angle_self hx, sub_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
rw : π - angle x x = π
rw₁ : π - 0 = π
⊢ angle x (-x) = π
have rw₂ : π = π
Tactic: rw [angle_neg_right, angle_self hx, sub_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ angle (-x) x = π
have rw : angle x (-x) = π
Tactic: rw [angle_comm, angle_self_neg_of_nonzero hx]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
rw : angle x (-x) = π
⊢ angle (-x) x = π
have rw₁ : π = π
Tactic: rw [angle_comm, angle_self_neg_of_nonzero hx]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : 0 < r
⊢ arccos (⟪x, r • y⟫ / (‖x‖ * ‖r • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw : arccos (r * ⟪x, 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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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‖))
⊢ arccos (⟪x, r • y⟫ / (‖x‖ * ‖r • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw₁ : arccos (r * ⟪x, 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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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‖))
⊢ arccos (⟪x, r • y⟫ / (‖x‖ * ‖r • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw₂ : arccos (r * ⟪x, 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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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‖))
⊢ arccos (⟪x, r • y⟫ / (‖x‖ * ‖r • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw₃ : arccos (r * ⟪x, 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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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‖))
⊢ arccos (⟪x, r • y⟫ / (‖x‖ * ‖r • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw₄ : arccos (r * ⟪x, 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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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‖))
⊢ arccos (⟪x, r • y⟫ / (‖x‖ * ‖r • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw₅ : arccos (r * ⟪x, y⟫ / (r * ‖x‖ * ‖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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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‖))
⊢ arccos (⟪x, r • y⟫ / (‖x‖ * ‖r • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw₆ : arccos (r * ⟪x, y⟫ / (r * (‖x‖ * ‖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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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‖))
⊢ arccos (⟪x, r • y⟫ / (‖x‖ * ‖r • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
have rw₇ : arccos (⟪x, y⟫ / (‖x‖ * ‖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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : 0 < r
⊢ angle (r • x) y = angle x y
have rw : angle y (r • x) = angle x y
Tactic: rw [angle_comm, angle_smul_right_of_pos y x hr, angle_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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
⊢ angle (r • x) y = angle x y
have rw₁ : angle y x = angle x y
Tactic: rw [angle_comm, angle_smul_right_of_pos y x hr, angle_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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
⊢ angle (r • x) y = angle x y
have rw₂ : angle x y = angle x y
Tactic: rw [angle_comm, angle_smul_right_of_pos y x hr, angle_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : r < 0
⊢ angle x (r • y) = angle x (-y)
have rw : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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)
⊢ angle x (r • y) = angle x (-y)
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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)
⊢ angle x (r • y) = angle x (-y)
have rw₂ : π - 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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)
⊢ angle x (r • y) = angle x (-y)
have rw₃ : π - angle x 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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)
⊢ angle x (r • y) = angle x (-y)
have rw₄ : π - angle x 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : r < 0
⊢ angle (r • x) y = angle (-x) y
have rw : angle y (r • x) = angle (-x) y
Tactic: rw [angle_comm, angle_smul_right_of_neg y x hr, angle_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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
⊢ angle (r • x) y = angle (-x) y
have rw₁ : angle y (-x) = angle (-x) y
Tactic: rw [angle_comm, angle_smul_right_of_neg y x hr, angle_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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
⊢ angle (r • x) y = angle (-x) y
have rw₂ : angle (-x) y = angle (-x) y
Tactic: rw [angle_comm, angle_smul_right_of_neg y x hr, angle_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) * (‖x‖ * ‖y‖) = ⟪x, y⟫
have rw : ‖x‖ * ‖y‖ = 0 → ⟪x, y⟫ = 0
Tactic: rw [cos_angle, div_mul_cancel_of_imp]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ sin (arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
have rw : √(1 - HPow.hPow (β := ℕ) (⟪x, y⟫ / (‖x‖ * ‖y‖)) 2) * (‖x‖ * ‖y‖) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
Tactic: rw [Real.sin_arccos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ √(1 - HPow.hPow (β := ℕ) (⟪x, y⟫ / (‖x‖ * ‖y‖)) 2) * (‖x‖ * ‖y‖) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
have nth_rw : √(1 - HPow.hPow (β := ℕ) (⟪x, y⟫ / (‖x‖ * ‖y‖)) 2) * √(HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
  √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
Tactic: nth_rw 2 [← Real.sqrt_sq (mul_nonneg (norm_nonneg x) (norm_nonneg y))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ √(1 - HPow.hPow (β := ℕ) (⟪x, y⟫ / (‖x‖ * ‖y‖)) 2) * √(HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
have rw : √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
  √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
Tactic: rw [← Real.sqrt_mul' _ (by positivity), sq]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
have 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⟫)
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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⟫)
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
have 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⟫)
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
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⟫)
have 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⟫)
Tactic: rcases eq_or_ne y 0 with (rfl | hy)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
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⟫)
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
have 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⟫)
Tactic: rcases eq_or_ne y 0 with (rfl | hy)