[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ oangle o x (x + y) = ↑(Real.arccos (‖x‖ / ‖x + y‖))
[PROOFSTEP]
have hs : (o.oangle x (x + y)).sign = 1 := by rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o x (x + y)) = 1
[PROOFSTEP]
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o x (x + y)) = 1
⊢ oangle o x (x + y) = ↑(Real.arccos (‖x‖ / ‖x + y‖))
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs,
  InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ oangle o (x + y) y = ↑(Real.arccos (‖y‖ / ‖x + y‖))
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ oangle (-o) y (x + y) = ↑(Real.arccos (‖y‖ / ‖x + y‖))
[PROOFSTEP]
rw [add_comm]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ oangle (-o) y (y + x) = ↑(Real.arccos (‖y‖ / ‖y + x‖))
[PROOFSTEP]
exact (-o).oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ oangle o x (x + y) = ↑(Real.arcsin (‖y‖ / ‖x + y‖))
[PROOFSTEP]
have hs : (o.oangle x (x + y)).sign = 1 := by rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o x (x + y)) = 1
[PROOFSTEP]
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o x (x + y)) = 1
⊢ oangle o x (x + y) = ↑(Real.arcsin (‖y‖ / ‖x + y‖))
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs,
  InnerProductGeometry.angle_add_eq_arcsin_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.left_ne_zero_of_oangle_eq_pi_div_two h))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ oangle o (x + y) y = ↑(Real.arcsin (‖x‖ / ‖x + y‖))
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ oangle (-o) y (x + y) = ↑(Real.arcsin (‖x‖ / ‖x + y‖))
[PROOFSTEP]
rw [add_comm]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ oangle (-o) y (y + x) = ↑(Real.arcsin (‖x‖ / ‖y + x‖))
[PROOFSTEP]
exact (-o).oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ oangle o x (x + y) = ↑(Real.arctan (‖y‖ / ‖x‖))
[PROOFSTEP]
have hs : (o.oangle x (x + y)).sign = 1 := by rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o x (x + y)) = 1
[PROOFSTEP]
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o x (x + y)) = 1
⊢ oangle o x (x + y) = ↑(Real.arctan (‖y‖ / ‖x‖))
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs,
  InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
    (o.left_ne_zero_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ oangle o (x + y) y = ↑(Real.arctan (‖x‖ / ‖y‖))
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ oangle (-o) y (x + y) = ↑(Real.arctan (‖x‖ / ‖y‖))
[PROOFSTEP]
rw [add_comm]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ oangle (-o) y (y + x) = ↑(Real.arctan (‖x‖ / ‖y‖))
[PROOFSTEP]
exact (-o).oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.cos (oangle o x (x + y)) = ‖x‖ / ‖x + y‖
[PROOFSTEP]
have hs : (o.oangle x (x + y)).sign = 1 := by rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o x (x + y)) = 1
[PROOFSTEP]
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o x (x + y)) = 1
⊢ Real.Angle.cos (oangle o x (x + y)) = ‖x‖ / ‖x + y‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  InnerProductGeometry.cos_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.cos (oangle o (x + y) y) = ‖y‖ / ‖x + y‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.cos (oangle (-o) y (x + y)) = ‖y‖ / ‖x + y‖
[PROOFSTEP]
rw [add_comm]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.cos (oangle (-o) y (y + x)) = ‖y‖ / ‖y + x‖
[PROOFSTEP]
exact (-o).cos_oangle_add_right_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sin (oangle o x (x + y)) = ‖y‖ / ‖x + y‖
[PROOFSTEP]
have hs : (o.oangle x (x + y)).sign = 1 := by rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o x (x + y)) = 1
[PROOFSTEP]
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o x (x + y)) = 1
⊢ Real.Angle.sin (oangle o x (x + y)) = ‖y‖ / ‖x + y‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  InnerProductGeometry.sin_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.left_ne_zero_of_oangle_eq_pi_div_two h))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sin (oangle o (x + y) y) = ‖x‖ / ‖x + y‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.sin (oangle (-o) y (x + y)) = ‖x‖ / ‖x + y‖
[PROOFSTEP]
rw [add_comm]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.sin (oangle (-o) y (y + x)) = ‖x‖ / ‖y + x‖
[PROOFSTEP]
exact (-o).sin_oangle_add_right_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.tan (oangle o x (x + y)) = ‖y‖ / ‖x‖
[PROOFSTEP]
have hs : (o.oangle x (x + y)).sign = 1 := by rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o x (x + y)) = 1
[PROOFSTEP]
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o x (x + y)) = 1
⊢ Real.Angle.tan (oangle o x (x + y)) = ‖y‖ / ‖x‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  InnerProductGeometry.tan_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.tan (oangle o (x + y) y) = ‖x‖ / ‖y‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.tan (oangle (-o) y (x + y)) = ‖x‖ / ‖y‖
[PROOFSTEP]
rw [add_comm]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.tan (oangle (-o) y (y + x)) = ‖x‖ / ‖y‖
[PROOFSTEP]
exact (-o).tan_oangle_add_right_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.cos (oangle o x (x + y)) * ‖x + y‖ = ‖x‖
[PROOFSTEP]
have hs : (o.oangle x (x + y)).sign = 1 := by rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o x (x + y)) = 1
[PROOFSTEP]
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o x (x + y)) = 1
⊢ Real.Angle.cos (oangle o x (x + y)) * ‖x + y‖ = ‖x‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.cos (oangle o (x + y) y) * ‖x + y‖ = ‖y‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.cos (oangle (-o) y (x + y)) * ‖x + y‖ = ‖y‖
[PROOFSTEP]
rw [add_comm]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.cos (oangle (-o) y (y + x)) * ‖y + x‖ = ‖y‖
[PROOFSTEP]
exact (-o).cos_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sin (oangle o x (x + y)) * ‖x + y‖ = ‖y‖
[PROOFSTEP]
have hs : (o.oangle x (x + y)).sign = 1 := by rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o x (x + y)) = 1
[PROOFSTEP]
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o x (x + y)) = 1
⊢ Real.Angle.sin (oangle o x (x + y)) * ‖x + y‖ = ‖y‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  InnerProductGeometry.sin_angle_add_mul_norm_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sin (oangle o (x + y) y) * ‖x + y‖ = ‖x‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.sin (oangle (-o) y (x + y)) * ‖x + y‖ = ‖x‖
[PROOFSTEP]
rw [add_comm]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.sin (oangle (-o) y (y + x)) * ‖y + x‖ = ‖x‖
[PROOFSTEP]
exact (-o).sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.tan (oangle o x (x + y)) * ‖x‖ = ‖y‖
[PROOFSTEP]
have hs : (o.oangle x (x + y)).sign = 1 := by rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o x (x + y)) = 1
[PROOFSTEP]
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o x (x + y)) = 1
⊢ Real.Angle.tan (oangle o x (x + y)) * ‖x‖ = ‖y‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  InnerProductGeometry.tan_angle_add_mul_norm_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.left_ne_zero_of_oangle_eq_pi_div_two h))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.tan (oangle o (x + y) y) * ‖y‖ = ‖x‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.tan (oangle (-o) y (x + y)) * ‖y‖ = ‖x‖
[PROOFSTEP]
rw [add_comm]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.tan (oangle (-o) y (y + x)) * ‖y‖ = ‖x‖
[PROOFSTEP]
exact (-o).tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ ‖x‖ / Real.Angle.cos (oangle o x (x + y)) = ‖x + y‖
[PROOFSTEP]
have hs : (o.oangle x (x + y)).sign = 1 := by rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o x (x + y)) = 1
[PROOFSTEP]
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o x (x + y)) = 1
⊢ ‖x‖ / Real.Angle.cos (oangle o x (x + y)) = ‖x + y‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.left_ne_zero_of_oangle_eq_pi_div_two h))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ ‖y‖ / Real.Angle.cos (oangle o (x + y) y) = ‖x + y‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ ‖y‖ / Real.Angle.cos (oangle (-o) y (x + y)) = ‖x + y‖
[PROOFSTEP]
rw [add_comm]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ ‖y‖ / Real.Angle.cos (oangle (-o) y (y + x)) = ‖y + x‖
[PROOFSTEP]
exact (-o).norm_div_cos_oangle_add_right_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ ‖y‖ / Real.Angle.sin (oangle o x (x + y)) = ‖x + y‖
[PROOFSTEP]
have hs : (o.oangle x (x + y)).sign = 1 := by rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o x (x + y)) = 1
[PROOFSTEP]
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o x (x + y)) = 1
⊢ ‖y‖ / Real.Angle.sin (oangle o x (x + y)) = ‖x + y‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  InnerProductGeometry.norm_div_sin_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inr (o.right_ne_zero_of_oangle_eq_pi_div_two h))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ ‖x‖ / Real.Angle.sin (oangle o (x + y) y) = ‖x + y‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ ‖x‖ / Real.Angle.sin (oangle (-o) y (x + y)) = ‖x + y‖
[PROOFSTEP]
rw [add_comm]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ ‖x‖ / Real.Angle.sin (oangle (-o) y (y + x)) = ‖y + x‖
[PROOFSTEP]
exact (-o).norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ ‖y‖ / Real.Angle.tan (oangle o x (x + y)) = ‖x‖
[PROOFSTEP]
have hs : (o.oangle x (x + y)).sign = 1 := by rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o x (x + y)) = 1
[PROOFSTEP]
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o x (x + y)) = 1
⊢ ‖y‖ / Real.Angle.tan (oangle o x (x + y)) = ‖x‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inr (o.right_ne_zero_of_oangle_eq_pi_div_two h))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ ‖x‖ / Real.Angle.tan (oangle o (x + y) y) = ‖y‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ ‖x‖ / Real.Angle.tan (oangle (-o) y (x + y)) = ‖y‖
[PROOFSTEP]
rw [add_comm]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ ‖x‖ / Real.Angle.tan (oangle (-o) y (y + x)) = ‖y‖
[PROOFSTEP]
exact (-o).norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ oangle o y (y - x) = ↑(Real.arccos (‖y‖ / ‖y - x‖))
[PROOFSTEP]
have hs : (o.oangle y (y - x)).sign = 1 := by rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o y (y - x)) = 1
[PROOFSTEP]
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o y (y - x)) = 1
⊢ oangle o y (y - x) = ↑(Real.arccos (‖y‖ / ‖y - x‖))
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs,
  InnerProductGeometry.angle_sub_eq_arccos_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ oangle o (x - y) x = ↑(Real.arccos (‖x‖ / ‖x - y‖))
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ oangle (-o) x (x - y) = ↑(Real.arccos (‖x‖ / ‖x - y‖))
[PROOFSTEP]
exact (-o).oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ oangle o y (y - x) = ↑(Real.arcsin (‖x‖ / ‖y - x‖))
[PROOFSTEP]
have hs : (o.oangle y (y - x)).sign = 1 := by rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o y (y - x)) = 1
[PROOFSTEP]
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o y (y - x)) = 1
⊢ oangle o y (y - x) = ↑(Real.arcsin (‖x‖ / ‖y - x‖))
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs,
  InnerProductGeometry.angle_sub_eq_arcsin_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.right_ne_zero_of_oangle_eq_pi_div_two h))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ oangle o (x - y) x = ↑(Real.arcsin (‖y‖ / ‖x - y‖))
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ oangle (-o) x (x - y) = ↑(Real.arcsin (‖y‖ / ‖x - y‖))
[PROOFSTEP]
exact (-o).oangle_sub_right_eq_arcsin_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ oangle o y (y - x) = ↑(Real.arctan (‖x‖ / ‖y‖))
[PROOFSTEP]
have hs : (o.oangle y (y - x)).sign = 1 := by rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o y (y - x)) = 1
[PROOFSTEP]
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o y (y - x)) = 1
⊢ oangle o y (y - x) = ↑(Real.arctan (‖x‖ / ‖y‖))
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs,
  InnerProductGeometry.angle_sub_eq_arctan_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
    (o.right_ne_zero_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ oangle o (x - y) x = ↑(Real.arctan (‖y‖ / ‖x‖))
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ oangle (-o) x (x - y) = ↑(Real.arctan (‖y‖ / ‖x‖))
[PROOFSTEP]
exact (-o).oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.cos (oangle o y (y - x)) = ‖y‖ / ‖y - x‖
[PROOFSTEP]
have hs : (o.oangle y (y - x)).sign = 1 := by rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o y (y - x)) = 1
[PROOFSTEP]
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o y (y - x)) = 1
⊢ Real.Angle.cos (oangle o y (y - x)) = ‖y‖ / ‖y - x‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  InnerProductGeometry.cos_angle_sub_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.cos (oangle o (x - y) x) = ‖x‖ / ‖x - y‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.cos (oangle (-o) x (x - y)) = ‖x‖ / ‖x - y‖
[PROOFSTEP]
exact (-o).cos_oangle_sub_right_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sin (oangle o y (y - x)) = ‖x‖ / ‖y - x‖
[PROOFSTEP]
have hs : (o.oangle y (y - x)).sign = 1 := by rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o y (y - x)) = 1
[PROOFSTEP]
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o y (y - x)) = 1
⊢ Real.Angle.sin (oangle o y (y - x)) = ‖x‖ / ‖y - x‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  InnerProductGeometry.sin_angle_sub_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.right_ne_zero_of_oangle_eq_pi_div_two h))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sin (oangle o (x - y) x) = ‖y‖ / ‖x - y‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.sin (oangle (-o) x (x - y)) = ‖y‖ / ‖x - y‖
[PROOFSTEP]
exact (-o).sin_oangle_sub_right_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.tan (oangle o y (y - x)) = ‖x‖ / ‖y‖
[PROOFSTEP]
have hs : (o.oangle y (y - x)).sign = 1 := by rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o y (y - x)) = 1
[PROOFSTEP]
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o y (y - x)) = 1
⊢ Real.Angle.tan (oangle o y (y - x)) = ‖x‖ / ‖y‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  InnerProductGeometry.tan_angle_sub_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.tan (oangle o (x - y) x) = ‖y‖ / ‖x‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.tan (oangle (-o) x (x - y)) = ‖y‖ / ‖x‖
[PROOFSTEP]
exact (-o).tan_oangle_sub_right_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.cos (oangle o y (y - x)) * ‖y - x‖ = ‖y‖
[PROOFSTEP]
have hs : (o.oangle y (y - x)).sign = 1 := by rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o y (y - x)) = 1
[PROOFSTEP]
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o y (y - x)) = 1
⊢ Real.Angle.cos (oangle o y (y - x)) * ‖y - x‖ = ‖y‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  InnerProductGeometry.cos_angle_sub_mul_norm_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.cos (oangle o (x - y) x) * ‖x - y‖ = ‖x‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.cos (oangle (-o) x (x - y)) * ‖x - y‖ = ‖x‖
[PROOFSTEP]
exact (-o).cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sin (oangle o y (y - x)) * ‖y - x‖ = ‖x‖
[PROOFSTEP]
have hs : (o.oangle y (y - x)).sign = 1 := by rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o y (y - x)) = 1
[PROOFSTEP]
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o y (y - x)) = 1
⊢ Real.Angle.sin (oangle o y (y - x)) * ‖y - x‖ = ‖x‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  InnerProductGeometry.sin_angle_sub_mul_norm_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sin (oangle o (x - y) x) * ‖x - y‖ = ‖y‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.sin (oangle (-o) x (x - y)) * ‖x - y‖ = ‖y‖
[PROOFSTEP]
exact (-o).sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.tan (oangle o y (y - x)) * ‖y‖ = ‖x‖
[PROOFSTEP]
have hs : (o.oangle y (y - x)).sign = 1 := by rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o y (y - x)) = 1
[PROOFSTEP]
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o y (y - x)) = 1
⊢ Real.Angle.tan (oangle o y (y - x)) * ‖y‖ = ‖x‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  InnerProductGeometry.tan_angle_sub_mul_norm_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.right_ne_zero_of_oangle_eq_pi_div_two h))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.tan (oangle o (x - y) x) * ‖x‖ = ‖y‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ Real.Angle.tan (oangle (-o) x (x - y)) * ‖x‖ = ‖y‖
[PROOFSTEP]
exact (-o).tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ ‖y‖ / Real.Angle.cos (oangle o y (y - x)) = ‖y - x‖
[PROOFSTEP]
have hs : (o.oangle y (y - x)).sign = 1 := by rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o y (y - x)) = 1
[PROOFSTEP]
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o y (y - x)) = 1
⊢ ‖y‖ / Real.Angle.cos (oangle o y (y - x)) = ‖y - x‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  InnerProductGeometry.norm_div_cos_angle_sub_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.right_ne_zero_of_oangle_eq_pi_div_two h))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ ‖x‖ / Real.Angle.cos (oangle o (x - y) x) = ‖x - y‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ ‖x‖ / Real.Angle.cos (oangle (-o) x (x - y)) = ‖x - y‖
[PROOFSTEP]
exact (-o).norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ ‖x‖ / Real.Angle.sin (oangle o y (y - x)) = ‖y - x‖
[PROOFSTEP]
have hs : (o.oangle y (y - x)).sign = 1 := by rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o y (y - x)) = 1
[PROOFSTEP]
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o y (y - x)) = 1
⊢ ‖x‖ / Real.Angle.sin (oangle o y (y - x)) = ‖y - x‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  InnerProductGeometry.norm_div_sin_angle_sub_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inr (o.left_ne_zero_of_oangle_eq_pi_div_two h))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ ‖y‖ / Real.Angle.sin (oangle o (x - y) x) = ‖x - y‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ ‖y‖ / Real.Angle.sin (oangle (-o) x (x - y)) = ‖x - y‖
[PROOFSTEP]
exact (-o).norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ ‖x‖ / Real.Angle.tan (oangle o y (y - x)) = ‖y‖
[PROOFSTEP]
have hs : (o.oangle y (y - x)).sign = 1 := by rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ Real.Angle.sign (oangle o y (y - x)) = 1
[PROOFSTEP]
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
hs : Real.Angle.sign (oangle o y (y - x)) = 1
⊢ ‖x‖ / Real.Angle.tan (oangle o y (y - x)) = ‖y‖
[PROOFSTEP]
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  InnerProductGeometry.norm_div_tan_angle_sub_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inr (o.left_ne_zero_of_oangle_eq_pi_div_two h))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : oangle o x y = ↑(π / 2)
⊢ ‖y‖ / Real.Angle.tan (oangle o (x - y) x) = ‖x‖
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h✝ : oangle o x y = ↑(π / 2)
h : oangle (-o) y x = ↑(π / 2)
⊢ ‖y‖ / Real.Angle.tan (oangle (-o) x (x - y)) = ‖x‖
[PROOFSTEP]
exact (-o).norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
⊢ oangle o x (x + r • ↑(rotation o ↑(π / 2)) x) = ↑(Real.arctan r)
[PROOFSTEP]
rcases lt_trichotomy r 0 with (hr | rfl | hr)
[GOAL]
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ oangle o x (x + r • ↑(rotation o ↑(π / 2)) x) = ↑(Real.arctan r)
[PROOFSTEP]
have ha : o.oangle x (r • o.rotation (π / 2 : ℝ) x) = -(π / 2 : ℝ) :=
  by
  rw [o.oangle_smul_right_of_neg _ _ hr, o.oangle_neg_right h, o.oangle_rotation_self_right h, ← sub_eq_zero, add_comm,
    sub_neg_eq_add, ← Real.Angle.coe_add, ← Real.Angle.coe_add, add_assoc, add_halves, ← two_mul, Real.Angle.coe_two_pi]
  simpa using h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ oangle o x (r • ↑(rotation o ↑(π / 2)) x) = -↑(π / 2)
[PROOFSTEP]
rw [o.oangle_smul_right_of_neg _ _ hr, o.oangle_neg_right h, o.oangle_rotation_self_right h, ← sub_eq_zero, add_comm,
  sub_neg_eq_add, ← Real.Angle.coe_add, ← Real.Angle.coe_add, add_assoc, add_halves, ← two_mul, Real.Angle.coe_two_pi]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ ↑(rotation o ↑(π / 2)) x ≠ 0
[PROOFSTEP]
simpa using h
[GOAL]
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
ha : oangle o x (r • ↑(rotation o ↑(π / 2)) x) = -↑(π / 2)
⊢ oangle o x (x + r • ↑(rotation o ↑(π / 2)) x) = ↑(Real.arctan r)
[PROOFSTEP]
rw [← neg_inj, ← oangle_neg_orientation_eq_neg, @neg_neg Real.Angle] at ha
[GOAL]
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
ha✝ : oangle o x (r • ↑(rotation o ↑(π / 2)) x) = -↑(π / 2)
ha : oangle (-o) x (r • ↑(rotation o ↑(π / 2)) x) = ↑(π / 2)
⊢ oangle o x (x + r • ↑(rotation o ↑(π / 2)) x) = ↑(Real.arctan r)
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj, oangle_rev,
  (-o).oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two ha, norm_smul, LinearIsometryEquiv.norm_map, mul_div_assoc,
  div_self (norm_ne_zero_iff.2 h), mul_one, Real.norm_eq_abs, abs_of_neg hr, Real.arctan_neg, Real.Angle.coe_neg,
  neg_neg]
[GOAL]
case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
⊢ oangle o x (x + 0 • ↑(rotation o ↑(π / 2)) x) = ↑(Real.arctan 0)
[PROOFSTEP]
rw [zero_smul, add_zero, oangle_self, Real.arctan_zero, Real.Angle.coe_zero]
[GOAL]
case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 0 < r
⊢ oangle o x (x + r • ↑(rotation o ↑(π / 2)) x) = ↑(Real.arctan r)
[PROOFSTEP]
have ha : o.oangle x (r • o.rotation (π / 2 : ℝ) x) = (π / 2 : ℝ) := by
  rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right h]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 0 < r
⊢ oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(π / 2)
[PROOFSTEP]
rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right h]
[GOAL]
case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 0 < r
ha : oangle o x (r • ↑(rotation o ↑(π / 2)) x) = ↑(π / 2)
⊢ oangle o x (x + r • ↑(rotation o ↑(π / 2)) x) = ↑(Real.arctan r)
[PROOFSTEP]
rw [o.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two ha, norm_smul, LinearIsometryEquiv.norm_map, mul_div_assoc,
  div_self (norm_ne_zero_iff.2 h), mul_one, Real.norm_eq_abs, abs_of_pos hr]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
⊢ oangle o (x + r • ↑(rotation o ↑(π / 2)) x) (r • ↑(rotation o ↑(π / 2)) x) = ↑(Real.arctan r⁻¹)
[PROOFSTEP]
by_cases hr : r = 0
[GOAL]
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ oangle o (x + r • ↑(rotation o ↑(π / 2)) x) (r • ↑(rotation o ↑(π / 2)) x) = ↑(Real.arctan r⁻¹)
[PROOFSTEP]
simp [hr]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ oangle o (x + r • ↑(rotation o ↑(π / 2)) x) (r • ↑(rotation o ↑(π / 2)) x) = ↑(Real.arctan r⁻¹)
[PROOFSTEP]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj, ← neg_neg ((π / 2 : ℝ) : Real.Angle), ←
  rotation_neg_orientation_eq_neg, add_comm]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ oangle (-o) (r • ↑(rotation (-o) (-↑(π / 2))) x) (r • ↑(rotation (-o) (-↑(π / 2))) x + x) = ↑(Real.arctan r⁻¹)
[PROOFSTEP]
have hx : x = r⁻¹ • (-o).rotation (π / 2 : ℝ) (r • (-o).rotation (-(π / 2 : ℝ)) x) := by simp [hr]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ x = r⁻¹ • ↑(rotation (-o) ↑(π / 2)) (r • ↑(rotation (-o) (-↑(π / 2))) x)
[PROOFSTEP]
simp [hr]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : x = r⁻¹ • ↑(rotation (-o) ↑(π / 2)) (r • ↑(rotation (-o) (-↑(π / 2))) x)
⊢ oangle (-o) (r • ↑(rotation (-o) (-↑(π / 2))) x) (r • ↑(rotation (-o) (-↑(π / 2))) x + x) = ↑(Real.arctan r⁻¹)
[PROOFSTEP]
nth_rw 3 [hx]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : x = r⁻¹ • ↑(rotation (-o) ↑(π / 2)) (r • ↑(rotation (-o) (-↑(π / 2))) x)
⊢ oangle (-o) (r • ↑(rotation (-o) (-↑(π / 2))) x)
      (r • ↑(rotation (-o) (-↑(π / 2))) x + r⁻¹ • ↑(rotation (-o) ↑(π / 2)) (r • ↑(rotation (-o) (-↑(π / 2))) x)) =
    ↑(Real.arctan r⁻¹)
[PROOFSTEP]
refine' (-o).oangle_add_right_smul_rotation_pi_div_two _ _
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : x = r⁻¹ • ↑(rotation (-o) ↑(π / 2)) (r • ↑(rotation (-o) (-↑(π / 2))) x)
⊢ r • ↑(rotation (-o) (-↑(π / 2))) x ≠ 0
[PROOFSTEP]
simp [hr, h]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
⊢ Real.Angle.tan (oangle o x (x + r • ↑(rotation o ↑(π / 2)) x)) = r
[PROOFSTEP]
rw [o.oangle_add_right_smul_rotation_pi_div_two h, Real.Angle.tan_coe, Real.tan_arctan]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
⊢ Real.Angle.tan (oangle o (x + r • ↑(rotation o ↑(π / 2)) x) (r • ↑(rotation o ↑(π / 2)) x)) = r⁻¹
[PROOFSTEP]
rw [o.oangle_add_left_smul_rotation_pi_div_two h, Real.Angle.tan_coe, Real.tan_arctan]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
⊢ oangle o (r • ↑(rotation o ↑(π / 2)) x) (r • ↑(rotation o ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)
[PROOFSTEP]
by_cases hr : r = 0
[GOAL]
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ oangle o (r • ↑(rotation o ↑(π / 2)) x) (r • ↑(rotation o ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)
[PROOFSTEP]
simp [hr]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ oangle o (r • ↑(rotation o ↑(π / 2)) x) (r • ↑(rotation o ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)
[PROOFSTEP]
have hx : -x = r⁻¹ • o.rotation (π / 2 : ℝ) (r • o.rotation (π / 2 : ℝ) x) := by simp [hr, ← Real.Angle.coe_add]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ -x = r⁻¹ • ↑(rotation o ↑(π / 2)) (r • ↑(rotation o ↑(π / 2)) x)
[PROOFSTEP]
simp [hr, ← Real.Angle.coe_add]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : -x = r⁻¹ • ↑(rotation o ↑(π / 2)) (r • ↑(rotation o ↑(π / 2)) x)
⊢ oangle o (r • ↑(rotation o ↑(π / 2)) x) (r • ↑(rotation o ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)
[PROOFSTEP]
rw [sub_eq_add_neg, hx, o.oangle_add_right_smul_rotation_pi_div_two]
[GOAL]
case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : -x = r⁻¹ • ↑(rotation o ↑(π / 2)) (r • ↑(rotation o ↑(π / 2)) x)
⊢ r • ↑(rotation o ↑(π / 2)) x ≠ 0
[PROOFSTEP]
simpa [hr] using h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
⊢ oangle o (x - r • ↑(rotation o ↑(π / 2)) x) x = ↑(Real.arctan r)
[PROOFSTEP]
by_cases hr : r = 0
[GOAL]
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ oangle o (x - r • ↑(rotation o ↑(π / 2)) x) x = ↑(Real.arctan r)
[PROOFSTEP]
simp [hr]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ oangle o (x - r • ↑(rotation o ↑(π / 2)) x) x = ↑(Real.arctan r)
[PROOFSTEP]
have hx : x = r⁻¹ • o.rotation (π / 2 : ℝ) (-(r • o.rotation (π / 2 : ℝ) x)) := by simp [hr, ← Real.Angle.coe_add]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ x = r⁻¹ • ↑(rotation o ↑(π / 2)) (-(r • ↑(rotation o ↑(π / 2)) x))
[PROOFSTEP]
simp [hr, ← Real.Angle.coe_add]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : x = r⁻¹ • ↑(rotation o ↑(π / 2)) (-(r • ↑(rotation o ↑(π / 2)) x))
⊢ oangle o (x - r • ↑(rotation o ↑(π / 2)) x) x = ↑(Real.arctan r)
[PROOFSTEP]
rw [sub_eq_add_neg, add_comm]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : x = r⁻¹ • ↑(rotation o ↑(π / 2)) (-(r • ↑(rotation o ↑(π / 2)) x))
⊢ oangle o (-(r • ↑(rotation o ↑(π / 2)) x) + x) x = ↑(Real.arctan r)
[PROOFSTEP]
nth_rw 3 [hx]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : x = r⁻¹ • ↑(rotation o ↑(π / 2)) (-(r • ↑(rotation o ↑(π / 2)) x))
⊢ oangle o (-(r • ↑(rotation o ↑(π / 2)) x) + x) (r⁻¹ • ↑(rotation o ↑(π / 2)) (-(r • ↑(rotation o ↑(π / 2)) x))) =
    ↑(Real.arctan r)
[PROOFSTEP]
nth_rw 2 [hx]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : x = r⁻¹ • ↑(rotation o ↑(π / 2)) (-(r • ↑(rotation o ↑(π / 2)) x))
⊢ oangle o (-(r • ↑(rotation o ↑(π / 2)) x) + r⁻¹ • ↑(rotation o ↑(π / 2)) (-(r • ↑(rotation o ↑(π / 2)) x)))
      (r⁻¹ • ↑(rotation o ↑(π / 2)) (-(r • ↑(rotation o ↑(π / 2)) x))) =
    ↑(Real.arctan r)
[PROOFSTEP]
rw [o.oangle_add_left_smul_rotation_pi_div_two, inv_inv]
[GOAL]
case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : x = r⁻¹ • ↑(rotation o ↑(π / 2)) (-(r • ↑(rotation o ↑(π / 2)) x))
⊢ -(r • ↑(rotation o ↑(π / 2)) x) ≠ 0
[PROOFSTEP]
simpa [hr] using h
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∡ p₂ p₃ p₁ = ↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃))
[PROOFSTEP]
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₂ p₃ p₁) = 1
[PROOFSTEP]
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₂ p₃ p₁) = 1
⊢ ∡ p₂ p₃ p₁ = ↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃))
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs,
  angle_eq_arccos_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃))
[PROOFSTEP]
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₃ p₁ p₂) = 1
[PROOFSTEP]
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₃ p₁ p₂) = 1
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃))
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm,
  angle_eq_arccos_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h), dist_comm p₁ p₃]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∡ p₂ p₃ p₁ = ↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃))
[PROOFSTEP]
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₂ p₃ p₁) = 1
[PROOFSTEP]
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₂ p₃ p₁) = 1
⊢ ∡ p₂ p₃ p₁ = ↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃))
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs,
  angle_eq_arcsin_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))]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃))
[PROOFSTEP]
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₃ p₁ p₂) = 1
[PROOFSTEP]
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₃ p₁ p₂) = 1
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃))
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm,
  angle_eq_arcsin_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)),
  dist_comm p₁ p₃]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∡ p₂ p₃ p₁ = ↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂))
[PROOFSTEP]
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₂ p₃ p₁) = 1
[PROOFSTEP]
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₂ p₃ p₁) = 1
⊢ ∡ p₂ p₃ p₁ = ↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂))
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs,
  angle_eq_arctan_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (right_ne_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂))
[PROOFSTEP]
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₃ p₁ p₂) = 1
[PROOFSTEP]
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₃ p₁ p₂) = 1
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂))
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm,
  angle_eq_arctan_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (left_ne_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.cos (∡ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃
[PROOFSTEP]
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₂ p₃ p₁) = 1
[PROOFSTEP]
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₂ p₃ p₁) = 1
⊢ Real.Angle.cos (∡ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  cos_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.cos (∡ p₃ p₁ p₂) = dist p₁ p₂ / dist p₁ p₃
[PROOFSTEP]
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₃ p₁ p₂) = 1
[PROOFSTEP]
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₃ p₁ p₂) = 1
⊢ Real.Angle.cos (∡ p₃ p₁ p₂) = dist p₁ p₂ / dist p₁ p₃
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe,
  cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h), dist_comm p₁ p₃]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sin (∡ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
[PROOFSTEP]
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₂ p₃ p₁) = 1
[PROOFSTEP]
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₂ p₃ p₁) = 1
⊢ Real.Angle.sin (∡ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  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))]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sin (∡ p₃ p₁ p₂) = dist p₃ p₂ / dist p₁ p₃
[PROOFSTEP]
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₃ p₁ p₂) = 1
[PROOFSTEP]
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₃ p₁ p₂) = 1
⊢ Real.Angle.sin (∡ p₃ p₁ p₂) = dist p₃ p₂ / dist p₁ p₃
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe,
  sin_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)),
  dist_comm p₁ p₃]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.tan (∡ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
[PROOFSTEP]
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₂ p₃ p₁) = 1
[PROOFSTEP]
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₂ p₃ p₁) = 1
⊢ Real.Angle.tan (∡ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  tan_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.tan (∡ p₃ p₁ p₂) = dist p₃ p₂ / dist p₁ p₂
[PROOFSTEP]
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₃ p₁ p₂) = 1
[PROOFSTEP]
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₃ p₁ p₂) = 1
⊢ Real.Angle.tan (∡ p₃ p₁ p₂) = dist p₃ p₂ / dist p₁ p₂
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
  tan_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.cos (∡ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
[PROOFSTEP]
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₂ p₃ p₁) = 1
[PROOFSTEP]
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₂ p₃ p₁) = 1
⊢ Real.Angle.cos (∡ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  cos_angle_mul_dist_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.cos (∡ p₃ p₁ p₂) * dist p₁ p₃ = dist p₁ p₂
[PROOFSTEP]
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₃ p₁ p₂) = 1
[PROOFSTEP]
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₃ p₁ p₂) = 1
⊢ Real.Angle.cos (∡ p₃ p₁ p₂) * dist p₁ p₃ = dist p₁ p₂
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe, dist_comm p₁ p₃,
  cos_angle_mul_dist_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sin (∡ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
[PROOFSTEP]
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₂ p₃ p₁) = 1
[PROOFSTEP]
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₂ p₃ p₁) = 1
⊢ Real.Angle.sin (∡ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  sin_angle_mul_dist_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sin (∡ p₃ p₁ p₂) * dist p₁ p₃ = dist p₃ p₂
[PROOFSTEP]
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₃ p₁ p₂) = 1
[PROOFSTEP]
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₃ p₁ p₂) = 1
⊢ Real.Angle.sin (∡ p₃ p₁ p₂) * dist p₁ p₃ = dist p₃ p₂
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe, dist_comm p₁ p₃,
  sin_angle_mul_dist_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.tan (∡ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
[PROOFSTEP]
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₂ p₃ p₁) = 1
[PROOFSTEP]
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₂ p₃ p₁) = 1
⊢ Real.Angle.tan (∡ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
[PROOFSTEP]
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  tan_angle_mul_dist_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))]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.tan (∡ p₃ p₁ p₂) * dist p₁ p₂ = dist p₃ p₂
[PROOFSTEP]
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₃ p₁ p₂) = 1
[PROOFSTEP]
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₃ p₁ p₂) = 1
⊢ Real.Angle.tan (∡ p₃ p₁ p₂) * dist p₁ p₂ = dist p₃ p₂
[PROOFSTEP]
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))]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ dist p₃ p₂ / Real.Angle.cos (∡ p₂ p₃ p₁) = dist p₁ p₃
[PROOFSTEP]
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₂ p₃ p₁) = 1
[PROOFSTEP]
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₂ p₃ p₁) = 1
⊢ dist p₃ p₂ / Real.Angle.cos (∡ p₂ p₃ p₁) = dist p₁ p₃
[PROOFSTEP]
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))]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ dist p₁ p₂ / Real.Angle.cos (∡ p₃ p₁ p₂) = dist p₁ p₃
[PROOFSTEP]
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₃ p₁ p₂) = 1
[PROOFSTEP]
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₃ p₁ p₂) = 1
⊢ dist p₁ p₂ / Real.Angle.cos (∡ p₃ p₁ p₂) = dist p₁ p₃
[PROOFSTEP]
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))]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ dist p₁ p₂ / Real.Angle.sin (∡ p₂ p₃ p₁) = dist p₁ p₃
[PROOFSTEP]
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₂ p₃ p₁) = 1
[PROOFSTEP]
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₂ p₃ p₁) = 1
⊢ dist p₁ p₂ / Real.Angle.sin (∡ p₂ p₃ p₁) = dist p₁ p₃
[PROOFSTEP]
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))]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ dist p₃ p₂ / Real.Angle.sin (∡ p₃ p₁ p₂) = dist p₁ p₃
[PROOFSTEP]
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₃ p₁ p₂) = 1
[PROOFSTEP]
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₃ p₁ p₂) = 1
⊢ dist p₃ p₂ / Real.Angle.sin (∡ p₃ p₁ p₂) = dist p₁ p₃
[PROOFSTEP]
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))]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ dist p₁ p₂ / Real.Angle.tan (∡ p₂ p₃ p₁) = dist p₃ p₂
[PROOFSTEP]
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₂ p₃ p₁) = 1
[PROOFSTEP]
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₂ p₃ p₁) = 1
⊢ dist p₁ p₂ / Real.Angle.tan (∡ p₂ p₃ p₁) = dist p₃ p₂
[PROOFSTEP]
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))]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ dist p₃ p₂ / Real.Angle.tan (∡ p₃ p₁ p₂) = dist p₁ p₂
[PROOFSTEP]
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ Real.Angle.sign (∡ p₃ p₁ p₂) = 1
[PROOFSTEP]
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Module.Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : Real.Angle.sign (∡ p₃ p₁ p₂) = 1
⊢ dist p₃ p₂ / Real.Angle.tan (∡ p₃ p₁ p₂) = dist p₁ p₂
[PROOFSTEP]
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))]