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 : ℝ
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)
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 (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(Real.arctan r) : Real.Angle)
inl₅ :
  -(↑(Real.arctan (‖HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)‖ / ‖x‖)) :
        Real.Angle) =
    (↑(Real.arctan r) : Real.Angle)
inl₆ :
  -(↑(Real.arctan (‖r‖ * norm (E := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) / ‖x‖)) :
        Real.Angle) =
    (↑(Real.arctan r) : Real.Angle)
inl₇ : -(↑(Real.arctan (‖r‖ * ‖x‖ / ‖x‖)) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inl₈ : -(↑(Real.arctan (‖r‖ * (‖x‖ / ‖x‖))) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inl₉ : -(↑(Real.arctan (‖r‖ * 1)) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inl₁₀ : -(↑(Real.arctan ‖r‖) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inl₁₁ : -(↑(Real.arctan |r|) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inl₁₂ : -(↑(Real.arctan (-r)) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inl₁₃ : -(↑(-Real.arctan r) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inl₁₄ : - -(↑(Real.arctan r) : Real.Angle) = (↑(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₁₅ : (↑(Real.arctan r) : Real.Angle) = (↑(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 : 0 < r
⊢ o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(π / 2) : Real.Angle)
have rw : o.oangle x ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x) = (↑(π / 2) : Real.Angle)
Tactic: rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right 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 : ℝ
hr : 0 < r
rw : o.oangle x ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x) = (↑(π / 2) : Real.Angle)
⊢ o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(π / 2) : Real.Angle)
have rw₁ : (↑(π / 2) : Real.Angle) = (↑(π / 2) : Real.Angle)
Tactic: rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right 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 : 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 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_pos _ _ hr, o.oangle_rotation_self_right 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 : ℝ
hr : 0 < r
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 inr : (↑(Real.arctan (‖HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)‖ / ‖x‖)) :
    Real.Angle) =
  (↑(Real.arctan r) : Real.Angle)
Tactic: rw [o.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two ha, norm_smul,
      LinearIsometryEquiv.norm_map, mul_div_assoc, div_self (norm_ne_zero_iff.2 h), mul_one,
      Real.norm_eq_abs, abs_of_pos hr]
-- 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 : 0 < r
ha :
  o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(π / 2) : Real.Angle)
inr :
  (↑(Real.arctan (‖HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)‖ / ‖x‖)) :
      Real.Angle) =
    (↑(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₁ : (↑(Real.arctan (‖r‖ * norm (E := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) / ‖x‖)) : Real.Angle) =
  (↑(Real.arctan r) : Real.Angle)
Tactic: rw [o.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two ha, norm_smul,
      LinearIsometryEquiv.norm_map, mul_div_assoc, div_self (norm_ne_zero_iff.2 h), mul_one,
      Real.norm_eq_abs, abs_of_pos hr]
-- 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 : 0 < r
ha :
  o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(π / 2) : Real.Angle)
inr :
  (↑(Real.arctan (‖HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)‖ / ‖x‖)) :
      Real.Angle) =
    (↑(Real.arctan r) : Real.Angle)
inr₁ :
  (↑(Real.arctan (‖r‖ * norm (E := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) / ‖x‖)) : Real.Angle) =
    (↑(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₂ : (↑(Real.arctan (‖r‖ * ‖x‖ / ‖x‖)) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
Tactic: rw [o.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two ha, norm_smul,
      LinearIsometryEquiv.norm_map, mul_div_assoc, div_self (norm_ne_zero_iff.2 h), mul_one,
      Real.norm_eq_abs, abs_of_pos hr]
-- 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 : 0 < r
ha :
  o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(π / 2) : Real.Angle)
inr :
  (↑(Real.arctan (‖HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)‖ / ‖x‖)) :
      Real.Angle) =
    (↑(Real.arctan r) : Real.Angle)
inr₁ :
  (↑(Real.arctan (‖r‖ * norm (E := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) / ‖x‖)) : Real.Angle) =
    (↑(Real.arctan r) : Real.Angle)
inr₂ : (↑(Real.arctan (‖r‖ * ‖x‖ / ‖x‖)) : Real.Angle) = (↑(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₃ : (↑(Real.arctan (‖r‖ * (‖x‖ / ‖x‖))) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
Tactic: rw [o.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two ha, norm_smul,
      LinearIsometryEquiv.norm_map, mul_div_assoc, div_self (norm_ne_zero_iff.2 h), mul_one,
      Real.norm_eq_abs, abs_of_pos hr]
-- 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 : 0 < r
ha :
  o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(π / 2) : Real.Angle)
inr :
  (↑(Real.arctan (‖HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)‖ / ‖x‖)) :
      Real.Angle) =
    (↑(Real.arctan r) : Real.Angle)
inr₁ :
  (↑(Real.arctan (‖r‖ * norm (E := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) / ‖x‖)) : Real.Angle) =
    (↑(Real.arctan r) : Real.Angle)
inr₂ : (↑(Real.arctan (‖r‖ * ‖x‖ / ‖x‖)) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inr₃ : (↑(Real.arctan (‖r‖ * (‖x‖ / ‖x‖))) : Real.Angle) = (↑(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₄ : (↑(Real.arctan (‖r‖ * 1)) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
Tactic: rw [o.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two ha, norm_smul,
      LinearIsometryEquiv.norm_map, mul_div_assoc, div_self (norm_ne_zero_iff.2 h), mul_one,
      Real.norm_eq_abs, abs_of_pos hr]
-- 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 : 0 < r
ha :
  o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(π / 2) : Real.Angle)
inr :
  (↑(Real.arctan (‖HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)‖ / ‖x‖)) :
      Real.Angle) =
    (↑(Real.arctan r) : Real.Angle)
inr₁ :
  (↑(Real.arctan (‖r‖ * norm (E := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) / ‖x‖)) : Real.Angle) =
    (↑(Real.arctan r) : Real.Angle)
inr₂ : (↑(Real.arctan (‖r‖ * ‖x‖ / ‖x‖)) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inr₃ : (↑(Real.arctan (‖r‖ * (‖x‖ / ‖x‖))) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inr₄ : (↑(Real.arctan (‖r‖ * 1)) : Real.Angle) = (↑(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₅ : (↑(Real.arctan ‖r‖) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
Tactic: rw [o.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two ha, norm_smul,
      LinearIsometryEquiv.norm_map, mul_div_assoc, div_self (norm_ne_zero_iff.2 h), mul_one,
      Real.norm_eq_abs, abs_of_pos hr]
-- 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 : 0 < r
ha :
  o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(π / 2) : Real.Angle)
inr :
  (↑(Real.arctan (‖HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)‖ / ‖x‖)) :
      Real.Angle) =
    (↑(Real.arctan r) : Real.Angle)
inr₁ :
  (↑(Real.arctan (‖r‖ * norm (E := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) / ‖x‖)) : Real.Angle) =
    (↑(Real.arctan r) : Real.Angle)
inr₂ : (↑(Real.arctan (‖r‖ * ‖x‖ / ‖x‖)) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inr₃ : (↑(Real.arctan (‖r‖ * (‖x‖ / ‖x‖))) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inr₄ : (↑(Real.arctan (‖r‖ * 1)) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inr₅ : (↑(Real.arctan ‖r‖) : Real.Angle) = (↑(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₆ : (↑(Real.arctan |r|) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
Tactic: rw [o.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two ha, norm_smul,
      LinearIsometryEquiv.norm_map, mul_div_assoc, div_self (norm_ne_zero_iff.2 h), mul_one,
      Real.norm_eq_abs, abs_of_pos hr]
-- 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 : 0 < r
ha :
  o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(π / 2) : Real.Angle)
inr :
  (↑(Real.arctan (‖HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)‖ / ‖x‖)) :
      Real.Angle) =
    (↑(Real.arctan r) : Real.Angle)
inr₁ :
  (↑(Real.arctan (‖r‖ * norm (E := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) / ‖x‖)) : Real.Angle) =
    (↑(Real.arctan r) : Real.Angle)
inr₂ : (↑(Real.arctan (‖r‖ * ‖x‖ / ‖x‖)) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inr₃ : (↑(Real.arctan (‖r‖ * (‖x‖ / ‖x‖))) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inr₄ : (↑(Real.arctan (‖r‖ * 1)) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inr₅ : (↑(Real.arctan ‖r‖) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
inr₆ : (↑(Real.arctan |r|) : Real.Angle) = (↑(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₇ : (↑(Real.arctan r) : Real.Angle) = (↑(Real.arctan r) : Real.Angle)
Tactic: rw [o.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two ha, norm_smul,
      LinearIsometryEquiv.norm_map, mul_div_assoc, div_self (norm_ne_zero_iff.2 h), mul_one,
      Real.norm_eq_abs, abs_of_pos hr]
-- 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))
      (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(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))
      (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(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))
        (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
      (↑(Real.arctan r⁻¹) : Real.Angle)
⊢ o.oangle (x + 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)) =
    (↑(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))
      (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(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 : ℝ
hr : ¬r = 0
⊢ o.oangle (x + 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)) =
    (↑(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) x : V) + x) =
  (↑(Real.arctan r⁻¹) : Real.Angle)
Tactic: rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj, ←
    neg_neg ((π / 2 : ℝ) : Real.Angle), ← rotation_neg_orientation_eq_neg, add_comm]
-- 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]
-- 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 : (-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) +
      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))
      (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)) =
    (↑(Real.arctan r⁻¹) : Real.Angle)
have neg : HSMul.hSMul (β := V) r (((-o).rotation (-(↑(π / 2) : Real.Angle)) : (a : V) → V) x : V) ≠ 0
Tactic: refine (-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 (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V))).tan = r
have rw : (↑(Real.arctan r) : Real.Angle).tan = r
Tactic: rw [o.oangle_add_right_smul_rotation_pi_div_two h, Real.Angle.tan_coe, Real.tan_arctan]
-- 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 : ℝ
rw : (↑(Real.arctan r) : Real.Angle).tan = r
⊢ (o.oangle x (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V))).tan = r
have rw₁ : Real.tan (Real.arctan r) = r
Tactic: rw [o.oangle_add_right_smul_rotation_pi_div_two h, Real.Angle.tan_coe, Real.tan_arctan]
-- 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 : ℝ
rw : (↑(Real.arctan r) : Real.Angle).tan = r
rw₁ : Real.tan (Real.arctan r) = r
⊢ (o.oangle x (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V))).tan = r
have rw₂ : r = r
Tactic: rw [o.oangle_add_right_smul_rotation_pi_div_two h, Real.Angle.tan_coe, Real.tan_arctan]
-- 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))
        (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V))).tan =
    r⁻¹
have rw : (↑(Real.arctan r⁻¹) : Real.Angle).tan = r⁻¹
Tactic: rw [o.oangle_add_left_smul_rotation_pi_div_two h, Real.Angle.tan_coe, Real.tan_arctan]
-- 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 : ℝ
rw : (↑(Real.arctan r⁻¹) : Real.Angle).tan = r⁻¹
⊢ (o.oangle (x + 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))).tan =
    r⁻¹
have rw₁ : Real.tan (Real.arctan r⁻¹) = r⁻¹
Tactic: rw [o.oangle_add_left_smul_rotation_pi_div_two h, Real.Angle.tan_coe, Real.tan_arctan]
-- 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 : ℝ
rw : (↑(Real.arctan r⁻¹) : Real.Angle).tan = r⁻¹
rw₁ : Real.tan (Real.arctan r⁻¹) = r⁻¹
⊢ (o.oangle (x + 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))).tan =
    r⁻¹
have rw₂ : r⁻¹ = r⁻¹
Tactic: rw [o.oangle_add_left_smul_rotation_pi_div_two h, Real.Angle.tan_coe, Real.tan_arctan]