English
For x ≠ 0 and r ∈ R, the angle o.oangle(x + r·rotation(π/2)x, r·rotation(π/2)x) equals arctan r⁻¹.
Русский
Для x ≠ 0 и r ∈ R угол o.oangle(x + r·rotation(π/2)x, r·rotation(π/2)x) равен arctan r⁻¹.
LaTeX
$$$ o.oangle\left(x + r\cdot rotation\left(\frac{\pi}{2}\right)x,\; r\cdot rotation\left(\frac{\pi}{2}\right)x\right) = \arctan r^{-1} $$$
Lean4
/-- An angle in a right-angled triangle expressed using `arctan`, where one side is a multiple
of a rotation of another by `π / 2`. -/
theorem oangle_add_left_smul_rotation_pi_div_two {x : V} (h : x ≠ 0) (r : ℝ) :
o.oangle (x + r • o.rotation (π / 2 : ℝ) x) (r • o.rotation (π / 2 : ℝ) x) = Real.arctan r⁻¹ :=
by
by_cases hr : r = 0; · simp [hr]
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj, ← neg_neg ((π / 2 : ℝ) : Real.Angle), ←
rotation_neg_orientation_eq_neg, add_comm]
have hx : x = r⁻¹ • (-o).rotation (π / 2 : ℝ) (r • (-o).rotation (-(π / 2 : ℝ)) x) := by simp [hr]
nth_rw 3 [hx]
refine (-o).oangle_add_right_smul_rotation_pi_div_two ?_ _
simp [hr, h]
