awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
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 : ℝ
⊢ 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) x : V) - x) =
    (↑(Real.arctan r⁻¹) : Real.Angle)
have pos : ∀ (hr : r = 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) x : V) - x) =
    (↑(Real.arctan r⁻¹) : Real.Angle)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
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 : ℝ
pos :
  ∀ (hr : r = 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) x : V) - x) =
      (↑(Real.arctan r⁻¹) : Real.Angle)
⊢ 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) x : V) - x) =
    (↑(Real.arctan r⁻¹) : Real.Angle)
have neg : ∀ (hr : ¬r = 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) x : V) - x) =
    (↑(Real.arctan r⁻¹) : Real.Angle)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (hypothesis)
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
⊢ 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) x : V) - x) =
    (↑(Real.arctan r⁻¹) : Real.Angle)
have 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)
Tactic: have hx : -x = r⁻¹ • o.rotation (π / 2 : ℝ) (r • o.rotation (π / 2 : ℝ) x) := by
    simp [hr, ← Real.Angle.coe_add]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
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)
⊢ 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) x : V) - x) =
    (↑(Real.arctan r⁻¹) : Real.Angle)
have neg : HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ≠ 0
Tactic: rw [sub_eq_add_neg, hx, o.oangle_add_right_smul_rotation_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
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 : ℝ
⊢ o.oangle (x - HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) x =
    (↑(Real.arctan r) : Real.Angle)
have pos : ∀ (hr : r = 0),
  o.oangle (x - HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) x =
    (↑(Real.arctan r) : Real.Angle)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
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 : ℝ
pos :
  ∀ (hr : r = 0),
    o.oangle (x - HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) 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)
have neg : ∀ (hr : ¬r = 0),
  o.oangle (x - HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) x =
    (↑(Real.arctan r) : Real.Angle)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (hypothesis)
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
⊢ o.oangle (x - HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) x =
    (↑(Real.arctan r) : Real.Angle)
have 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)
Tactic: have hx : x = r⁻¹ • o.rotation (π / 2 : ℝ) (-(r • o.rotation (π / 2 : ℝ) x)) := by
    simp [hr, ← Real.Angle.coe_add]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
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)
⊢ o.oangle (x - HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) x =
    (↑(Real.arctan r) : Real.Angle)
have neg : o.oangle (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) + x) x =
  (↑(Real.arctan r) : Real.Angle)
Tactic: rw [sub_eq_add_neg, add_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
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)
⊢ o.oangle (-HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) + x) x =
    (↑(Real.arctan r) : Real.Angle)
have 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)
Tactic: nth_rw 3 [hx]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
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)
⊢ 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)
have 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)
Tactic: nth_rw 2 [hx]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
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)
⊢ 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)
have neg : -HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ≠ 0
Tactic: rw [o.oangle_add_left_smul_rotation_pi_div_two, inv_inv]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ (∡ p₂ p₃ p₁).sign = 1
have rw : (∡ p₁ p₂ p₃).sign = 1
Tactic: rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
rw : (∡ p₁ p₂ p₃).sign = 1
⊢ (∡ p₂ p₃ p₁).sign = 1
have rw₁ : (↑(π / 2) : Real.Angle).sign = 1
Tactic: rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
rw : (∡ p₁ p₂ p₃).sign = 1
rw₁ : (↑(π / 2) : Real.Angle).sign = 1
⊢ (∡ p₂ p₃ p₁).sign = 1
have rw₂ : Eq (α := SignType) 1 1
Tactic: rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ ∡ p₂ p₃ p₁ = (↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
have hs : (∡ p₂ p₃ p₁).sign = 1
Tactic: have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ ∡ p₂ p₃ p₁ = (↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
have rw : (↑(∠ p₂ p₃ p₁) : Real.Angle) = (↑(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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : (↑(∠ p₂ p₃ p₁) : Real.Angle) = (↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
⊢ ∡ p₂ p₃ p₁ = (↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
have rw₁ : (↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle) = (↑(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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ (∡ p₃ p₁ p₂).sign = 1
have rw : (∡ p₁ p₂ p₃).sign = 1
Tactic: rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
rw : (∡ p₁ p₂ p₃).sign = 1
⊢ (∡ p₃ p₁ p₂).sign = 1
have rw₁ : (↑(π / 2) : Real.Angle).sign = 1
Tactic: rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
rw : (∡ p₁ p₂ p₃).sign = 1
rw₁ : (↑(π / 2) : Real.Angle).sign = 1
⊢ (∡ p₃ p₁ p₂).sign = 1
have rw₂ : Eq (α := SignType) 1 1
Tactic: rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
have hs : (∡ p₃ p₁ p₂).sign = 1
Tactic: have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
have rw : (↑(∠ p₃ p₁ p₂) : Real.Angle) = (↑(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₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle) = (↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
have rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle) = (↑(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₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle) = (↑(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)
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
have rw₂ : (↑(Real.arccos (dist p₁ p₂ / dist p₃ p₁)) : Real.Angle) = (↑(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₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle) = (↑(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)
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
have rw₃ : (↑(Real.arccos (dist p₁ p₂ / dist p₃ p₁)) : Real.Angle) = (↑(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₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ ∡ p₂ p₃ p₁ = (↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
have hs : (∡ p₂ p₃ p₁).sign = 1
Tactic: have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ ∡ p₂ p₃ p₁ = (↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
have rw : (↑(∠ p₂ p₃ p₁) : Real.Angle) = (↑(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))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₂ p₃ p₁).sign = 1
rw : (↑(∠ p₂ p₃ p₁) : Real.Angle) = (↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
⊢ ∡ p₂ p₃ p₁ = (↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle)
have rw₁ : (↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃)) : Real.Angle) = (↑(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))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
have hs : (∡ p₃ p₁ p₂).sign = 1
Tactic: have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
have rw : (↑(∠ p₃ p₁ p₂) : Real.Angle) = (↑(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₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle) = (↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
have rw₁ : (↑(∠ p₂ p₁ p₃) : Real.Angle) = (↑(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₃]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = (↑(π / 2) : Real.Angle)
hs : (∡ p₃ p₁ p₂).sign = 1
rw : (↑(∠ p₃ p₁ p₂) : Real.Angle) = (↑(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)
⊢ ∡ p₃ p₁ p₂ = (↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃)) : Real.Angle)
have rw₂ : (↑(Real.arcsin (dist p₃ p₂ / dist p₃ p₁)) : Real.Angle) = (↑(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₃]