awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ -ᵥ p₂⟫ = 0
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
have h0₁ : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ ≠ 0
Tactic: rw [← @vsub_ne_zero V, @ne_comm _ p₃, ← @vsub_ne_zero V _ _ _ p₂, or_comm] at h0
Cleared hypotheses: 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
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
have rw : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ 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]
-- 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
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ ≠ 0
rw : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₁ p₂ / dist p₁ p₃
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
have rw₁ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ 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, 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
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₃
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
have rw₂ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (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, 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
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₃‖
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
have rw₃ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃))) = ‖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, 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
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₃)‖
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
have rw₄ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))) = ‖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, 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
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₂)‖
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
have rw₅ : ‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖ = ‖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, 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
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
⊢ Real.tan (∠ p₂ p₃ p₁) = 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
⊢ Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
have rw : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ 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]
-- 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 : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = dist p₁ p₂ / dist p₃ p₂
⊢ Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
have rw₁ : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ 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, tan_angle_add_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 : 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₂
⊢ Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
have rw₂ : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (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, tan_angle_add_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 : 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₃‖
⊢ Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
have rw₃ : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (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, tan_angle_add_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 : 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₃‖
⊢ Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
have rw₄ : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (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, tan_angle_add_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 : 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₃‖
⊢ Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
have rw₅ : ‖p₁ -ᵥ p₂‖ / ‖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, tan_angle_add_of_inner_eq_zero h]
-- 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
⊢ Real.cos (∠ p₂ p₃ p₁) * 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
⊢ Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
have rw : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ 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]
-- 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 : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist p₁ p₃ = dist p₃ p₂
⊢ Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
have rw₁ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist 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, 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
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₃‖
⊢ Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
have rw₂ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (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, 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
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₃‖
⊢ Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
have rw₃ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃))) * ‖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, 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
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₃‖
⊢ Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
have rw₄ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))) * ‖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, 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
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₃‖
⊢ Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
have rw₅ : ‖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, 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
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
⊢ Real.sin (∠ p₂ p₃ p₁) * 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
⊢ Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
have rw : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ 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]
-- 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 : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist p₁ p₃ = dist p₁ p₂
⊢ Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
have rw₁ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist 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, sin_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
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₂‖
⊢ Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
have rw₂ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (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, sin_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
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₂‖
⊢ Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
have rw₃ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃))) * ‖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, sin_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
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₂‖
⊢ Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
have rw₄ : Real.sin (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))) * ‖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, sin_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
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₂‖
⊢ Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
have rw₅ : ‖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, sin_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
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₂
⊢ Real.tan (∠ p₂ p₃ p₁) * 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, h0
-- 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₁ -ᵥ p₂⟫ = 0
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
have h0₁ : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
Tactic: rw [ne_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, or_comm] at h0
Cleared hypotheses: 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
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
have rw : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ 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]
-- 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
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
rw : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist p₃ p₂ = dist p₁ p₂
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
have rw₁ : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist 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, tan_angle_add_mul_norm_of_inner_eq_zero h h0]