awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
⊢ Real.tan (angle x (x - y)) = ‖y‖ / ‖x‖
have rw : Real.tan (angle x (x + -y)) = ‖y‖ / ‖x‖
Tactic: rw [sub_eq_add_neg, tan_angle_add_of_inner_eq_zero h, norm_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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‖
⊢ Real.tan (angle x (x - y)) = ‖y‖ / ‖x‖
have rw₁ : ‖-y‖ / ‖x‖ = ‖y‖ / ‖x‖
Tactic: rw [sub_eq_add_neg, tan_angle_add_of_inner_eq_zero h, norm_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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‖
⊢ Real.tan (angle x (x - y)) = ‖y‖ / ‖x‖
have rw₂ : ‖y‖ / ‖x‖ = ‖y‖ / ‖x‖
Tactic: rw [sub_eq_add_neg, tan_angle_add_of_inner_eq_zero h, norm_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖
have h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
⊢ Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖
have rw : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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‖
⊢ Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖
have rw₁ : ‖x‖ = ‖x‖
Tactic: rw [sub_eq_add_neg, cos_angle_add_mul_norm_of_inner_eq_zero h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖
have h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
⊢ Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖
have rw : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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‖
⊢ Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖
have rw₁ : ‖-y‖ = ‖y‖
Tactic: rw [sub_eq_add_neg, sin_angle_add_mul_norm_of_inner_eq_zero h, norm_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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‖
⊢ Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖
have rw₂ : ‖y‖ = ‖y‖
Tactic: rw [sub_eq_add_neg, sin_angle_add_mul_norm_of_inner_eq_zero h, norm_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y = 0
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖
have h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
Cleared hypotheses: h, h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0 ∨ y = 0
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖
have h0₁ : x ≠ 0 ∨ -y = 0
Tactic: rw [← neg_eq_zero] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0 ∨ -y = 0
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖
have rw : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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‖
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖
have rw₁ : ‖-y‖ = ‖y‖
Tactic: rw [sub_eq_add_neg, tan_angle_add_mul_norm_of_inner_eq_zero h h0, norm_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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‖
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖
have rw₂ : ‖y‖ = ‖y‖
Tactic: rw [sub_eq_add_neg, tan_angle_add_mul_norm_of_inner_eq_zero h h0, norm_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (hypothesis)
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‖ / Real.cos (angle x (x - y)) = ‖x - y‖
have h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
Cleared hypotheses: h, h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (hypothesis)
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‖ / Real.cos (angle x (x - y)) = ‖x - y‖
have h0₁ : x ≠ 0 ∨ -y = 0
Tactic: rw [← neg_eq_zero] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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‖ / Real.cos (angle x (x - y)) = ‖x - y‖
have rw : ‖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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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‖
⊢ ‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖
have rw₁ : ‖x + -y‖ = ‖x + -y‖
Tactic: rw [sub_eq_add_neg, norm_div_cos_angle_add_of_inner_eq_zero h h0]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖
have h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
Cleared hypotheses: h, h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖
have h0₁ : x = 0 ∨ -y ≠ 0
Tactic: rw [← neg_ne_zero] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖
have rw : ‖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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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‖
⊢ ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖
have rw₁ : ‖-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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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‖
⊢ ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖
have rw₂ : ‖x + -y‖ = ‖x + -y‖
Tactic: rw [sub_eq_add_neg, ← norm_neg, norm_div_sin_angle_add_of_inner_eq_zero h h0]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖
have h₁ : ⟪x, -y⟫ = 0
Tactic: rw [← neg_eq_zero, ← inner_neg_right] at h
Cleared hypotheses: h, h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖
have h0₁ : x = 0 ∨ -y ≠ 0
Tactic: rw [← neg_ne_zero] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖
have rw : ‖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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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‖
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖
have rw₁ : ‖-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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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‖
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖
have rw₂ : ‖x‖ = ‖x‖
Tactic: rw [sub_eq_add_neg, ← norm_neg, norm_div_tan_angle_add_of_inner_eq_zero h h0]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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
⊢ dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π / 2
have erw : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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
⊢ dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π / 2
have erw₁ : ‖p₁ -ᵥ p₃‖ * ‖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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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
⊢ dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π / 2
have erw₂ : ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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
⊢ dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π / 2
have erw₃ : ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₂ -ᵥ p₃‖ * ‖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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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
⊢ dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π / 2
have 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₂‖
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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₂‖
⊢ dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π / 2
have 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₂‖
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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₂‖
⊢ dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π / 2
have 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₃)‖
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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₃)‖
⊢ dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π / 2
have 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₃‖
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (hypothesis)
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₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
have h₁ : ⟪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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
have rw : InnerProductGeometry.angle (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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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₃)
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
have rw₁ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arccos (‖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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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₃)
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
have rw₂ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arccos (‖p₂ -ᵥ p₃‖ / ‖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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle (goal)
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₃‖)
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
have rw₃ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) = Real.arccos (‖p₂ -ᵥ p₃‖ / ‖p₁ -ᵥ p₂ + (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]