Deriv Fmod GReal

theorem deriv_FmodGReal (t : ℝ) (ht : 0 < t) :    deriv FmodGReal t = (-2 * π) * (L₁₀ ⟨Complex.I * t, by simp [ht]⟩).re /      (G ⟨Complex.I * t, by simp [ht]⟩).re ^ 2 := by  set z : ℍ := ⟨Complex.I * t, by simp [ht]⟩ with hz_def  have hF_deriv := hasDerivAt_resToImagAxis_re F_holo ht  have hG_deriv := hasDerivAt_resToImagAxis_re G_holo ht  have hG_pos : 0 < (G z).re := by simpa [ResToImagAxis, ht] using G_imag_axis_pos.2 t ht  have hG_ne : (G.resToImagAxis t).re ≠ 0 := by    simpa [ResToImagAxis, ht, hz_def] using ne_of_gt hG_pos  have heq : FmodGReal =ᶠ[nhds t]      (fun s => (F.resToImagAxis s).re / (G.resToImagAxis s).re) := by    filter_upwards [lt_mem_nhds ht] with s hs    simp only [FmodGReal, FReal, GReal, Function.resToImagAxis_apply, ResToImagAxis,      hs, ↓reduceDIte]  rw [heq.deriv_eq]  have hdiv : deriv (fun s ↦ (F.resToImagAxis s).re / (G.resToImagAxis s).re) t =      (deriv (fun s ↦ (F.resToImagAxis s).re) t * (G.resToImagAxis t).re -        (F.resToImagAxis t).re * deriv (fun s ↦ (G.resToImagAxis s).re) t) /          (G.resToImagAxis t).re ^ 2 :=    deriv_div hF_deriv.differentiableAt hG_deriv.differentiableAt hG_ne  rw [hdiv, hF_deriv.deriv, hG_deriv.deriv]  simp only [Function.resToImagAxis_apply, ResToImagAxis, ht, ↓reduceDIte, hz_def]  have hF_real := F_imag_axis_real t ht  have hG_real := G_imag_axis_real t ht  simp only [Function.resToImagAxis_apply, ResToImagAxis, ht, ↓reduceDIte] at hF_real hG_real  have hL₁₀ := L₁₀_eq_FD_G_sub_F_DG z  simp only [hz_def] at hL₁₀ hF_real hG_real  rw [hL₁₀]  simp only [mul_re, sub_re, hF_real, hG_real, mul_zero, sub_zero, zero_mul]  ring