addition of sin and cos of the same angle

Stream: Is there code for X?

[Edison Xie]

import Mathlib

example (a b x : ℝ) (ha : 0 < a) (hb : 0 ≤ b) :
    a * Real.cos x + b * Real.sin x = Real.sqrt (a ^ 2 + b ^ 2) *
    Real.cos (x - Real.arctan (b / a)) := by
  simp only [Real.cos_sub, mul_comm (Real.cos x), mul_comm (Real.sin x), mul_add, ← mul_assoc]
  congr
  · simp only [Real.cos_arctan, one_div]
    rw [← mul_inv_eq_iff_eq_mul₀ (ne_of_gt <| inv_pos.2 <| Real.sqrt_pos_of_pos (by nlinarith)),
      inv_inv, ← sq_eq_sq₀ (mul_nonneg (le_of_lt ha) (Real.sqrt_nonneg _)) (Real.sqrt_nonneg _)]
    simp [mul_pow]
    rw [Real.sq_sqrt (by nlinarith), Real.sq_sqrt (by nlinarith)]
    simp [mul_add, div_pow, mul_div_cancel₀ (b := a ^ 2) _ (by nlinarith)]
  · simp only [div_eq_mul_inv, Real.sin_arctan, ← mul_assoc]
    rw [← mul_inv_eq_iff_eq_mul₀ (ne_of_gt <| inv_pos.2 <| Real.sqrt_pos_of_pos (by nlinarith)),
      ← mul_inv_eq_iff_eq_mul₀ (ne_of_gt <| inv_pos.2 ha), inv_inv, inv_inv, mul_comm, ← mul_assoc,
      ← sq_eq_sq₀ (mul_nonneg (by nlinarith) (Real.sqrt_nonneg _)) <|
        mul_nonneg (Real.sqrt_nonneg _) hb]
    simp only [mul_pow]
    rw [Real.sq_sqrt (by nlinarith), Real.sq_sqrt (by nlinarith)]
    simp only [inv_pow, mul_add, mul_one, ← mul_assoc, add_mul, add_right_inj]
    rw [mul_assoc (a^2), ← pow_add, mul_comm, ← mul_assoc, inv_mul_cancel₀ (by nlinarith), one_mul]

Do we have this in mathlib?

[Andrew Yang]

I can't find it but you don't need hb:

import Mathlib

open Real Complex

example (a b x : ℝ) (ha : 0 < a) :
    a * Real.cos x + b * Real.sin x = Real.sqrt (a ^ 2 + b ^ 2) *
    Real.cos (x - Real.arctan (b / a)) := by
  have h₁ : √(a ^ 2 + b ^ 2) = a * √(1 + (b / a) ^ 2) := by
    nth_rw 2 [← sqrt_sq ha.le]
    simp [← sqrt_mul, mul_add, sq_nonneg, ← mul_pow, ← mul_div_assoc, ha.ne']
  have h₂ : (a - I * b).arg = - Real.arctan (b / a) := by
    simp [arg, ha.le, arctan_eq_arcsin, norm_eq_sqrt_sq_add_sq, ← arcsin_neg, div_div, h₁, neg_div]
  trans ((a - Complex.I * b) * Complex.exp (↑x * Complex.I)).re
  · simp
  · rw [← (a - Complex.I * b).norm_mul_exp_arg_mul_I, mul_assoc, ← Complex.exp_add, ← add_mul, h₂]
    simp [add_comm, Complex.norm_eq_sqrt_sq_add_sq, ← Complex.exp_ofReal_mul_I_re, sub_eq_add_neg]

[Eric Wieser]

Do we have "arctan2"?

[Eric Wieser]

I guess you could use (a + b * I).arg instead

[Eric Wieser]

(the goal of this suggestion is to remove ha)

[Edison Xie]

should we PR this if this is not in mathlib?

[Jz Pan]

Informally, left hand side is just the real part of (a-b*I) * exp(I*x), correct?

[Kenny Lau]

certainly sounds very formal to me