CH2.ϕ_c2_left

@[blueprint  "phi-c2-left"  (title := "$\\varphi$ is $C^2$ on [-1,0]")  (statement := /--  $\varphi$ is $C^2$ on $[-1,0]$.  -/)  (proof := /-- Since $\Phi^{\pm, \circ}_\nu(z)$ and $\Phi^{\pm, \circ}_\nu(z)$ have no poles on $\mathbb{R}$, they have no poles on some open neighborhood of $[-1,1]$. Hence they are $C^2$ on this interval.  Since $w(0) = \nu$, we see that $\Phi^{\pm, \ast}_\nu(0)=0$, giving the claim. -/)  (latexEnv := "lemma")]theorem ϕ_c2_left (ν ε : ℝ) (hlam : ν ≠ 0) : ContDiffOn ℝ 2 (ϕ_pm ν ε) (Set.Icc (-1) 0) := by  have h_diff_star : ContDiff ℝ 2 (fun t : ℝ => Phi_star ν ε (t : ℂ)) := Phi_star.contDiff_real ν ε hlam  have h_eq : ∀ t ∈ Set.Icc (-1 : ℝ) 0, ϕ_pm ν ε t = Phi_circ ν ε (t : ℂ) - (if t = 0 then 0 else Phi_star ν ε (t : ℂ)) := by    unfold ϕ_pm    intro t ht    split_ifs    · norm_num      grind    · rw [Real.sign_of_neg (lt_of_le_of_ne ht.2 ‹_›)]      norm_num [sub_eq_add_neg]    · grind    · grind  refine ContDiffOn.congr ?_ h_eq  apply_rules [ContDiffOn.sub, (Phi_circ.contDiff_real ν ε hlam).contDiffOn, h_diff_star.contDiffOn]  refine h_diff_star.contDiffOn.congr fun x hx => ?_  grind [Phi_star, neg_mul, ofReal_zero, mul_zero, neg_zero, zero_add,    sub_self, zero_div]