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 : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx :
  x =
    HSMul.hSMul (β := V) r⁻¹
      ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
          (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) :
        V)
neg :
  o.oangle (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) + x) x =
    (↑(Real.arctan r) : Real.Angle)
⊢ o.oangle (x - HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) x =
    (↑(Real.arctan r) : Real.Angle)

Tactic:
rw [sub_eq_add_neg, add_comm]

Premises used: sub_eq_add_neg, add_comm
-- 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 : ℝ
hr : ¬r = 0
hx :
  x =
    HSMul.hSMul (β := V) r⁻¹
      ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
          (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) :
        V)
neg :
  o.oangle (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) + x)
      (HSMul.hSMul (β := V) r⁻¹
        ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
            (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) :
          V)) =
    (↑(Real.arctan r) : Real.Angle)
⊢ o.oangle (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) + x) x =
    (↑(Real.arctan r) : Real.Angle)

Tactic:
nth_rw 3 [hx]
-- 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 : ℝ
hr : ¬r = 0
hx :
  x =
    HSMul.hSMul (β := V) r⁻¹
      ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
          (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) :
        V)
neg :
  o.oangle
      (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) +
        HSMul.hSMul (β := V) r⁻¹
          ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
              (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) :
            V))
      (HSMul.hSMul (β := V) r⁻¹
        ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
            (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) :
          V)) =
    (↑(Real.arctan r) : Real.Angle)
⊢ o.oangle (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) + x)
      (HSMul.hSMul (β := V) r⁻¹
        ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
            (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) :
          V)) =
    (↑(Real.arctan r) : Real.Angle)

Tactic:
nth_rw 2 [hx]
-- 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 : ℝ
hr : ¬r = 0
hx :
  x =
    HSMul.hSMul (β := V) r⁻¹
      ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
          (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) :
        V)
neg : -HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ≠ 0
⊢ o.oangle
      (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) +
        HSMul.hSMul (β := V) r⁻¹
          ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
              (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) :
            V))
      (HSMul.hSMul (β := V) r⁻¹
        ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
            (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) :
          V)) =
    (↑(Real.arctan r) : Real.Angle)

Tactic:
rw [o.oangle_add_left_smul_rotation_pi_div_two, inv_inv]

Premises used: Orientation.oangle_add_left_smul_rotation_pi_div_two, inv_inv
-- 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 : ℝ
hr : ¬r = 0
hx :
  x =
    HSMul.hSMul (β := V) r⁻¹
      ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
          (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) :
        V)
⊢ -HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ≠ 0

Tactic:
simpa [hr] using h
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
rw : (∡ p₁ p₂ p₃).sign = 1
rw₁ : (↑(π / 2) : Real.Angle).sign = 1
rw₂ rw₃ : Eq (α := SignType) 1 1
⊢ (∡ p₂ p₃ p₁).sign = 1

Tactic:
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Premises used: EuclideanGeometry.oangle_rotate_sign, Real.Angle.sign_coe_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ (∡ p₂ p₃ p₁).sign = 1

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : (↑(∠ p₂ p₃ p₁) : Real.Angle) = (↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
rw₁ rw₂ :
  (↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle) = (↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
⊢ ∡ p₂ p₃ p₁ = (↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)

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

Premises used: EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.angle_eq_arccos_of_angle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
rw : (∡ p₁ p₂ p₃).sign = 1
rw₁ : (↑(π / 2) : Real.Angle).sign = 1
rw₂ rw₃ : Eq (α := SignType) 1 1
⊢ (∡ p₃ p₁ p₂).sign = 1

Tactic:
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Premises used: EuclideanGeometry.oangle_rotate_sign, Real.Angle.sign_coe_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ (∡ p₃ p₁ p₂).sign = 1

Tactic:
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle) = (↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle) = (↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
rw₂ : (↑(Real.arccos (dist p₁ p₂ / dist p₃ p₁)) : Real.Angle) = (↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
rw₃ rw₄ :
  (↑(Real.arccos (dist p₁ p₂ / dist p₃ p₁)) : Real.Angle) = (↑(Real.arccos (dist p₁ p₂ / dist p₃ p₁)) : Real.Angle)
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)

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

Premises used: EuclideanGeometry.angle_comm, dist_comm, EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.angle_eq_arccos_of_angle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : (↑(∠ p₂ p₃ p₁) : Real.Angle) = (↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
rw₁ rw₂ :
  (↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle) = (↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
⊢ ∡ p₂ p₃ p₁ = (↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)

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

Premises used: EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.angle_eq_arcsin_of_angle_eq_pi_div_two, EuclideanGeometry.left_ne_of_oangle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one, Or.inl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle) = (↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle) = (↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
rw₂ : (↑(Real.arcsin (dist p₃ p₂ / dist p₃ p₁)) : Real.Angle) = (↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
rw₃ rw₄ :
  (↑(Real.arcsin (dist p₃ p₂ / dist p₃ p₁)) : Real.Angle) = (↑(Real.arcsin (dist p₃ p₂ / dist p₃ p₁)) : Real.Angle)
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)

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

Premises used: EuclideanGeometry.angle_comm, dist_comm, EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.angle_eq_arcsin_of_angle_eq_pi_div_two, EuclideanGeometry.left_ne_of_oangle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one, Or.inr
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : (↑(∠ p₂ p₃ p₁) : Real.Angle) = (↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂)) : Real.Angle)
rw₁ rw₂ :
  (↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂)) : Real.Angle) = (↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂)) : Real.Angle)
⊢ ∡ p₂ p₃ p₁ = (↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂)) : Real.Angle)

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

Premises used: EuclideanGeometry.angle_eq_arctan_of_angle_eq_pi_div_two, EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.right_ne_of_oangle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle) = (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle)
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle) = (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle)
rw₂ rw₃ :
  (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle) = (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle)
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂)) : Real.Angle)

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

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_eq_arctan_of_angle_eq_pi_div_two, EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.left_ne_of_oangle_eq_pi_div_two, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
pos : ∀ (hp₂ : p₂ = p₃), |(∡ p₂ p₃ p₁).toReal| < π / 2
neg : ∀ (hp₂ : ¬p₂ = p₃), |(∡ p₂ p₃ p₁).toReal| < π / 2
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2

Tactic:
by_cases hp₂ : p₂ = p₃
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : p₂ = p₃
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2

Tactic:
simp [hp₂, Real.pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : ¬p₂ = p₃
pos : ∀ (hp₁ : p₁ = p₃), |(∡ p₂ p₃ p₁).toReal| < π / 2
neg : ∀ (hp₁ : ¬p₁ = p₃), |(∡ p₂ p₃ p₁).toReal| < π / 2
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2

Tactic:
by_cases hp₁ : p₁ = p₃
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : ¬p₂ = p₃
hp₁ : p₁ = p₃
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2

Tactic:
simp [hp₁, Real.pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : ¬p₂ = p₃
hp₁ : ¬p₁ = p₃
neg : ∠ p₂ p₃ p₁ < π / 2
⊢ |(∡ p₂ p₃ p₁).toReal| < π / 2

Tactic:
rw [← angle_eq_abs_oangle_toReal hp₂ hp₁]

Premises used: EuclideanGeometry.angle_eq_abs_oangle_toReal
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : ¬p₂ = p₃
hp₁ : ¬p₁ = p₃
⊢ ∠ p₂ p₃ p₁ < π / 2

Tactic:
angle_lt_pi_div_two_of_angle_eq_pi_div_two h (Ne.symm hp₂)

Premises used: Ne.symm, EuclideanGeometry.angle_lt_pi_div_two_of_angle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
hp₂ : ¬p₂ = p₃
hp₁ : ¬p₁ = p₃
⊢ ∠ p₂ p₃ p₁ < π / 2

Tactic:
exact angle_lt_pi_div_two_of_angle_eq_pi_div_two h (Ne.symm hp₂)

Premises used: Ne.symm, EuclideanGeometry.angle_lt_pi_div_two_of_angle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁) = HSMul.hSMul (α := ℤ) 2 (∡ p₅ p₆ p₄)
h₁₂₃ : ∠ p₁ p₂ p₃ = π / 2
h₄₅₆ : ∠ p₄ p₅ p₆ = π / 2
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h : ∡ p₂ p₃ p₁ = ∡ p₅ p₆ p₄) (h₁₂₃ : ∠ p₁ p₂ p₃ = π / 2) (h₄₅₆ : ∠ p₄ p₅ p₆ = π / 2), ∡ p₂ p₃ p₁ = ∡ p₅ p₆ p₄
⊢ ∡ p₂ p₃ p₁ = ∡ p₅ p₆ p₄

Tactic:
rwa [Real.Angle.two_zsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two
    (abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two h₁₂₃)
    (abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two h₄₅₆)] at h

Premises used: Real.Angle.two_zsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two, EuclideanGeometry.abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₆ p₅)
h₁₂₃ : ∠ p₁ p₂ p₃ = π / 2
h₄₅₆ : ∠ p₄ p₅ p₆ = π / 2
⊢ ∡ p₂ p₃ p₁ = ∡ p₄ p₆ p₅

Tactic:
(Real.Angle.two_zsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two
    (abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two h₁₂₃) ?_).1 h

Premises used: Real.Angle.two_zsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two, EuclideanGeometry.abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₆ p₅)
h₁₂₃ : ∠ p₁ p₂ p₃ = π / 2
h₄₅₆ : ∠ p₄ p₅ p₆ = π / 2
refine : |(∡ p₄ p₆ p₅).toReal| < π / 2
⊢ ∡ p₂ p₃ p₁ = ∡ p₄ p₆ p₅

Tactic:
refine (Real.Angle.two_zsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two
    (abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two h₁₂₃) ?_).1 h

Premises used: Real.Angle.two_zsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two, EuclideanGeometry.abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₆ p₅)
h₁₂₃ : ∠ p₁ p₂ p₃ = π / 2
h₄₅₆ : ∠ p₄ p₅ p₆ = π / 2
rw : |(∡ p₅ p₆ p₄).toReal| < π / 2
⊢ |(∡ p₄ p₆ p₅).toReal| < π / 2

Tactic:
rw [oangle_rev, Real.Angle.abs_toReal_neg]

Premises used: EuclideanGeometry.oangle_rev, Real.Angle.abs_toReal_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₆ p₅)
h₁₂₃ : ∠ p₁ p₂ p₃ = π / 2
h₄₅₆ : ∠ p₄ p₅ p₆ = π / 2
⊢ |(∡ p₅ p₆ p₄).toReal| < π / 2

Tactic:
abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two h₄₅₆

Premises used: EuclideanGeometry.abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₂ p₃ p₁) = HSMul.hSMul (α := ℤ) 2 (∡ p₄ p₆ p₅)
h₁₂₃ : ∠ p₁ p₂ p₃ = π / 2
h₄₅₆ : ∠ p₄ p₅ p₆ = π / 2
⊢ |(∡ p₅ p₆ p₄).toReal| < π / 2

Tactic:
exact abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two h₄₅₆

Premises used: EuclideanGeometry.abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : (↑(∠ p₂ p₃ p₁) : Real.Angle).cos = dist p₃ p₂ / dist p₁ p₃
rw₁ : Real.cos (∠ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃
rw₂ rw₃ : dist p₃ p₂ / dist p₁ p₃ = dist p₃ p₂ / dist p₁ p₃
⊢ (∡ p₂ p₃ p₁).cos = dist p₃ p₂ / dist p₁ p₃

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

Premises used: EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.cos_angle_of_angle_eq_pi_div_two, Real.Angle.cos_coe, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle).cos = dist p₁ p₂ / dist p₁ p₃
rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle).cos = dist p₁ p₂ / dist p₁ p₃
rw₂ : Real.cos (∠ p₂ p₁ p₃) = dist p₁ p₂ / dist p₁ p₃
rw₃ : dist p₁ p₂ / dist p₃ p₁ = dist p₁ p₂ / dist p₁ p₃
rw₄ rw₅ : dist p₁ p₂ / dist p₃ p₁ = dist p₁ p₂ / dist p₃ p₁
⊢ (∡ p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃

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

Premises used: EuclideanGeometry.angle_comm, dist_comm, EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two, EuclideanGeometry.cos_angle_of_angle_eq_pi_div_two, Real.Angle.cos_coe, EuclideanGeometry.oangle_eq_angle_of_sign_eq_one