From 69a35228ee68487d43b50be32993ddcf6b86988e Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 8 May 2024 08:32:06 +0200
Subject: [PATCH] Update complexHarmonic.lean

---
 Nevanlinna/complexHarmonic.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index b38a823..568d2c6 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -46,9 +46,14 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
     unfold Complex.laplace
     rw [CauchyRiemann₄ h]
 
+    -- This lemma says that partial derivatives commute with complex scalar
+    -- multiplication. This is a consequence of partialDeriv_compContLin once we
+    -- note that complex scalar multiplication is continuous ℝ-linear.
     have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → ℂ, Differentiable ℝ g →  Real.partialDeriv v (s • g) = s • (Real.partialDeriv v g) := by
       intro v s g hg
 
+      -- Present scalar multiplication as a continuous ℝ-linear map. This is
+      -- horrible, there must be better ways to do that.
       let sMuls : ℂ →L[ℝ] ℂ :=
       {
         toFun := fun x ↦ s * x
@@ -61,8 +66,11 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
           ring
       }
 
+      -- Bring the goal into a form that is recognized by
+      -- partialDeriv_compContLin.
       have : s • g = sMuls ∘ g := by rfl
       rw [this]
+
       rw [partialDeriv_compContLin hg]
       rfl