From f2988797b4675ed38eabf1cb8412f8957302bc56 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 29 Jul 2024 11:22:47 +0200
Subject: [PATCH] Fix compilation

---
 Nevanlinna/diffOpGrothendieck.lean    |  9 +++++++++
 Nevanlinna/holomorphic.primitive.lean | 29 ++++++++++-----------------
 2 files changed, 20 insertions(+), 18 deletions(-)
 create mode 100644 Nevanlinna/diffOpGrothendieck.lean

diff --git a/Nevanlinna/diffOpGrothendieck.lean b/Nevanlinna/diffOpGrothendieck.lean
new file mode 100644
index 0000000..c76f80c
--- /dev/null
+++ b/Nevanlinna/diffOpGrothendieck.lean
@@ -0,0 +1,9 @@
+import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.InnerProductSpace.PiL2
+
+/-
+
+Here we would like to define differential operators, following EGA 4-1, §20.
+This is work to be done in the future.
+
+-/
\ No newline at end of file
diff --git a/Nevanlinna/holomorphic.primitive.lean b/Nevanlinna/holomorphic.primitive.lean
index c537d70..d7e3921 100644
--- a/Nevanlinna/holomorphic.primitive.lean
+++ b/Nevanlinna/holomorphic.primitive.lean
@@ -96,13 +96,13 @@ theorem CauchyRiemann₄
     simp
     rw [← mul_one Complex.I]
     rw [← smul_eq_mul]
-    rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f w) Complex.I 1]
   conv =>
     right
     right
     intro w
     rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)]
-
+  funext w
+  simp
 
 theorem MeasureTheory.integral2_divergence₃
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
@@ -200,12 +200,12 @@ theorem integral_divergence₅
     rw [this]
     apply ContDiff.comp
     exact contDiff_const_smul _
-    exact h₁f
+    exact h₁f  
 
   let A := integral_divergence₄ (-Complex.I • F) F h₁g h₁f lowerLeft.re upperRight.im upperRight.re lowerLeft.im
-  have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv _ F z := by rfl
+  have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv Complex.I F z := by rfl
   conv at A in (fderiv ℝ F _) _ => rw [this]
-  have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv _ (-Complex.I • F) z := by rfl
+  have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv 1 (-Complex.I • F) z := by rfl
   conv at A in (fderiv ℝ (-Complex.I • F) _) _ => rw [this]
   conv at A =>
     left
@@ -231,6 +231,7 @@ theorem integral_divergence₅
   exact B
 
 
+
 noncomputable def primitive
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] :
   ℂ  → (ℂ → E) → (ℂ → E) := by
@@ -291,26 +292,18 @@ theorem primitive_fderivAtBasepointZero
     fun_prop
   have t₂ {a b : ℝ} : IntervalIntegrable (fun x_1 => f { re := a, im := x_1 }) MeasureTheory.volume 0 b := by
     apply Continuous.intervalIntegrable
-    apply Continuous.comp
-    exact hf
-    have : ((fun x => { re := a, im := x }) : ℝ → ℂ) = (fun x => { re := a, im := 0 } + { re := 0, im := x }) := by
+    apply Continuous.comp hf
+    have : (Complex.mk a) = (fun x => Complex.I • Complex.ofRealCLM x + { re := a, im := 0 }) := by
       funext x
       apply Complex.ext
       rw [Complex.add_re]
       simp
-      rw [Complex.add_im]
       simp
     rw [this]
     apply Continuous.add
-    fun_prop
-    have : (fun x => { re := 0, im := x } : ℝ → ℂ) = Complex.I • Complex.ofRealCLM := by
-      funext x
-      simp
-      have : (x : ℂ) = {re := x, im := 0} := by rfl
-      rw [this]
-      rw [Complex.I_mul]
-      simp
     continuity
+    fun_prop
+    
 
   have t₃ {a : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 a := by
     apply Continuous.intervalIntegrable
@@ -557,7 +550,7 @@ lemma integrability₂
   apply Continuous.intervalIntegrable
   apply Continuous.comp
   exact Differentiable.continuous hf
-  have : ((fun x => { re := b, im := x }) : ℝ → ℂ) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by
+  have : (Complex.mk b) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by
     funext x
     apply Complex.ext
     rw [Complex.add_re]