CH2.lemma_5_1_d

@[blueprint  "ch2-lemma-5-1-d"  (title := "$G^\\star$ reflection (CH2 Lemma 5.1, eq. 4)")  (statement := /--  Since $C_{n,1}^-$ is the conjugate of $C_{n,1}^+$ traversed backwards and $G^\star(\bar s) =  -\overline{G^\star(s)}$, the two $G^\star$ contour integrals combine into a single imaginary part:  $$ \int_{C_{n,1}^+} G^\star(s) x^s\, ds - \int_{C_{n,1}^-} G^\star(s) x^s\, ds = 2i\, \Im \int_{C_{n,1}^+} G^\star(s) x^s\, ds. $$ -/)  (proof := /-- For the conjugation-antisymmetric integrand $G^\star x^s$, $\int_{C_{n,1}^-} = \overline{\int_{C_{n,1}^+}}$, and $z - \bar z = 2i\, \Im z$. -/)  (latexEnv := "sublemma")  (discussion := 1451)]theorem lemma_5_1_d (n : ℕ) (hG_star_symm : ConjAntisymm G_star)    (hx₀ : 1 ≤ x₀) (hx : x₀ < x) :    l.intCn1Plus n (fun s ↦ G_star s * (x : ℂ) ^ s) -        l.intCn1Minus n (fun s ↦ G_star s * (x : ℂ) ^ s) =      2 * Complex.I * ((l.intCn1Plus n (fun s ↦ G_star s * (x : ℂ) ^ s)).im : ℂ) := by  have hF : ∀ s, starRingEnd ℂ (G_star s * (x : ℂ) ^ s) = - (G_star (starRingEnd ℂ s) * (x : ℂ) ^ (starRingEnd ℂ s)) := by    intro s    rw [map_mul]    have h_x_symm : starRingEnd ℂ ((x:ℂ)^s) = (x:ℂ)^(starRingEnd ℂ s) := by      have hx_pos : 0 ≤ x := by linarith [hx₀, hx]      have harg : (x : ℂ).arg ≠ Real.pi := by        rw [Complex.arg_ofReal_of_nonneg hx_pos]        exact Real.pi_ne_zero.symm      have h1 := Complex.cpow_conj (x : ℂ) s harg      rw [h1, conj_ofReal]    rw [h_x_symm]    have hG_symm := hG_star_symm s    rw [hG_symm]    ring  have h_plus_minus : starRingEnd ℂ (l.intCn1Plus n (fun s ↦ G_star s * (x : ℂ) ^ s)) = l.intCn1Minus n (fun s ↦ G_star s * (x : ℂ) ^ s) := by    unfold LadderParams.intCn1Plus LadderParams.intCn1Minus    rw [map_add, map_add]    have h1 := conj_intHSeg_of_antisymm l.δ 1 (l.σ n) (fun s ↦ G_star s * (x : ℂ) ^ s) hF    have h2 := conj_intVSeg_of_antisymm 1 0 l.δ (fun s ↦ G_star s * (x : ℂ) ^ s) hF    have h3 := conj_intVSeg_of_antisymm (l.σ n) l.δ l.T (fun s ↦ G_star s * (x : ℂ) ^ s) hF    rw [h1, h2, h3]    ring_nf  have h_sub : l.intCn1Plus n (fun s ↦ G_star s * (x : ℂ) ^ s) - l.intCn1Minus n (fun s ↦ G_star s * (x : ℂ) ^ s) =      l.intCn1Plus n (fun s ↦ G_star s * (x : ℂ) ^ s) - starRingEnd ℂ (l.intCn1Plus n (fun s ↦ G_star s * (x : ℂ) ^ s)) := by    rw [h_plus_minus]  rw [h_sub, Complex.sub_conj]  simp; ring_nf