CH2.Phi_circ.contDiff_real

theorem Phi_circ.contDiff_real (ν ε : ℝ) (hlam : ν ≠ 0) : ContDiff ℝ 2 (fun t : ℝ => Phi_circ ν ε (t : ℂ)) := by  have h_diff : ContDiff ℝ 2 (fun t : ℝ => 1 / Complex.tanh ((-2 * Real.pi * Complex.I * t + ν) / 2)) := by    simp only [Complex.tanh_eq_sinh_div_cosh]    have h_inner : ContDiff ℝ 2 (fun t : ℝ => (-2 * Real.pi * Complex.I * t + ν) / 2) := by fun_prop    have h_sinh_cosh_diff : ContDiff ℝ 2 (fun t : ℝ => Complex.sinh ((-2 * Real.pi * Complex.I * t + ν) / 2)) ∧ ContDiff ℝ 2 (fun t : ℝ => Complex.cosh ((-2 * Real.pi * Complex.I * t + ν) / 2)) ∧ ∀ t : ℝ, Complex.sinh ((-2 * Real.pi * Complex.I * t + ν) / 2) ≠ 0 := by      refine ⟨Complex.contDiff_sinh_real.comp h_inner, Complex.contDiff_cosh_real.comp h_inner, ?_⟩      · norm_num [Complex.sinh, Complex.exp_ne_zero]        norm_num [sub_eq_zero, Complex.exp_ne_zero]        intro t ht; rw [Complex.exp_eq_exp_iff_exists_int] at ht        obtain ⟨k, hk⟩ := ht; norm_num [Complex.ext_iff] at hk        rcases k with ⟨_ | k⟩ <;> norm_num at hk <;> ring_nf at hk <;> norm_num at hk <;>          cases lt_or_gt_of_ne hlam <;> nlinarith [Real.pi_pos]    simp_all only [ne_eq, neg_mul, division_def, mul_inv_rev, inv_inv, one_mul]    exact ContDiff.mul h_sinh_cosh_diff.2.1 (ContDiff.inv h_sinh_cosh_diff.1 fun t => h_sinh_cosh_diff.2.2 t)  exact ContDiff.mul contDiff_const (h_diff.add contDiff_const)