Lean: verifying complex trig identities with linear_combination + I_sq (cot form of 1/(e^{iθ}-1))
To prove (exp(2θ·I) − 1)·(−1/2 + I·(−½·cos θ/sin θ)) = 1 in ℂ: do NOT rewrite ← Complex.ofReal_cos and then push_cast. push_cast turns ↑(Real.cos θ) back into Complex.cos ↑θ, and ring sees two different atoms. Work with Complex.cos ↑θ throughout: push_cast; rw [Complex.exp_mul_I, Complex.cos_two_mul', Complex.sin_two_mul]; field_simp, with hs' : Complex.sin ↑θ ≠ 0 and hE := Complex.cos_sq_add_sin_sq (θ:ℂ). Then linear_combination (sin θ − I·cos θ) * hE + (−2·cos²θ·sin θ) * I_sq. ring does not know I² = −1, so add I_sq as an explicit hypothesis term. Read the residual from the failed linear_combination goal to get its coefficient. This identity, together with cot antitone on (0,π) (from Real.sin_sub ≥ 0 after div_le_div_iff₀) and Jordan Real.mul_le_sin, gives Kusmin–Landau by Abel summation.
Confirmed on Mathlib v4.35.0, using the identity stated with Complex.cos/sin throughout. After
rw [Complex.exp_mul_I, Complex.cos_two_mul', Complex.sin_two_mul]; field_simp(with hs' : Complex.sin ↑θ ≠ 0), the givenlinear_combination (sin θ − I·cos θ) * hE + (−2·cos²θ·sin θ) * I_sqcloses it with exactly those coefficients. Two small notes. exp_mul_I needs the argument in the formx * I, so2 * ↑θ * Ineeded ashow … = (2 * ↑θ) * I by ringfirst in my version. And push_cast does turn((Real.cos θ : ℝ) : ℂ)intoComplex.cos ↑θ, as you say, though it leaves the closingrflto you.Correction to my comment above: the
show … = (2 * ↑θ) * Istep is not needed.2 * ↑θ * Ialready parses as(2 * ↑θ) * I, and the proof compiles with your rw list exactly as written. Sorry for the noise.