awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
rw₁ : Real.tan (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) * dist 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₂‖
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₂
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₂‖
⊢ 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_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₂
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₂‖
⊢ 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_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₂
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₂‖
⊢ Real.tan (∠ 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, tan_angle_add_mul_norm_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
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ dist p₃ p₂ / Real.cos (∠ p₂ 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₂
⊢ dist p₃ p₂ / Real.cos (∠ p₂ 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
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
have rw : dist p₃ p₂ / Real.cos (InnerProductGeometry.angle (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, 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
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₃
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
have rw₁ : ‖p₂ -ᵥ p₃‖ / Real.cos (InnerProductGeometry.angle (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, 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
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₃
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
have rw₂ : ‖p₂ -ᵥ p₃‖ / Real.cos (InnerProductGeometry.angle (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, 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
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₃‖
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
have rw₃ : ‖p₂ -ᵥ p₃‖ / Real.cos (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, 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
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₃)‖
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
have rw₄ : ‖p₂ -ᵥ p₃‖ / Real.cos (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, 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
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₂)‖
⊢ dist p₃ p₂ / Real.cos (∠ p₂ 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, 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
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₂
⊢ dist p₁ p₂ / Real.sin (∠ p₂ 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₂
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃
have h0₁ : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
Tactic: rw [eq_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
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃
have rw : dist p₁ p₂ / Real.sin (InnerProductGeometry.angle (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, 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
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₃
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃
have rw₁ : ‖p₁ -ᵥ p₂‖ / Real.sin (InnerProductGeometry.angle (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, 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
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₃
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃
have rw₂ : ‖p₁ -ᵥ p₂‖ / Real.sin (InnerProductGeometry.angle (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, 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
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₃‖
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃
have rw₃ : ‖p₁ -ᵥ p₂‖ / Real.sin (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, 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
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₃)‖
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃
have rw₄ : ‖p₁ -ᵥ p₂‖ / Real.sin (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, 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
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₂)‖
⊢ dist p₁ p₂ / Real.sin (∠ p₂ 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, 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
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₂
⊢ dist p₁ p₂ / Real.tan (∠ p₂ 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₂
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
have h0₁ : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
Tactic: rw [eq_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
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
have rw : dist p₁ p₂ / Real.tan (InnerProductGeometry.angle (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, 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
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₂
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
have rw₁ : ‖p₁ -ᵥ p₂‖ / Real.tan (InnerProductGeometry.angle (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, 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
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₂
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
have rw₂ : ‖p₁ -ᵥ p₂‖ / Real.tan (InnerProductGeometry.angle (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, 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
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₃‖
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
have rw₃ : ‖p₁ -ᵥ p₂‖ / 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, 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
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₃‖
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
have rw₄ : ‖p₁ -ᵥ p₂‖ / 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, 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
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₃‖
⊢ dist p₁ p₂ / Real.tan (∠ p₂ 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, norm_div_tan_angle_add_of_inner_eq_zero h h0]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : ‖y‖ = 1
⊢ ortho y x = x - ⟪y, x⟫ • y
have rw : HSub.hSub (β := V) x ((Submodule.starProjection (ℝ ∙ y) : (a : V) → V) x : V) = x - ⟪y, x⟫ • y
Tactic: rw [ortho, Submodule.starProjection_unit_singleton _ hy]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ ortho y x = x - ⟪y, x⟫ • y
have rw₁ : x - ⟪y, x⟫ • y = x - ⟪y, x⟫ • y
Tactic: rw [ortho, Submodule.starProjection_unit_singleton _ hy]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 0 ≤ ⟪x, ortho y x⟫
have rw : ⟪x, y⟫ * ⟪x, y⟫ ≤ 1
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, y⟫ * ⟪x, y⟫ ≤ 1
have grw : HPow.hPow (β := ℕ) ⟪x, y⟫ 2 ≤ 1
Tactic: grw [← sq, sq_le_one_iff_abs_le_one, abs_real_inner_le_norm, hx, hy, one_mul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality (goal)
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
⊢ ⟪x, y⟫ * ⟪x, y⟫ ≤ 1
have grw₁ : |⟪x, y⟫| ≤ 1
Tactic: grw [← sq, sq_le_one_iff_abs_le_one, abs_real_inner_le_norm, hx, hy, one_mul]