import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Complex.TaylorSeries
import Mathlib.Analysis.Calculus.LineDeriv.Basic
import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Nevanlinna.cauchyRiemann

noncomputable def Complex.laplace : (ℂ → ℂ) → (ℂ → ℂ) := by
  intro f

  let fx  := fun w ↦ fderiv ℝ f w 1
  let fxx := fun z ↦ fderiv ℝ fx z 1
  let fy  := fun w ↦ fderiv ℝ f w Complex.I
  let fyy := fun z ↦ fderiv ℝ fy z Complex.I
  exact fun z ↦ (fxx z) + (fyy z)


def Harmonic (f : ℂ → ℂ) : Prop :=
  (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)


theorem re_comp_holomorphic_is_harmonic (f : ℂ → ℂ) :
  Differentiable ℂ f → Harmonic f := by

  intro h

  constructor
  · -- Complex.reCLM ∘ f is two times real continuously differentiable
    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)

  · -- Laplace of f is zero
    intro z
    unfold Complex.laplace
    simp

    conv =>
      left
      right
      arg 1
      arg 2
      intro z
      rw [CauchyRiemann₁ (h z)]
    
    have t₀ : ∀ z, DifferentiableAt ℝ (fun w => (fderiv ℝ f w) 1) z := by
      intro z
      
      sorry

    have t₁ : ∀ x, (fderiv ℝ (fun w => Complex.I * (fderiv ℝ f w) 1) z) x
      = Complex.I * ((fderiv ℝ (fun w => (fderiv ℝ f w) 1) z) x) := by
      intro x
      rw [fderiv_const_mul]
      simp
      exact t₀ z
    rw [t₁]
    
    have t₂ : (fderiv ℝ (fun w => (fderiv ℝ f w) 1) z) Complex.I 
      = (fderiv ℝ (fun w => (fderiv ℝ f w) Complex.I) z) 1 := by
      sorry
    rw [t₂]

    conv =>
      left
      right
      arg 2
      arg 1
      arg 2
      intro z
      rw [CauchyRiemann₁ (h z)]
    
    rw [t₁]
    
    rw [← mul_assoc]
    simp