awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
rw :
  ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), (-o).oangle x (x - y) = (↑(Real.arctan (‖y‖ / ‖x‖)) : Real.Angle)
⊢ o.oangle (x - y) x = (↑(Real.arctan (‖y‖ / ‖x‖)) : Real.Angle)

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Premises used: neg_inj, Orientation.oangle_rev, Orientation.oangle_neg_orientation_eq_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ (-o).oangle x (x - y) = (↑(Real.arctan (‖y‖ / ‖x‖)) : Real.Angle)

Tactic:
(-o).oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two h

Premises used: Orientation.oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ (-o).oangle x (x - y) = (↑(Real.arctan (‖y‖ / ‖x‖)) : Real.Angle)

Tactic:
exact (-o).oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two h

Premises used: Orientation.oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle y (y - x)).sign = 1
rw : (↑(InnerProductGeometry.angle y (y - x)) : Real.Angle).cos = ‖y‖ / ‖y - x‖
rw₁ : Real.cos (InnerProductGeometry.angle y (y - x)) = ‖y‖ / ‖y - x‖
rw₂ rw₃ : ‖y‖ / ‖y - x‖ = ‖y‖ / ‖y - x‖
⊢ (o.oangle y (y - x)).cos = ‖y‖ / ‖y - x‖

Tactic:
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)]

Premises used: InnerProductGeometry.cos_angle_sub_of_inner_eq_zero, Orientation.oangle_eq_angle_of_sign_eq_one, Real.Angle.cos_coe, Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ((-o).oangle x (x - y)).cos = ‖x‖ / ‖x - y‖
⊢ (o.oangle (x - y) x).cos = ‖x‖ / ‖x - y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Premises used: neg_inj, Orientation.oangle_rev, Orientation.oangle_neg_orientation_eq_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle x (x - y)).cos = ‖x‖ / ‖x - y‖

Tactic:
(-o).cos_oangle_sub_right_of_oangle_eq_pi_div_two h

Premises used: Orientation.cos_oangle_sub_right_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle x (x - y)).cos = ‖x‖ / ‖x - y‖

Tactic:
exact (-o).cos_oangle_sub_right_of_oangle_eq_pi_div_two h

Premises used: Orientation.cos_oangle_sub_right_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle y (y - x)).sign = 1
rw : (↑(InnerProductGeometry.angle y (y - x)) : Real.Angle).sin = ‖x‖ / ‖y - x‖
rw₁ : Real.sin (InnerProductGeometry.angle y (y - x)) = ‖x‖ / ‖y - x‖
rw₂ rw₃ : ‖x‖ / ‖y - x‖ = ‖x‖ / ‖y - x‖
⊢ (o.oangle y (y - x)).sin = ‖x‖ / ‖y - x‖

Tactic:
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))]

Premises used: InnerProductGeometry.sin_angle_sub_of_inner_eq_zero, Orientation.oangle_eq_angle_of_sign_eq_one, Real.Angle.sin_coe, Orientation.right_ne_zero_of_oangle_eq_pi_div_two, Or.inl, Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ((-o).oangle x (x - y)).sin = ‖y‖ / ‖x - y‖
⊢ (o.oangle (x - y) x).sin = ‖y‖ / ‖x - y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Premises used: neg_inj, Orientation.oangle_rev, Orientation.oangle_neg_orientation_eq_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle x (x - y)).sin = ‖y‖ / ‖x - y‖

Tactic:
(-o).sin_oangle_sub_right_of_oangle_eq_pi_div_two h

Premises used: Orientation.sin_oangle_sub_right_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle x (x - y)).sin = ‖y‖ / ‖x - y‖

Tactic:
exact (-o).sin_oangle_sub_right_of_oangle_eq_pi_div_two h

Premises used: Orientation.sin_oangle_sub_right_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle y (y - x)).sign = 1
rw : (↑(InnerProductGeometry.angle y (y - x)) : Real.Angle).tan = ‖x‖ / ‖y‖
rw₁ : Real.tan (InnerProductGeometry.angle y (y - x)) = ‖x‖ / ‖y‖
rw₂ rw₃ : ‖x‖ / ‖y‖ = ‖x‖ / ‖y‖
⊢ (o.oangle y (y - x)).tan = ‖x‖ / ‖y‖

Tactic:
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)]

Premises used: InnerProductGeometry.tan_angle_sub_of_inner_eq_zero, Orientation.oangle_eq_angle_of_sign_eq_one, Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two, Real.Angle.tan_coe
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ((-o).oangle x (x - y)).tan = ‖y‖ / ‖x‖
⊢ (o.oangle (x - y) x).tan = ‖y‖ / ‖x‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Premises used: neg_inj, Orientation.oangle_rev, Orientation.oangle_neg_orientation_eq_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle x (x - y)).tan = ‖y‖ / ‖x‖

Tactic:
(-o).tan_oangle_sub_right_of_oangle_eq_pi_div_two h

Premises used: Orientation.tan_oangle_sub_right_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle x (x - y)).tan = ‖y‖ / ‖x‖

Tactic:
exact (-o).tan_oangle_sub_right_of_oangle_eq_pi_div_two h

Premises used: Orientation.tan_oangle_sub_right_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle y (y - x)).sign = 1
rw : (↑(InnerProductGeometry.angle y (y - x)) : Real.Angle).cos * ‖y - x‖ = ‖y‖
rw₁ : Real.cos (InnerProductGeometry.angle y (y - x)) * ‖y - x‖ = ‖y‖
rw₂ rw₃ : ‖y‖ = ‖y‖
⊢ (o.oangle y (y - x)).cos * ‖y - x‖ = ‖y‖

Tactic:
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)]

Premises used: Orientation.oangle_eq_angle_of_sign_eq_one, Real.Angle.cos_coe, InnerProductGeometry.cos_angle_sub_mul_norm_of_inner_eq_zero, Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ((-o).oangle x (x - y)).cos * ‖x - y‖ = ‖x‖
⊢ (o.oangle (x - y) x).cos * ‖x - y‖ = ‖x‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Premises used: neg_inj, Orientation.oangle_rev, Orientation.oangle_neg_orientation_eq_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle x (x - y)).cos * ‖x - y‖ = ‖x‖

Tactic:
(-o).cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two h

Premises used: Orientation.cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle x (x - y)).cos * ‖x - y‖ = ‖x‖

Tactic:
exact (-o).cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two h

Premises used: Orientation.cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle y (y - x)).sign = 1
rw : (↑(InnerProductGeometry.angle y (y - x)) : Real.Angle).sin * ‖y - x‖ = ‖x‖
rw₁ : Real.sin (InnerProductGeometry.angle y (y - x)) * ‖y - x‖ = ‖x‖
rw₂ rw₃ : ‖x‖ = ‖x‖
⊢ (o.oangle y (y - x)).sin * ‖y - x‖ = ‖x‖

Tactic:
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)]

Premises used: InnerProductGeometry.sin_angle_sub_mul_norm_of_inner_eq_zero, Orientation.oangle_eq_angle_of_sign_eq_one, Real.Angle.sin_coe, Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ((-o).oangle x (x - y)).sin * ‖x - y‖ = ‖y‖
⊢ (o.oangle (x - y) x).sin * ‖x - y‖ = ‖y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Premises used: neg_inj, Orientation.oangle_rev, Orientation.oangle_neg_orientation_eq_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle x (x - y)).sin * ‖x - y‖ = ‖y‖

Tactic:
(-o).sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two h

Premises used: Orientation.sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle x (x - y)).sin * ‖x - y‖ = ‖y‖

Tactic:
exact (-o).sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two h

Premises used: Orientation.sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle y (y - x)).sign = 1
rw : (↑(InnerProductGeometry.angle y (y - x)) : Real.Angle).tan * ‖y‖ = ‖x‖
rw₁ : Real.tan (InnerProductGeometry.angle y (y - x)) * ‖y‖ = ‖x‖
rw₂ rw₃ : ‖x‖ = ‖x‖
⊢ (o.oangle y (y - x)).tan * ‖y‖ = ‖x‖

Tactic:
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))]

Premises used: InnerProductGeometry.tan_angle_sub_mul_norm_of_inner_eq_zero, Orientation.oangle_eq_angle_of_sign_eq_one, Orientation.right_ne_zero_of_oangle_eq_pi_div_two, Or.inl, Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two, Real.Angle.tan_coe
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ((-o).oangle x (x - y)).tan * ‖x‖ = ‖y‖
⊢ (o.oangle (x - y) x).tan * ‖x‖ = ‖y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Premises used: neg_inj, Orientation.oangle_rev, Orientation.oangle_neg_orientation_eq_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle x (x - y)).tan * ‖x‖ = ‖y‖

Tactic:
(-o).tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two h

Premises used: Orientation.tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ((-o).oangle x (x - y)).tan * ‖x‖ = ‖y‖

Tactic:
exact (-o).tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two h

Premises used: Orientation.tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle y (y - x)).sign = 1
rw : ‖y‖ / (↑(InnerProductGeometry.angle y (y - x)) : Real.Angle).cos = ‖y - x‖
rw₁ : ‖y‖ / Real.cos (InnerProductGeometry.angle y (y - x)) = ‖y - x‖
rw₂ rw₃ : ‖y - x‖ = ‖y - x‖
⊢ ‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖

Tactic:
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))]

Premises used: InnerProductGeometry.norm_div_cos_angle_sub_of_inner_eq_zero, Orientation.oangle_eq_angle_of_sign_eq_one, Real.Angle.cos_coe, Orientation.right_ne_zero_of_oangle_eq_pi_div_two, Or.inl, Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ‖x‖ / ((-o).oangle x (x - y)).cos = ‖x - y‖
⊢ ‖x‖ / (o.oangle (x - y) x).cos = ‖x - y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Premises used: neg_inj, Orientation.oangle_rev, Orientation.oangle_neg_orientation_eq_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ‖x‖ / ((-o).oangle x (x - y)).cos = ‖x - y‖

Tactic:
(-o).norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two h

Premises used: Orientation.norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ‖x‖ / ((-o).oangle x (x - y)).cos = ‖x - y‖

Tactic:
exact (-o).norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two h

Premises used: Orientation.norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle y (y - x)).sign = 1
rw : ‖x‖ / (↑(InnerProductGeometry.angle y (y - x)) : Real.Angle).sin = ‖y - x‖
rw₁ : ‖x‖ / Real.sin (InnerProductGeometry.angle y (y - x)) = ‖y - x‖
rw₂ rw₃ : ‖y - x‖ = ‖y - x‖
⊢ ‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖

Tactic:
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))]

Premises used: Orientation.left_ne_zero_of_oangle_eq_pi_div_two, Orientation.oangle_eq_angle_of_sign_eq_one, InnerProductGeometry.norm_div_sin_angle_sub_of_inner_eq_zero, Real.Angle.sin_coe, Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two, Or.inr
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ‖y‖ / ((-o).oangle x (x - y)).sin = ‖x - y‖
⊢ ‖y‖ / (o.oangle (x - y) x).sin = ‖x - y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Premises used: neg_inj, Orientation.oangle_rev, Orientation.oangle_neg_orientation_eq_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ‖y‖ / ((-o).oangle x (x - y)).sin = ‖x - y‖

Tactic:
(-o).norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two h

Premises used: Orientation.norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ‖y‖ / ((-o).oangle x (x - y)).sin = ‖x - y‖

Tactic:
exact (-o).norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two h

Premises used: Orientation.norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
hs : (o.oangle y (y - x)).sign = 1
rw : ‖x‖ / (↑(InnerProductGeometry.angle y (y - x)) : Real.Angle).tan = ‖y‖
rw₁ : ‖x‖ / Real.tan (InnerProductGeometry.angle y (y - x)) = ‖y‖
rw₂ rw₃ : ‖y‖ = ‖y‖
⊢ ‖x‖ / (o.oangle y (y - x)).tan = ‖y‖

Tactic:
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))]

Premises used: Orientation.left_ne_zero_of_oangle_eq_pi_div_two, InnerProductGeometry.norm_div_tan_angle_sub_of_inner_eq_zero, Orientation.oangle_eq_angle_of_sign_eq_one, Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two, Or.inr, Real.Angle.tan_coe
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ‖y‖ / ((-o).oangle x (x - y)).tan = ‖x‖
⊢ ‖y‖ / (o.oangle (x - y) x).tan = ‖x‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Premises used: neg_inj, Orientation.oangle_rev, Orientation.oangle_neg_orientation_eq_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ‖y‖ / ((-o).oangle x (x - y)).tan = ‖x‖

Tactic:
(-o).norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two h

Premises used: Orientation.norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = (↑(π / 2) : Real.Angle)
⊢ ‖y‖ / ((-o).oangle x (x - y)).tan = ‖x‖

Tactic:
exact (-o).norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two h

Premises used: Orientation.norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
inl :
  ∀ (hr : r < 0),
    o.oangle x (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
      (↑(Real.arctan r) : Real.Angle)
inr :
  o.oangle x (x + HSMul.hSMul (α := ℝ) (β := V) 0 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(Real.arctan 0) : Real.Angle)
inr₁ :
  ∀ (hr : 0 < r),
    o.oangle x (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
      (↑(Real.arctan r) : Real.Angle)
⊢ o.oangle x (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(Real.arctan r) : Real.Angle)

Tactic:
rcases lt_trichotomy r 0 with (hr | rfl | hr)

Premises used: OfNat.ofNat, rfl, lt_trichotomy