From ce751dff8391e498cd3598d295bc132bd80a2519 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 12 Jun 2024 13:50:29 +0200
Subject: [PATCH] Update holomorphic.primitive.lean

---
 Nevanlinna/holomorphic.primitive.lean | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean
index 07b8d1d..4813e2c 100644
--- a/Nevanlinna/holomorphic.primitive.lean
+++ b/Nevanlinna/holomorphic.primitive.lean
@@ -161,15 +161,21 @@ theorem integral_divergence₅
   (∫ (x : ℝ) in a₁..b₁, Complex.I • F { re := x, im := a₂ }) +
   (∫ (y : ℝ) in a₂..b₂, F { re := a₁, im := y }) := by
 
-  let f := F
-  let h₁f : ContDiff ℝ 1 f := by sorry
+  let h₁f : ContDiff ℝ 1 F :=  (hF.contDiff : ContDiff ℂ 1 F).restrict_scalars ℝ
+
   let g := Complex.I • F
-  let h₁g : ContDiff ℝ 1 g := by sorry
+  let h₁g : ContDiff ℝ 1 (Complex.I • F) := by
+    have : Complex.I • F = fun x ↦ Complex.I • F x := by rfl
+    rw [this]
+    apply ContDiff.comp
+    exact contDiff_const_smul Complex.I
+    exact h₁f
 
-  let A := integral_divergence₄ f g h₁f h₁g a₁ a₂ b₁ b₂
 
-  have {z : ℂ} : fderiv ℝ f z 1 = partialDeriv ℝ 1 f z := by rfl
-  conv at A in (fderiv ℝ f _) 1 => rw [this]
+  let A := integral_divergence₄ F g h₁f h₁g a₁ a₂ b₁ b₂
+
+  have {z : ℂ} : fderiv ℝ F z 1 = partialDeriv ℝ 1 F z := by rfl
+  conv at A in (fderiv ℝ F _) 1 => rw [this]
   have {z : ℂ} : fderiv ℝ g z Complex.I = partialDeriv ℝ Complex.I g z := by rfl
   conv at A in (fderiv ℝ g _) Complex.I => rw [this]
 
@@ -186,4 +192,6 @@ theorem integral_divergence₅
     simp
   simp at A
 
+
+
   sorry