awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ 0 < InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))

Tactic:
exact angle_add_pos_of_inner_eq_zero h h0

Premises used: InnerProductGeometry.angle_add_pos_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
rw : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) ≤ π / 2
⊢ ∠ p₂ p₃ p₁ ≤ π / 2

Tactic:
rw [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]

Premises used: vsub_add_vsub_cancel, add_comm, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) ≤ π / 2

Tactic:
angle_add_le_pi_div_two_of_inner_eq_zero h

Premises used: InnerProductGeometry.angle_add_le_pi_div_two_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) ≤ π / 2

Tactic:
exact angle_add_le_pi_div_two_of_inner_eq_zero h

Premises used: InnerProductGeometry.angle_add_le_pi_div_two_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0
rw : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) < π / 2
⊢ ∠ p₂ p₃ p₁ < π / 2

Tactic:
rw [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]

Premises used: vsub_add_vsub_cancel, add_comm, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) < π / 2

Tactic:
angle_add_lt_pi_div_two_of_inner_eq_zero h h0

Premises used: InnerProductGeometry.angle_add_lt_pi_div_two_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) < π / 2

Tactic:
exact angle_add_lt_pi_div_two_of_inner_eq_zero h h0

Premises used: InnerProductGeometry.angle_add_lt_pi_div_two_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
rw : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₃ p₂ / dist p₁ p₃
rw₁ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₂ -ᵥ p₃‖ / dist p₁ p₃
rw₂ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₂ -ᵥ p₃‖ / ‖p₁ -ᵥ p₃‖
rw₃ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃))) = ‖p₂ -ᵥ p₃‖ / ‖p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)‖
rw₄ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))) = ‖p₂ -ᵥ p₃‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖
rw₅ rw₆ : ‖p₂ -ᵥ p₃‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖ = ‖p₂ -ᵥ p₃‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖
⊢ Real.cos (∠ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃

Tactic:
rw [angle, dist_eq_norm_vsub' V p₃ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, cos_angle_add_of_inner_eq_zero h]

Premises used: InnerProductGeometry.cos_angle_add_of_inner_eq_zero, vsub_add_vsub_cancel, dist_eq_norm_vsub', add_comm, dist_eq_norm_vsub, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ ≠ 0
rw : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₁ p₂ / dist p₁ p₃
rw₁ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₁ -ᵥ p₂‖ / dist p₁ p₃
rw₂ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₁ -ᵥ p₂‖ / ‖p₁ -ᵥ p₃‖
rw₃ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃))) = ‖p₁ -ᵥ p₂‖ / ‖p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)‖
rw₄ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))) = ‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖
rw₅ rw₆ : ‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖ = ‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃

Tactic:
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, sin_angle_add_of_inner_eq_zero h h0]

Premises used: vsub_add_vsub_cancel, add_comm, InnerProductGeometry.sin_angle_add_of_inner_eq_zero, dist_eq_norm_vsub, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
rw : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₁ p₂ / dist p₃ p₂
rw₁ : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₁ -ᵥ p₂‖ / dist p₃ p₂
rw₂ : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖
rw₃ : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃))) = ‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖
rw₄ : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))) = ‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖
rw₅ rw₆ : ‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖
⊢ Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂

Tactic:
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub' V p₃ p₂, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, tan_angle_add_of_inner_eq_zero h]

Premises used: vsub_add_vsub_cancel, dist_eq_norm_vsub', add_comm, InnerProductGeometry.tan_angle_add_of_inner_eq_zero, dist_eq_norm_vsub, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
rw : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist p₁ p₃ = dist p₃ p₂
rw₁ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist p₁ p₃ = ‖p₂ -ᵥ p₃‖
rw₂ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * ‖p₁ -ᵥ p₃‖ = ‖p₂ -ᵥ p₃‖
rw₃ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃))) * ‖p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)‖ = ‖p₂ -ᵥ p₃‖
rw₄ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))) * ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖ = ‖p₂ -ᵥ p₃‖
rw₅ rw₆ : ‖p₂ -ᵥ p₃‖ = ‖p₂ -ᵥ p₃‖
⊢ Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂

Tactic:
rw [angle, dist_eq_norm_vsub' V p₃ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, cos_angle_add_mul_norm_of_inner_eq_zero h]

Premises used: vsub_add_vsub_cancel, dist_eq_norm_vsub', add_comm, InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero, dist_eq_norm_vsub, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
rw : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist p₁ p₃ = dist p₁ p₂
rw₁ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist p₁ p₃ = ‖p₁ -ᵥ p₂‖
rw₂ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖
rw₃ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃))) * ‖p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)‖ = ‖p₁ -ᵥ p₂‖
rw₄ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))) * ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖ = ‖p₁ -ᵥ p₂‖
rw₅ rw₆ : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₂‖
⊢ Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂

Tactic:
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, sin_angle_add_mul_norm_of_inner_eq_zero h]

Premises used: vsub_add_vsub_cancel, add_comm, dist_eq_norm_vsub, InnerProductGeometry.sin_angle_add_mul_norm_of_inner_eq_zero, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
    inner_neg_left, neg_vsub_eq_vsub_rev] at h

Premises used: neg_eq_zero, neg_vsub_eq_vsub_rev, real_inner_comm, InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, EuclideanGeometry.angle, inner_neg_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
h₁ : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
⊢ p₁ = p₂ ∨ p₃ ≠ p₂

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
    inner_neg_left, neg_vsub_eq_vsub_rev] at h

Premises used: neg_eq_zero, neg_vsub_eq_vsub_rev, real_inner_comm, InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, EuclideanGeometry.angle, inner_neg_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0

Tactic:
rw [ne_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, or_comm] at h0

Premises used: vsub_ne_zero, vsub_eq_zero_iff_eq, ne_comm, or_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
rw : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist p₃ p₂ = dist p₁ p₂
rw₁ : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist p₃ p₂ = ‖p₁ -ᵥ p₂‖
rw₂ : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * ‖p₂ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖
rw₃ : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃))) * ‖p₂ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖
rw₄ : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))) * ‖p₂ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖
rw₅ rw₆ : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₂‖
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂

Tactic:
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub' V p₃ p₂, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, tan_angle_add_mul_norm_of_inner_eq_zero h h0]

Premises used: InnerProductGeometry.tan_angle_add_mul_norm_of_inner_eq_zero, vsub_add_vsub_cancel, dist_eq_norm_vsub', add_comm, dist_eq_norm_vsub, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
rw : dist p₃ p₂ / Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₁ p₃
rw₁ : ‖p₂ -ᵥ p₃‖ / Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₁ p₃
rw₂ : ‖p₂ -ᵥ p₃‖ / Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₁ -ᵥ p₃‖
rw₃ : ‖p₂ -ᵥ p₃‖ / Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃))) = ‖p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)‖
rw₄ : ‖p₂ -ᵥ p₃‖ / Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))) = ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖
rw₅ rw₆ : ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖ = ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃

Tactic:
rw [angle, dist_eq_norm_vsub' V p₃ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, norm_div_cos_angle_add_of_inner_eq_zero h h0]

Premises used: vsub_add_vsub_cancel, dist_eq_norm_vsub', add_comm, dist_eq_norm_vsub, EuclideanGeometry.angle, InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0

Tactic:
rw [eq_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, or_comm] at h0

Premises used: vsub_ne_zero, vsub_eq_zero_iff_eq, eq_comm, or_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
rw : dist p₁ p₂ / Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₁ p₃
rw₁ : ‖p₁ -ᵥ p₂‖ / Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₁ p₃
rw₂ : ‖p₁ -ᵥ p₂‖ / Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₁ -ᵥ p₃‖
rw₃ : ‖p₁ -ᵥ p₂‖ / Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃))) = ‖p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)‖
rw₄ : ‖p₁ -ᵥ p₂‖ / Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))) = ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖
rw₅ rw₆ : ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖ = ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃

Tactic:
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, norm_div_sin_angle_add_of_inner_eq_zero h h0]

Premises used: vsub_add_vsub_cancel, InnerProductGeometry.norm_div_sin_angle_add_of_inner_eq_zero, add_comm, dist_eq_norm_vsub, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
rw : dist p₁ p₂ / Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₃ p₂
rw₁ : ‖p₁ -ᵥ p₂‖ / Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₃ p₂
rw₂ : ‖p₁ -ᵥ p₂‖ / Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₂ -ᵥ p₃‖
rw₃ : ‖p₁ -ᵥ p₂‖ / Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃))) = ‖p₂ -ᵥ p₃‖
rw₄ : ‖p₁ -ᵥ p₂‖ / Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))) = ‖p₂ -ᵥ p₃‖
rw₅ rw₆ : ‖p₂ -ᵥ p₃‖ = ‖p₂ -ᵥ p₃‖
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂

Tactic:
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub' V p₃ p₂, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, norm_div_tan_angle_add_of_inner_eq_zero h h0]

Premises used: vsub_add_vsub_cancel, dist_eq_norm_vsub', InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero, add_comm, dist_eq_norm_vsub, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : ‖y‖ = 1
rw : HSub.hSub (β := V) x ((Submodule.starProjection (ℝ ∙ y) : (a : V) → V) x : V) = x - ⟪y, x⟫ • y
rw₁ rw₂ : x - ⟪y, x⟫ • y = x - ⟪y, x⟫ • y
⊢ ortho y x = x - ⟪y, x⟫ • y

Tactic:
rw [ortho, Submodule.starProjection_unit_singleton _ hy]

Premises used: _private.0.InnerProductGeometry.ortho, Submodule.starProjection_unit_singleton
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
rw : ⟪x, y⟫ * ⟪x, y⟫ ≤ 1
⊢ 0 ≤ ⟪x, ortho y x⟫

Tactic:
rw [ortho_eq_sub_inner x hy, inner_sub_right,
    inner_self_eq_one_of_norm_eq_one hx, real_inner_smul_right, real_inner_comm, sub_nonneg]

Premises used: inner_self_eq_one_of_norm_eq_one, real_inner_smul_right, inner_sub_right, sub_nonneg, _private.0.InnerProductGeometry.ortho_eq_sub_inner, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
grw : HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≤ 1
grw₁ : |⟪x, y⟫| ≤ 1
grw₂ : ‖x‖ * ‖y‖ ≤ 1
grw₃ : 1 * ‖y‖ ≤ 1
grw₄ : HMul.hMul (α := ℝ) 1 1 ≤ 1
grw₅ grw₆ : LE.le (α := ℝ) 1 1
⊢ ⟪x, y⟫ * ⟪x, y⟫ ≤ 1

Tactic:
grw [← sq, sq_le_one_iff_abs_le_one, abs_real_inner_le_norm, hx, hy, one_mul]

Premises used: abs_real_inner_le_norm, sq, sq_le_one_iff_abs_le_one, one_mul
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
simp : ortho y x = 0 ∨ ⟪y, ortho y x⟫ = 0
⊢ ⟪y, NormedSpace.normalize (ortho y x)⟫ = 0

Tactic:
simp only [NormedSpace.normalize, real_inner_smul_right, mul_eq_zero, inv_eq_zero, norm_eq_zero]

Premises used: norm_eq_zero, inv_eq_zero, mul_eq_zero, real_inner_smul_right, NormedSpace.normalize
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪y, ortho y x⟫ = 0
⊢ ortho y x = 0 ∨ ⟪y, ortho y x⟫ = 0

Tactic:
right
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ y) y
⊢ ⟪y, ortho y x⟫ = 0

Tactic:
rw [ortho, real_inner_comm, Submodule.starProjection_inner_eq_zero]

Premises used: Submodule.starProjection_inner_eq_zero, _private.0.InnerProductGeometry.ortho, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ y) y

Tactic:
Submodule.mem_span_singleton_self y

Premises used: Set.Mem, Submodule.mem_span_singleton_self
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ y) y

Tactic:
exact Submodule.mem_span_singleton_self y

Premises used: Submodule.mem_span_singleton_self
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
rw : HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
⊢ HPow.hPow (β := ℕ) ⟪x, NormedSpace.normalize (ortho y x)⟫ 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1

Tactic:
rw [NormedSpace.normalize, real_inner_smul_right, ortho_eq_sub_inner _ hy, inner_sub_right,
    real_inner_smul_right]

Premises used: real_inner_smul_right, inner_sub_right, _private.0.InnerProductGeometry.ortho_eq_sub_inner, NormedSpace.normalize
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
pos :
  ∀ (h₁ : x = y),
    HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
neg :
  ∀ (h₁ : ¬x = y),
    HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
⊢ HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1

Tactic:
by_cases h₁ : x = y
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : x = y
⊢ HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
pos :
  ∀ (h₂ : x = -y),
    HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
neg :
  ∀ (h₂ : ¬x = -y),
    HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1
⊢ HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1

Tactic:
by_cases h₂ : x = -y
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : x = -y
⊢ HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
neg :
  HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (HPow.hPow (α := ℝ) (β := ℕ) 1 2 - ⟪y, x⟫ * ⟪x, y⟫)) 2 +
      HPow.hPow (β := ℕ) ⟪x, y⟫ 2 =
    1
⊢ HPow.hPow (β := ℕ) (‖x - ⟪y, x⟫ • y‖⁻¹ * (⟪x, x⟫ - ⟪y, x⟫ * ⟪x, y⟫)) 2 + HPow.hPow (β := ℕ) ⟪x, y⟫ 2 = 1

Tactic:
rw [real_inner_self_eq_norm_sq, hx]

Premises used: real_inner_self_eq_norm_sq
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
simp : ¬x = ⟪y, x⟫ • y
⊢ ‖x - ⟪y, x⟫ • y‖ ≠ 0

Tactic:
simp only [ne_eq, norm_eq_zero, sub_eq_zero]

Premises used: norm_eq_zero, sub_eq_zero, ne_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
⊢ |⟪y, x⟫| = 1

Tactic:
rw [H2, norm_smul, hy, Real.norm_eq_abs, mul_one] at hx

Premises used: norm_smul, mul_one, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
hx₁ : |⟪y, x⟫| = 1
⊢ ‖y‖ = 1

Tactic:
rw [H2, norm_smul, hy, Real.norm_eq_abs, mul_one] at hx

Premises used: norm_smul, mul_one, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
hx₁ : |⟪y, x⟫| = 1
hy₁ : ‖y‖ = 1
⊢ ¬x = y

Tactic:
rw [H2, norm_smul, hy, Real.norm_eq_abs, mul_one] at hx

Premises used: norm_smul, mul_one, Real.norm_eq_abs