-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_sub_right_smul_rotation_pi_div_two {x : V} (h : x ≠ 0) (r : ℝ) :
    o.oangle (r • o.rotation (π / 2 : ℝ) x) (r • o.rotation (π / 2 : ℝ) x - x)
      = Real.arctan r⁻¹

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : -x = r⁻¹ • (o.rotation ↑(π / 2)) (r • (o.rotation ↑(π / 2)) x)
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)

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

Result:
case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : -x = r⁻¹ • (o.rotation ↑(π / 2)) (r • (o.rotation ↑(π / 2)) x)
⊢ r • (o.rotation ↑(π / 2)) x ≠ 0

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ -x = r⁻¹ • (o.rotation ↑(π / 2)) (r • (o.rotation ↑(π / 2)) x)

Tactic:
simp [hr, ← Real.Angle.coe_add]

Result:
no goals

Proof state:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)

Tactic:
simp [hr]

Result:
no goals

Proof state:
case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : -x = r⁻¹ • (o.rotation ↑(π / 2)) (r • (o.rotation ↑(π / 2)) x)
⊢ r • (o.rotation ↑(π / 2)) x ≠ 0

Tactic:
simpa [hr] using h

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)

Tactic:
by_cases hr : r = 0

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r = 0
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)

Tactic:
have hx : -x = r⁻¹ • o.rotation (π / 2 : ℝ) (r • o.rotation (π / 2 : ℝ) x) := by
  simp [hr, ← Real.Angle.coe_add]

Result:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : -x = r⁻¹ • (o.rotation ↑(π / 2)) (r • (o.rotation ↑(π / 2)) x)
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)