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

Tactic:
rw [sub_eq_add_neg, angle_add_eq_arccos_of_inner_eq_zero h]

Premises used: sub_eq_add_neg, InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ ⟪x, -y⟫ = 0

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Premises used: inner_neg_right, neg_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
h₁ : ⟪x, -y⟫ = 0
⊢ x ≠ 0 ∨ y ≠ 0

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Premises used: inner_neg_right, neg_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ x ≠ 0 ∨ -y ≠ 0

Tactic:
rw [or_comm, ← neg_ne_zero, or_comm] at h0

Premises used: neg_ne_zero, or_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0 ∨ -y ≠ 0
rw : angle x (x + -y) = Real.arcsin (‖y‖ / ‖x + -y‖)
rw₁ : Real.arcsin (‖-y‖ / ‖x + -y‖) = Real.arcsin (‖y‖ / ‖x + -y‖)
rw₂ rw₃ : Real.arcsin (‖y‖ / ‖x + -y‖) = Real.arcsin (‖y‖ / ‖x + -y‖)
⊢ angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)

Tactic:
rw [sub_eq_add_neg, angle_add_eq_arcsin_of_inner_eq_zero h h0, norm_neg]

Premises used: sub_eq_add_neg, norm_neg, InnerProductGeometry.angle_add_eq_arcsin_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
⊢ ⟪x, -y⟫ = 0

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Premises used: inner_neg_right, neg_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0
h₁ : ⟪x, -y⟫ = 0
⊢ x ≠ 0

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Premises used: inner_neg_right, neg_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0
rw : angle x (x + -y) = Real.arctan (‖y‖ / ‖x‖)
rw₁ : Real.arctan (‖-y‖ / ‖x‖) = Real.arctan (‖y‖ / ‖x‖)
rw₂ rw₃ : Real.arctan (‖y‖ / ‖x‖) = Real.arctan (‖y‖ / ‖x‖)
⊢ angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)

Tactic:
rw [sub_eq_add_neg, angle_add_eq_arctan_of_inner_eq_zero h h0, norm_neg]

Premises used: sub_eq_add_neg, InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero, norm_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ⟪x, -y⟫ = 0

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Premises used: inner_neg_right, neg_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0 ∨ y ≠ 0
h₁ : ⟪x, -y⟫ = 0
⊢ x = 0 ∨ y ≠ 0

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Premises used: inner_neg_right, neg_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x = 0 ∨ y ≠ 0
⊢ x = 0 ∨ -y ≠ 0

Tactic:
rw [← neg_ne_zero] at h0

Premises used: neg_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x = 0 ∨ -y ≠ 0
rw : 0 < angle x (x + -y)
⊢ 0 < angle x (x - y)

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ 0 < angle x (x + -y)

Tactic:
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
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ 0 < angle x (x + -y)

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
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
rw : angle x (x + -y) ≤ π / 2
⊢ angle x (x - y) ≤ π / 2

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
⊢ angle x (x + -y) ≤ π / 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
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
⊢ angle x (x + -y) ≤ π / 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
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0
rw : angle x (x + -y) < π / 2
⊢ angle x (x - y) < π / 2

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0
⊢ angle x (x + -y) < π / 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
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0
⊢ angle x (x + -y) < π / 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
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
rw : Real.cos (angle x (x + -y)) = ‖x‖ / ‖x + -y‖
rw₁ rw₂ : ‖x‖ / ‖x + -y‖ = ‖x‖ / ‖x + -y‖
⊢ Real.cos (angle x (x - y)) = ‖x‖ / ‖x - y‖

Tactic:
rw [sub_eq_add_neg, cos_angle_add_of_inner_eq_zero h]

Premises used: InnerProductGeometry.cos_angle_add_of_inner_eq_zero, sub_eq_add_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0 ∨ -y ≠ 0
rw : Real.sin (angle x (x + -y)) = ‖y‖ / ‖x + -y‖
rw₁ : ‖-y‖ / ‖x + -y‖ = ‖y‖ / ‖x + -y‖
rw₂ rw₃ : ‖y‖ / ‖x + -y‖ = ‖y‖ / ‖x + -y‖
⊢ Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖

Tactic:
rw [sub_eq_add_neg, sin_angle_add_of_inner_eq_zero h h0, norm_neg]

Premises used: sub_eq_add_neg, norm_neg, InnerProductGeometry.sin_angle_add_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
rw : Real.tan (angle x (x + -y)) = ‖y‖ / ‖x‖
rw₁ : ‖-y‖ / ‖x‖ = ‖y‖ / ‖x‖
rw₂ rw₃ : ‖y‖ / ‖x‖ = ‖y‖ / ‖x‖
⊢ Real.tan (angle x (x - y)) = ‖y‖ / ‖x‖

Tactic:
rw [sub_eq_add_neg, tan_angle_add_of_inner_eq_zero h, norm_neg]

Premises used: sub_eq_add_neg, InnerProductGeometry.tan_angle_add_of_inner_eq_zero, norm_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
rw : Real.cos (angle x (x + -y)) * ‖x + -y‖ = ‖x‖
rw₁ rw₂ : ‖x‖ = ‖x‖
⊢ Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖

Tactic:
rw [sub_eq_add_neg, cos_angle_add_mul_norm_of_inner_eq_zero h]

Premises used: sub_eq_add_neg, InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
rw : Real.sin (angle x (x + -y)) * ‖x + -y‖ = ‖y‖
rw₁ : ‖-y‖ = ‖y‖
rw₂ rw₃ : ‖y‖ = ‖y‖
⊢ Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖

Tactic:
rw [sub_eq_add_neg, sin_angle_add_mul_norm_of_inner_eq_zero h, norm_neg]

Premises used: sub_eq_add_neg, norm_neg, InnerProductGeometry.sin_angle_add_mul_norm_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y = 0
⊢ ⟪x, -y⟫ = 0

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Premises used: inner_neg_right, neg_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y = 0
h₁ : ⟪x, -y⟫ = 0
⊢ x ≠ 0 ∨ y = 0

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Premises used: inner_neg_right, neg_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0 ∨ y = 0
⊢ x ≠ 0 ∨ -y = 0

Tactic:
rw [← neg_eq_zero] at h0

Premises used: neg_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0 ∨ -y = 0
rw : Real.tan (angle x (x + -y)) * ‖x‖ = ‖y‖
rw₁ : ‖-y‖ = ‖y‖
rw₂ rw₃ : ‖y‖ = ‖y‖
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖

Tactic:
rw [sub_eq_add_neg, tan_angle_add_mul_norm_of_inner_eq_zero h h0, norm_neg]

Premises used: InnerProductGeometry.tan_angle_add_mul_norm_of_inner_eq_zero, sub_eq_add_neg, norm_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0 ∨ -y = 0
rw : ‖x‖ / Real.cos (angle x (x + -y)) = ‖x + -y‖
rw₁ rw₂ : ‖x + -y‖ = ‖x + -y‖
⊢ ‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖

Tactic:
rw [sub_eq_add_neg, norm_div_cos_angle_add_of_inner_eq_zero h h0]

Premises used: sub_eq_add_neg, InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x = 0 ∨ -y ≠ 0
rw : ‖y‖ / Real.sin (angle x (x + -y)) = ‖x + -y‖
rw₁ : ‖-y‖ / Real.sin (angle x (x + -y)) = ‖x + -y‖
rw₂ rw₃ : ‖x + -y‖ = ‖x + -y‖
⊢ ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖

Tactic:
rw [sub_eq_add_neg, ← norm_neg, norm_div_sin_angle_add_of_inner_eq_zero h h0]

Premises used: sub_eq_add_neg, InnerProductGeometry.norm_div_sin_angle_add_of_inner_eq_zero, norm_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x = 0 ∨ -y ≠ 0
rw : ‖y‖ / Real.tan (angle x (x + -y)) = ‖x‖
rw₁ : ‖-y‖ / Real.tan (angle x (x + -y)) = ‖x‖
rw₂ rw₃ : ‖x‖ = ‖x‖
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖

Tactic:
rw [sub_eq_add_neg, ← norm_neg, norm_div_tan_angle_add_of_inner_eq_zero h h0]

Premises used: sub_eq_add_neg, InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero, norm_neg
-- 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
erw : dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₂ p₃ * dist p₂ p₃ ↔ ∠ p₁ p₂ p₃ = π / 2
erw₁ : ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = dist p₁ p₂ * dist p₁ p₂ + dist p₂ p₃ * dist p₂ p₃ ↔ ∠ p₁ p₂ p₃ = π / 2
erw₂ : ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + dist p₂ p₃ * dist p₂ p₃ ↔ ∠ p₁ p₂ p₃ = π / 2
erw₃ : ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₂ -ᵥ p₃‖ * ‖p₂ -ᵥ p₃‖ ↔ ∠ p₁ p₂ p₃ = π / 2
erw₄ :
  ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₂ -ᵥ p₃‖ * ‖p₂ -ᵥ p₃‖ ↔
    ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ * ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖
erw₅ :
  ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₂ -ᵥ p₃‖ * ‖p₂ -ᵥ p₃‖ ↔
    ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖
erw₆ :
  ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₂ -ᵥ p₃‖ * ‖p₂ -ᵥ p₃‖ ↔
    ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖-(p₂ -ᵥ p₃)‖ * ‖-(p₂ -ᵥ p₃)‖
erw₇ erw₈ :
  ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₂ -ᵥ p₃‖ * ‖p₂ -ᵥ p₃‖ ↔
    ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₂ -ᵥ p₃‖ * ‖p₂ -ᵥ p₃‖
⊢ dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π / 2

Tactic:
erw [dist_comm p₃ p₂, dist_eq_norm_vsub V p₁ p₃, dist_eq_norm_vsub V p₁ p₂,
    dist_eq_norm_vsub V p₂ p₃, ← norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two,
    vsub_sub_vsub_cancel_right p₁, ← neg_vsub_eq_vsub_rev p₂ p₃, norm_neg]

Premises used: InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two, dist_comm, vsub_sub_vsub_cancel_right, norm_neg, neg_vsub_eq_vsub_rev, dist_eq_norm_vsub
-- 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
⊢ ⟪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₁ -ᵥ p₂⟫ = 0
rw : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
rw₁ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arccos (‖p₂ -ᵥ p₃‖ / dist p₁ p₃)
rw₂ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arccos (‖p₂ -ᵥ p₃‖ / ‖p₁ -ᵥ p₃‖)
rw₃ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) = Real.arccos (‖p₂ -ᵥ p₃‖ / ‖p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)‖)
rw₄ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) = Real.arccos (‖p₂ -ᵥ p₃‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖)
rw₅ rw₆ : Real.arccos (‖p₂ -ᵥ p₃‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖) = Real.arccos (‖p₂ -ᵥ p₃‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖)
⊢ ∠ p₂ p₃ p₁ = Real.arccos (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, angle_add_eq_arccos_of_inner_eq_zero h]

Premises used: vsub_add_vsub_cancel, dist_eq_norm_vsub', add_comm, InnerProductGeometry.angle_add_eq_arccos_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₃ = π / 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 [← @vsub_ne_zero V, @ne_comm _ p₃, ← @vsub_ne_zero V _ _ _ p₂, or_comm] at h0

Premises used: vsub_ne_zero, 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 : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
rw₁ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arcsin (‖p₁ -ᵥ p₂‖ / dist p₁ p₃)
rw₂ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arcsin (‖p₁ -ᵥ p₂‖ / ‖p₁ -ᵥ p₃‖)
rw₃ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) = Real.arcsin (‖p₁ -ᵥ p₂‖ / ‖p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)‖)
rw₄ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) = Real.arcsin (‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖)
rw₅ rw₆ : Real.arcsin (‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖) = Real.arcsin (‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖)
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (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, angle_add_eq_arcsin_of_inner_eq_zero h h0]

Premises used: vsub_add_vsub_cancel, add_comm, dist_eq_norm_vsub, InnerProductGeometry.angle_add_eq_arcsin_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₂⟫ = 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₂
h₁ : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
⊢ 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₃ ≠ 0

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

Premises used: vsub_ne_zero, ne_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
rw : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
rw₁ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arctan (‖p₁ -ᵥ p₂‖ / dist p₃ p₂)
rw₂ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arctan (‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖)
rw₃ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) = Real.arctan (‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖)
rw₄ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) = Real.arctan (‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖)
rw₅ rw₆ : Real.arctan (‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖) = Real.arctan (‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖)
⊢ ∠ p₂ p₃ p₁ = Real.arctan (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, angle_add_eq_arctan_of_inner_eq_zero h h0]

Premises used: vsub_add_vsub_cancel, InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero, 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₃ = π / 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 [← @vsub_ne_zero V, eq_comm, ← @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 : 0 < InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))
⊢ 0 < ∠ p₂ p₃ p₁

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 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ 0 < InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))

Tactic:
angle_add_pos_of_inner_eq_zero h h0

Premises used: InnerProductGeometry.angle_add_pos_of_inner_eq_zero