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 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‖
⊢ (o.oangle y (y - x)).sin * ‖y - x‖ = ‖x‖
have rw₂ : ‖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)]
-- 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 y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ (o.oangle (x - y) x).sin * ‖x - y‖ = ‖y‖
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ((-o).oangle x (x - y)).sin * ‖x - y‖ = ‖y‖
Tactic: rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
Cleared hypotheses: h
-- 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 y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ (o.oangle y (y - x)).tan * ‖y‖ = ‖x‖
have hs : (o.oangle y (y - x)).sign = 1
Tactic: have hs : (o.oangle y (y - x)).sign = 1 := by
    rw [oangle_sign_sub_right_swap, 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
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
⊢ (o.oangle y (y - x)).tan * ‖y‖ = ‖x‖
have rw : (↑(InnerProductGeometry.angle y (y - x)) : Real.Angle).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))]
-- 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 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‖
⊢ (o.oangle y (y - x)).tan * ‖y‖ = ‖x‖
have rw₁ : Real.tan (InnerProductGeometry.angle y (y - x)) * ‖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))]
-- 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 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‖
⊢ (o.oangle y (y - x)).tan * ‖y‖ = ‖x‖
have rw₂ : ‖x‖ = ‖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))]
-- 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 y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ (o.oangle (x - y) x).tan * ‖x‖ = ‖y‖
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ((-o).oangle x (x - y)).tan * ‖x‖ = ‖y‖
Tactic: rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
Cleared hypotheses: h
-- 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 y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ ‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖
have hs : (o.oangle y (y - x)).sign = 1
Tactic: have hs : (o.oangle y (y - x)).sign = 1 := by
    rw [oangle_sign_sub_right_swap, 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
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
⊢ ‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖
have rw : ‖y‖ / (↑(InnerProductGeometry.angle y (y - x)) : Real.Angle).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))]
-- 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 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‖
⊢ ‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖
have rw₁ : ‖y‖ / Real.cos (InnerProductGeometry.angle y (y - x)) = ‖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))]
-- 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 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‖
⊢ ‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖
have rw₂ : ‖y - x‖ = ‖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))]
-- 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 y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ ‖x‖ / (o.oangle (x - y) x).cos = ‖x - y‖
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ‖x‖ / ((-o).oangle x (x - y)).cos = ‖x - y‖
Tactic: rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
Cleared hypotheses: h
-- 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 y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ ‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖
have hs : (o.oangle y (y - x)).sign = 1
Tactic: have hs : (o.oangle y (y - x)).sign = 1 := by
    rw [oangle_sign_sub_right_swap, 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
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
⊢ ‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖
have rw : ‖x‖ / (↑(InnerProductGeometry.angle y (y - x)) : Real.Angle).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))]
-- 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 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‖
⊢ ‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖
have rw₁ : ‖x‖ / Real.sin (InnerProductGeometry.angle y (y - x)) = ‖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))]
-- 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 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‖
⊢ ‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖
have rw₂ : ‖y - x‖ = ‖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))]
-- 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 y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ ‖y‖ / (o.oangle (x - y) x).sin = ‖x - y‖
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ‖y‖ / ((-o).oangle x (x - y)).sin = ‖x - y‖
Tactic: rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
Cleared hypotheses: h
-- 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 y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ ‖x‖ / (o.oangle y (y - x)).tan = ‖y‖
have hs : (o.oangle y (y - x)).sign = 1
Tactic: have hs : (o.oangle y (y - x)).sign = 1 := by
    rw [oangle_sign_sub_right_swap, 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
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
⊢ ‖x‖ / (o.oangle y (y - x)).tan = ‖y‖
have rw : ‖x‖ / (↑(InnerProductGeometry.angle y (y - x)) : Real.Angle).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))]
-- 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 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‖
⊢ ‖x‖ / (o.oangle y (y - x)).tan = ‖y‖
have rw₁ : ‖x‖ / Real.tan (InnerProductGeometry.angle y (y - x)) = ‖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))]
-- 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 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‖
⊢ ‖x‖ / (o.oangle y (y - x)).tan = ‖y‖
have rw₂ : ‖y‖ = ‖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))]
-- 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 y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ ‖y‖ / (o.oangle (x - y) x).tan = ‖x‖
have rw : ∀ (h : (-o).oangle y x = (↑(π / 2) : Real.Angle)), ‖y‖ / ((-o).oangle x (x - y)).tan = ‖x‖
Tactic: rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
Cleared hypotheses: h
-- 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 (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(Real.arctan r) : Real.Angle)
have 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)
Tactic: rcases lt_trichotomy r 0 with (hr | rfl | hr)
-- 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 : ℝ
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)
⊢ o.oangle x (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(Real.arctan r) : Real.Angle)
have inr : o.oangle x (x + HSMul.hSMul (α := ℝ) (β := V) 0 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
  (↑(Real.arctan 0) : Real.Angle)
Tactic: rcases lt_trichotomy r 0 with (hr | rfl | hr)
Cleared hypotheses: r
-- 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 : ℝ
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)
⊢ o.oangle x (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(Real.arctan r) : Real.Angle)
have 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)
Tactic: rcases lt_trichotomy r 0 with (hr | rfl | hr)
-- 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
⊢ o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    -(↑(π / 2) : Real.Angle)
have rw : Ne (α := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) (0 : V)
Tactic: 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]
-- 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 (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(Real.arctan r) : Real.Angle)
have ha : o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
  -(↑(π / 2) : Real.Angle)
Tactic: 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
-- 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
ha :
  o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    -(↑(π / 2) : 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)
have ha₁ : (-o).oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
  (↑(π / 2) : Real.Angle)
Tactic: rw [← neg_inj, ← oangle_neg_orientation_eq_neg, neg_neg] at ha
Cleared hypotheses: ha
-- 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
ha :
  (-o).oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(π / 2) : 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)
have inl : -o.oangle x (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
  -(↑(Real.arctan r) : Real.Angle)
Tactic: 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]
-- 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
ha :
  (-o).oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(π / 2) : Real.Angle)
inl :
  -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)
have inl₁ : - -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 [← 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]
-- 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
ha :
  (-o).oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(π / 2) : Real.Angle)
inl :
  -o.oangle x (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    -(↑(Real.arctan r) : Real.Angle)
inl₁ :
  - -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 (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(Real.arctan r) : Real.Angle)
have inl₂ : -(-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 [← 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]
-- 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
ha :
  (-o).oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(π / 2) : Real.Angle)
inl :
  -o.oangle x (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    -(↑(Real.arctan r) : Real.Angle)
inl₁ :
  - -o.oangle (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) x =
    -(↑(Real.arctan r) : Real.Angle)
inl₂ :
  -(-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 (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(Real.arctan r) : Real.Angle)
have inl₃ : (-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 [← 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]