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
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₃)‖)
⊢ ∠ 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]
-- 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₃‖)
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₂)‖)
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
have rw₅ : Real.arccos (‖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]
-- 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₂
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (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₂
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (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
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
have rw : InnerProductGeometry.angle (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]
-- 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 : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
have rw₁ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arcsin (‖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]
-- 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 : 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₃)
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
have rw₂ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arcsin (‖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_arcsin_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 : 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₃‖)
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
have rw₃ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) = Real.arcsin (‖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_arcsin_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 : 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₃)‖)
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
have rw₄ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) = Real.arcsin (‖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_arcsin_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 : 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₂)‖)
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
have rw₅ : Real.arcsin (‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖) = Real.arcsin (‖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_arcsin_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₃ p₁ = Real.arctan (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₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
have h0₁ : p₂ -ᵥ p₃ ≠ 0
Tactic: rw [ne_comm, ← @vsub_ne_zero V] 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₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
have rw : InnerProductGeometry.angle (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]
-- 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
rw : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
have rw₁ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arctan (‖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]
-- 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
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₂)
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
have rw₂ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arctan (‖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_arctan_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
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₃‖)
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
have rw₃ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) = Real.arctan (‖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_arctan_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
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₃‖)
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
have rw₄ : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) = Real.arctan (‖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_arctan_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
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₃‖)
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
have rw₅ : Real.arctan (‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖) = Real.arctan (‖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_arctan_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₂
⊢ 0 < ∠ p₂ 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₂
⊢ 0 < ∠ p₂ p₃ p₁
have h0₁ : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
Tactic: rw [← @vsub_ne_zero V, eq_comm, ← @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
⊢ 0 < ∠ p₂ p₃ p₁
have rw : 0 < InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))
Tactic: rw [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]
-- 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₁ ≤ π / 2
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₁ ≤ π / 2
have rw : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) ≤ π / 2
Tactic: rw [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]
-- 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₃ p₁ < π / 2
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₃ p₁ < π / 2
have h0₁ : p₂ -ᵥ p₃ ≠ 0
Tactic: rw [ne_comm, ← @vsub_ne_zero V] 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₃ p₁ < π / 2
have rw : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) < π / 2
Tactic: rw [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]
-- 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_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₃)) = ‖p₂ -ᵥ p₃‖ / dist p₁ p₃
Tactic: rw [angle, dist_eq_norm_vsub' V p₃ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, cos_angle_add_of_inner_eq_zero h]
-- 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₃)) = ‖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₃)) = ‖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_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₃)) = ‖p₂ -ᵥ p₃‖ / dist 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_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₃)) = ‖p₂ -ᵥ p₃‖ / dist p₁ p₃
rw₂ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₂ -ᵥ p₃‖ / ‖p₁ -ᵥ p₃‖
rw₃ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃))) = ‖p₂ -ᵥ p₃‖ / ‖p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)‖
⊢ 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_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₃)) = ‖p₂ -ᵥ p₃‖ / dist p₁ p₃
rw₂ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)) = ‖p₂ -ᵥ p₃‖ / ‖p₁ -ᵥ p₃‖
rw₃ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃))) = ‖p₂ -ᵥ p₃‖ / ‖p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)‖
rw₄ : Real.cos (InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))) = ‖p₂ -ᵥ p₃‖ / ‖p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)‖
⊢ Real.cos (∠ 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, cos_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
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ 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, h0