lower_secant_bound'

lemma lower_secant_bound' {η : ℝ} {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_le : |x| ≤ 2 * π - η) :    (2 / π) * η ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by  by_cases! ηpos : η ≤ 0  · calc (2 / π) * η    _ ≤ 0 := mul_nonpos_of_nonneg_of_nonpos (div_nonneg zero_le_two pi_pos.le) ηpos    _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := norm_nonneg _  wlog x_nonneg : 0 ≤ x generalizing x  · convert (@this (-x) _ (by simpa) (by linarith)) using 1    · rw [← Complex.norm_conj, map_sub, map_one, Complex.ofReal_neg, mul_neg,        ← Complex.exp_conj, map_mul, Complex.conj_I, neg_mul,        Complex.conj_ofReal]    · rwa [abs_neg]  rw [abs_of_nonneg x_nonneg] at *  wlog x_le_pi : x ≤ π generalizing x  · convert (@this (2 * π - x) ..) using 1    · rw [← Complex.norm_conj]      simp [← Complex.exp_conj, mul_sub, Complex.conj_ofReal, Complex.exp_sub,        mul_comm Complex.I (2 * π), ← Complex.exp_neg]    all_goals linarith  by_cases! h : x ≤ π / 2  · calc (2 / π) * η    _ ≤ (2 / π) * x := by gcongr    _ = (1 - (2 / π) * x) * sin 0 + ((2 / π) * x) * sin (π / 2) := by simp    _ ≤ sin ((1 - (2 / π) * x) * 0 + ((2 / π) * x) * (π / 2)) := by      apply (strictConcaveOn_sin_Icc.concaveOn).2 (by simp [pi_nonneg])      · simp only [Set.mem_Icc, half_le_self_iff]        constructor <;> linarith [pi_nonneg]      · rw [sub_nonneg, mul_comm]        exact mul_le_of_le_div₀ (by norm_num) (div_nonneg (by norm_num) pi_nonneg) (by simpa)      · exact mul_nonneg (div_nonneg (by norm_num) pi_nonneg) x_nonneg      · simp    _ = sin x := by simp; field_simp    _ ≤ sqrt ((sin x) ^ 2) := by      rw [sqrt_sq_eq_abs]      apply le_abs_self    _ ≤ ‖1 - Complex.exp (Complex.I * ↑x)‖ := by        rw [mul_comm, Complex.exp_mul_I, Complex.norm_eq_sqrt_sq_add_sq]        simp only [Complex.sub_re, Complex.one_re, Complex.add_re, Complex.cos_ofReal_re,          Complex.mul_re, Complex.sin_ofReal_re, Complex.I_re, Complex.sin_ofReal_im, Complex.I_im,          Complex.sub_im, Complex.one_im, Complex.add_im, Complex.cos_ofReal_im, Complex.mul_im]        apply (sqrt_le_sqrt_iff _).mpr        · simp [pow_two_nonneg]        · linarith [pow_two_nonneg (1 - cos x), pow_two_nonneg (sin x)]  · exact lower_secant_bound_aux ηpos le_abs_x abs_x_le x_le_pi h