awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ (∡ p₃ p₁ p₂).tan * dist p₁ p₂ = dist p₃ p₂
have hs : (∡ p₃ p₁ p₂).sign = 1
Tactic: have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).tan * dist p₁ p₂ = dist p₃ p₂
have rw : (↑(∠ p₃ p₁ p₂) : Real.Angle).tan * dist p₁ p₂ = dist p₃ p₂
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
    tan_angle_mul_dist_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle).tan * dist p₁ p₂ = dist p₃ p₂
⊢ (∡ p₃ p₁ p₂).tan * dist p₁ p₂ = dist p₃ p₂
have rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle).tan * dist p₁ p₂ = dist p₃ p₂
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
    tan_angle_mul_dist_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle).tan * dist p₁ p₂ = dist p₃ p₂
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle).tan * dist p₁ p₂ = dist p₃ p₂
⊢ (∡ p₃ p₁ p₂).tan * dist p₁ p₂ = dist p₃ p₂
have rw₂ : Real.tan (∠ p₂ p₁ p₃) * dist p₁ p₂ = dist p₃ p₂
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
    tan_angle_mul_dist_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle).tan * dist p₁ p₂ = dist p₃ p₂
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle).tan * dist p₁ p₂ = dist p₃ p₂
rw₂ : Real.tan (∠ p₂ p₁ p₃) * dist p₁ p₂ = dist p₃ p₂
⊢ (∡ p₃ p₁ p₂).tan * dist p₁ p₂ = dist p₃ p₂
have rw₃ : dist p₃ p₂ = dist p₃ p₂
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
    tan_angle_mul_dist_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ dist p₃ p₂ / (∡ p₂ p₃ p₁).cos = dist p₁ p₃
have hs : (∡ p₂ p₃ p₁).sign = 1
Tactic: have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ dist p₃ p₂ / (∡ p₂ p₃ p₁).cos = dist p₁ p₃
have rw : dist p₃ p₂ / (↑(∠ p₂ p₃ p₁) : Real.Angle).cos = dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    dist_div_cos_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (right_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : dist p₃ p₂ / (↑(∠ p₂ p₃ p₁) : Real.Angle).cos = dist p₁ p₃
⊢ dist p₃ p₂ / (∡ p₂ p₃ p₁).cos = dist p₁ p₃
have rw₁ : dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    dist_div_cos_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (right_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : dist p₃ p₂ / (↑(∠ p₂ p₃ p₁) : Real.Angle).cos = dist p₁ p₃
rw₁ : dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
⊢ dist p₃ p₂ / (∡ p₂ p₃ p₁).cos = dist p₁ p₃
have rw₂ : dist p₁ p₃ = dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    dist_div_cos_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (right_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ dist p₁ p₂ / (∡ p₃ p₁ p₂).cos = dist p₁ p₃
have hs : (∡ p₃ p₁ p₂).sign = 1
Tactic: have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ dist p₁ p₂ / (∡ p₃ p₁ p₂).cos = dist p₁ p₃
have rw : dist p₁ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).cos = dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe, dist_comm p₁ p₃,
    dist_div_cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : dist p₁ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).cos = dist p₁ p₃
⊢ dist p₁ p₂ / (∡ p₃ p₁ p₂).cos = dist p₁ p₃
have rw₁ : dist p₁ p₂ / (↑(∠ p₂ p₁ p₃) : Real.Angle).cos = dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe, dist_comm p₁ p₃,
    dist_div_cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : dist p₁ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).cos = dist p₁ p₃
rw₁ : dist p₁ p₂ / (↑(∠ p₂ p₁ p₃) : Real.Angle).cos = dist p₁ p₃
⊢ dist p₁ p₂ / (∡ p₃ p₁ p₂).cos = dist p₁ p₃
have rw₂ : dist p₁ p₂ / Real.cos (∠ p₂ p₁ p₃) = dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe, dist_comm p₁ p₃,
    dist_div_cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : dist p₁ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).cos = dist p₁ p₃
rw₁ : dist p₁ p₂ / (↑(∠ p₂ p₁ p₃) : Real.Angle).cos = dist p₁ p₃
rw₂ : dist p₁ p₂ / Real.cos (∠ p₂ p₁ p₃) = dist p₁ p₃
⊢ dist p₁ p₂ / (∡ p₃ p₁ p₂).cos = dist p₁ p₃
have rw₃ : dist p₁ p₂ / Real.cos (∠ p₂ p₁ p₃) = dist p₃ p₁
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe, dist_comm p₁ p₃,
    dist_div_cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : dist p₁ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).cos = dist p₁ p₃
rw₁ : dist p₁ p₂ / (↑(∠ p₂ p₁ p₃) : Real.Angle).cos = dist p₁ p₃
rw₂ : dist p₁ p₂ / Real.cos (∠ p₂ p₁ p₃) = dist p₁ p₃
rw₃ : dist p₁ p₂ / Real.cos (∠ p₂ p₁ p₃) = dist p₃ p₁
⊢ dist p₁ p₂ / (∡ p₃ p₁ p₂).cos = dist p₁ p₃
have rw₄ : dist p₃ p₁ = dist p₃ p₁
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe, dist_comm p₁ p₃,
    dist_div_cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).sin = dist p₁ p₃
have hs : (∡ p₂ p₃ p₁).sign = 1
Tactic: have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).sin = dist p₁ p₃
have rw : dist p₁ p₂ / (↑(∠ p₂ p₃ p₁) : Real.Angle).sin = dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    dist_div_sin_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : dist p₁ p₂ / (↑(∠ p₂ p₃ p₁) : Real.Angle).sin = dist p₁ p₃
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).sin = dist p₁ p₃
have rw₁ : dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    dist_div_sin_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : dist p₁ p₂ / (↑(∠ p₂ p₃ p₁) : Real.Angle).sin = dist p₁ p₃
rw₁ : dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).sin = dist p₁ p₃
have rw₂ : dist p₁ p₃ = dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    dist_div_sin_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).sin = dist p₁ p₃
have hs : (∡ p₃ p₁ p₂).sign = 1
Tactic: have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).sin = dist p₁ p₃
have rw : dist p₃ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).sin = dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe, dist_comm p₁ p₃,
    dist_div_sin_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (right_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : dist p₃ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).sin = dist p₁ p₃
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).sin = dist p₁ p₃
have rw₁ : dist p₃ p₂ / (↑(∠ p₂ p₁ p₃) : Real.Angle).sin = dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe, dist_comm p₁ p₃,
    dist_div_sin_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (right_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : dist p₃ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).sin = dist p₁ p₃
rw₁ : dist p₃ p₂ / (↑(∠ p₂ p₁ p₃) : Real.Angle).sin = dist p₁ p₃
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).sin = dist p₁ p₃
have rw₂ : dist p₃ p₂ / Real.sin (∠ p₂ p₁ p₃) = dist p₁ p₃
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe, dist_comm p₁ p₃,
    dist_div_sin_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (right_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : dist p₃ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).sin = dist p₁ p₃
rw₁ : dist p₃ p₂ / (↑(∠ p₂ p₁ p₃) : Real.Angle).sin = dist p₁ p₃
rw₂ : dist p₃ p₂ / Real.sin (∠ p₂ p₁ p₃) = dist p₁ p₃
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).sin = dist p₁ p₃
have rw₃ : dist p₃ p₂ / Real.sin (∠ p₂ p₁ p₃) = dist p₃ p₁
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe, dist_comm p₁ p₃,
    dist_div_sin_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (right_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : dist p₃ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).sin = dist p₁ p₃
rw₁ : dist p₃ p₂ / (↑(∠ p₂ p₁ p₃) : Real.Angle).sin = dist p₁ p₃
rw₂ : dist p₃ p₂ / Real.sin (∠ p₂ p₁ p₃) = dist p₁ p₃
rw₃ : dist p₃ p₂ / Real.sin (∠ p₂ p₁ p₃) = dist p₃ p₁
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).sin = dist p₁ p₃
have rw₄ : dist p₃ p₁ = dist p₃ p₁
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe, dist_comm p₁ p₃,
    dist_div_sin_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (right_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).tan = dist p₃ p₂
have hs : (∡ p₂ p₃ p₁).sign = 1
Tactic: have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).tan = dist p₃ p₂
have rw : dist p₁ p₂ / (↑(∠ p₂ p₃ p₁) : Real.Angle).tan = dist p₃ p₂
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    dist_div_tan_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : dist p₁ p₂ / (↑(∠ p₂ p₃ p₁) : Real.Angle).tan = dist p₃ p₂
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).tan = dist p₃ p₂
have rw₁ : dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    dist_div_tan_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : dist p₁ p₂ / (↑(∠ p₂ p₃ p₁) : Real.Angle).tan = dist p₃ p₂
rw₁ : dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
⊢ dist p₁ p₂ / (∡ p₂ p₃ p₁).tan = dist p₃ p₂
have rw₂ : dist p₃ p₂ = dist p₃ p₂
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    dist_div_tan_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (left_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).tan = dist p₁ p₂
have hs : (∡ p₃ p₁ p₂).sign = 1
Tactic: have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).tan = dist p₁ p₂
have rw : dist p₃ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).tan = dist p₁ p₂
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
    dist_div_tan_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (right_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : dist p₃ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).tan = dist p₁ p₂
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).tan = dist p₁ p₂
have rw₁ : dist p₃ p₂ / (↑(∠ p₂ p₁ p₃) : Real.Angle).tan = dist p₁ p₂
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
    dist_div_tan_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (right_ne_of_oangle_eq_pi_div_two h))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : dist p₃ p₂ / (↑(∠ p₃ p₁ p₂) : Real.Angle).tan = dist p₁ p₂
rw₁ : dist p₃ p₂ / (↑(∠ p₂ p₁ p₃) : Real.Angle).tan = dist p₁ p₂
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).tan = dist p₁ p₂
have rw₂ : dist p₃ p₂ / Real.tan (∠ p₂ p₁ p₃) = dist p₁ p₂
Tactic: rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
    dist_div_tan_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (right_ne_of_oangle_eq_pi_div_two h))]