awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
rw : Ne (α := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) (0 : V)
⊢ o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    -(↑(π / 2) : Real.Angle)

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]

Premises used: Orientation.oangle_neg_right, add_halves, sub_eq_zero, add_assoc, Real.Angle.coe_add, two_mul, add_comm, Orientation.oangle_smul_right_of_neg, Real.Angle.coe_two_pi, Orientation.oangle_rotation_self_right, sub_neg_eq_add
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ Ne (α := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) (0 : V)

Tactic:
simpa using h
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ 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
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
ha :
  o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    -(↑(π / 2) : Real.Angle)
⊢ (-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

Premises used: neg_neg, neg_inj, Orientation.oangle_neg_orientation_eq_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
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)
inl₁₅ 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)

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]

Premises used: Iff.mpr, norm_smul, LinearIsometryEquiv.norm_map, abs_of_neg, mul_div_assoc, Real.arctan_neg, neg_neg, norm_ne_zero_iff, Orientation.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two, neg_inj, Orientation.oangle_rev, mul_one, Orientation.oangle_neg_orientation_eq_neg, Neg.neg, div_self, Real.norm_eq_abs, Real.Angle.coe_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
⊢ o.oangle x (x + HSMul.hSMul (α := ℝ) (β := V) 0 ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(Real.arctan 0) : Real.Angle)

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 0 < r
rw : o.oangle x ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x) = (↑(π / 2) : Real.Angle)
rw₁ rw₂ : (↑(π / 2) : Real.Angle) = (↑(π / 2) : Real.Angle)
⊢ o.oangle x (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) =
    (↑(π / 2) : Real.Angle)

Tactic:
rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right h]

Premises used: Orientation.oangle_rotation_self_right, Orientation.oangle_smul_right_of_pos
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 0 < r
⊢ 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]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 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)
inr₇ 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)

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]

Premises used: Iff.mpr, norm_smul, LinearIsometryEquiv.norm_map, mul_div_assoc, norm_ne_zero_iff, Orientation.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two, abs_of_pos, mul_one, div_self, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
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)
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)
⊢ 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
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ 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:
simp [hr]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
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)
⊢ 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:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj, ←
    neg_neg ((π / 2 : ℝ) : Real.Angle), ← rotation_neg_orientation_eq_neg, add_comm]

Premises used: Real.pi, Real.Angle.coe, neg_neg, HDiv.hDiv, Orientation.rotation_neg_orientation_eq_neg, add_comm, neg_inj, Orientation.oangle_rev, OfNat.ofNat, Orientation.oangle_neg_orientation_eq_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ 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:
simp [hr]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ 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]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx :
  x =
    HSMul.hSMul (β := V) r⁻¹
      (((-o).rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
          (HSMul.hSMul (β := V) r (((-o).rotation (-(↑(π / 2) : Real.Angle)) : (a : V) → V) x : V)) :
        V)
neg :
  (-o).oangle (HSMul.hSMul (β := V) r (((-o).rotation (-(↑(π / 2) : Real.Angle)) : (a : V) → V) x : V))
      (HSMul.hSMul (β := V) r (((-o).rotation (-(↑(π / 2) : Real.Angle)) : (a : V) → V) 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)
⊢ (-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:
nth_rw 3 [hx]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx :
  x =
    HSMul.hSMul (β := V) r⁻¹
      (((-o).rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
          (HSMul.hSMul (β := V) r (((-o).rotation (-(↑(π / 2) : Real.Angle)) : (a : V) → V) x : V)) :
        V)
⊢ (-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:
(-o).oangle_add_right_smul_rotation_pi_div_two ?_ _

Premises used: Orientation.oangle_add_right_smul_rotation_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx :
  x =
    HSMul.hSMul (β := V) r⁻¹
      (((-o).rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
          (HSMul.hSMul (β := V) r (((-o).rotation (-(↑(π / 2) : Real.Angle)) : (a : V) → V) x : V)) :
        V)
neg : HSMul.hSMul (β := V) r (((-o).rotation (-(↑(π / 2) : Real.Angle)) : (a : V) → V) x : V) ≠ 0
⊢ (-o).oangle (HSMul.hSMul (β := V) r (((-o).rotation (-(↑(π / 2) : Real.Angle)) : (a : V) → V) x : V))
      (HSMul.hSMul (β := V) r (((-o).rotation (-(↑(π / 2) : Real.Angle)) : (a : V) → V) 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:
refine (-o).oangle_add_right_smul_rotation_pi_div_two ?_ _

Premises used: Orientation.oangle_add_right_smul_rotation_pi_div_two, Neg.neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx :
  x =
    HSMul.hSMul (β := V) r⁻¹
      (((-o).rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
          (HSMul.hSMul (β := V) r (((-o).rotation (-(↑(π / 2) : Real.Angle)) : (a : V) → V) x : V)) :
        V)
⊢ HSMul.hSMul (β := V) r (((-o).rotation (-(↑(π / 2) : Real.Angle)) : (a : V) → V) x : V) ≠ 0

Tactic:
simp [hr, h]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
rw : (↑(Real.arctan r) : Real.Angle).tan = r
rw₁ : Real.tan (Real.arctan r) = r
rw₂ rw₃ : r = r
⊢ (o.oangle x (x + HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V))).tan = r

Tactic:
rw [o.oangle_add_right_smul_rotation_pi_div_two h, Real.Angle.tan_coe, Real.tan_arctan]

Premises used: Orientation.oangle_add_right_smul_rotation_pi_div_two, Real.tan_arctan, Real.Angle.tan_coe
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
rw : (↑(Real.arctan r⁻¹) : Real.Angle).tan = r⁻¹
rw₁ : Real.tan (Real.arctan r⁻¹) = r⁻¹
rw₂ rw₃ : 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⁻¹

Tactic:
rw [o.oangle_add_left_smul_rotation_pi_div_two h, Real.Angle.tan_coe, Real.tan_arctan]

Premises used: Orientation.oangle_add_left_smul_rotation_pi_div_two, Real.tan_arctan, Real.Angle.tan_coe
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
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)
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)
⊢ 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
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ 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:
simp [hr]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ -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:
simp [hr, ← Real.Angle.coe_add]

Premises used: Real.Angle.coe_add
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ -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]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx :
  -x =
    HSMul.hSMul (β := V) r⁻¹
      ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
          (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) :
        V)
neg : HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ≠ 0
⊢ o.oangle (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V))
      (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) - x) =
    (↑(Real.arctan r⁻¹) : Real.Angle)

Tactic:
rw [sub_eq_add_neg, hx, o.oangle_add_right_smul_rotation_pi_div_two]

Premises used: sub_eq_add_neg, Orientation.oangle_add_right_smul_rotation_pi_div_two
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx :
  -x =
    HSMul.hSMul (β := V) r⁻¹
      ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V)
          (HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) :
        V)
⊢ HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) ≠ 0

Tactic:
simpa [hr] using h
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
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)
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)
⊢ 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
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ o.oangle (x - HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) x =
    (↑(Real.arctan r) : Real.Angle)

Tactic:
simp [hr]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ 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:
simp [hr, ← Real.Angle.coe_add]

Premises used: Real.Angle.coe_add
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ 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]