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)
⊢ 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)
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)
⊢ 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 (‖HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)‖ / ‖x‖)) :
      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 : 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)
⊢ 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‖ * norm (E := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) / ‖x‖)) : 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 : 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)
⊢ 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‖ * ‖x‖ / ‖x‖)) : 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 : 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)
⊢ 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‖ * (‖x‖ / ‖x‖))) : 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 : 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)
⊢ 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‖ * 1)) : 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 : 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)
⊢ 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 : 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)
⊢ 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 : 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)
⊢ 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 : 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)
⊢ 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 : 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)
⊢ 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]