import Mathlib.Data.Fin.Tuple.Basic
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 Real.partialDeriv : ℂ → (ℂ → ℂ) → (ℂ → ℂ) := by
  intro v
  intro f
  exact fun w ↦ (fderiv ℝ f w) v

theorem CauchyRiemann₄ {f : ℂ → ℂ} : (Differentiable ℂ f)
  → Real.partialDeriv Complex.I f = Complex.I • Real.partialDeriv 1 f := by
  intro h
  unfold Real.partialDeriv
  
  conv =>
    left
    intro w
    rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)]
    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)]

theorem partialDeriv_smul {f : ℂ → ℂ } {a v : ℂ } : Real.partialDeriv v (a • f) = a • Real.partialDeriv v f := by
  unfold Real.partialDeriv
  have : a • f = fun y ↦ a • f y := by rfl
  conv =>
    left
    intro w
    rw [this]
    rw [fderiv_const_smul]
    
  
  sorry

noncomputable def Complex.laplace : (ℂ → ℂ) → (ℂ → ℂ) := by
  intro f
  let fx  := Real.partialDeriv 1 f
  let fxx := Real.partialDeriv 1 fx
  let fy  := Real.partialDeriv Complex.I f 
  let fyy := Real.partialDeriv Complex.I fy
  exact fxx + fyy


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


lemma derivSymm (f : ℂ → ℂ) (hf : ContDiff ℝ 2 f) :
  ∀ z a b : ℂ, (fderiv ℝ (fun w => fderiv ℝ f w) z) a b = (fderiv ℝ (fun w => fderiv ℝ f w) z) b a := by
  intro z a b

  let f' := fderiv ℝ f
  have h₀ : ∀ y, HasFDerivAt f (f' y) y := by
    have h : Differentiable ℝ f := by
      exact (contDiff_succ_iff_fderiv.1 hf).left
    exact fun y => DifferentiableAt.hasFDerivAt (h y)

  let f'' := (fderiv ℝ f' z)
  have h₁ : HasFDerivAt f' f'' z := by
    apply DifferentiableAt.hasFDerivAt
    let A := (contDiff_succ_iff_fderiv.1 hf).right
    let B := (contDiff_succ_iff_fderiv.1 A).left
    simp at B
    exact B z

  let A := second_derivative_symmetric h₀ h₁ a b
  dsimp [f'', f'] at A
  apply A


lemma l₂ {f : ℂ → ℂ} (hf : ContDiff ℝ 2 f) (z a b : ℂ) :
    fderiv ℝ (fderiv ℝ f) z b a = fderiv ℝ (fun w ↦ fderiv ℝ f w a) z b := by
  rw [fderiv_clm_apply]
  · simp
  · exact (contDiff_succ_iff_fderiv.1 hf).2.differentiable le_rfl z
  · simp


theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
  Harmonic f := by

  -- f is real C²
  have f_is_real_C2 : ContDiff ℝ 2 f :=
    ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)

  -- f' is real C¹
  have f'_is_real_C1 : ContDiff ℝ 1 (fderiv ℝ f) :=
    (contDiff_succ_iff_fderiv.1 f_is_real_C2).right

  -- f' is real differentiable
  have f'_is_differentiable : Differentiable ℝ (fderiv ℝ f) :=
    (contDiff_succ_iff_fderiv.1 f'_is_real_C1).left

  -- Partial derivative in direction 1
  let f_1 := fun w ↦ (fderiv ℝ f w) 1

  -- Partial derivative in direction I
  let f_I := fun w ↦ (fderiv ℝ f w) Complex.I

  constructor
  · -- f is two times real continuously differentiable
    exact f_is_real_C2

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

    rw [CauchyRiemann₄ h]



    have t₁a : (fderiv ℝ (fun w ↦ Complex.I * (fderiv ℝ f w) 1) z) 
      = Complex.I • (fderiv ℝ f_1 z) := by
      rw [fderiv_const_mul]
      fun_prop

    rw [t₁a]

    have t₂ : (fderiv ℝ f_1 z) Complex.I = (fderiv ℝ f_I z) 1 := by
      let B := l₂ f_is_real_C2 z Complex.I 1
      rw [← B]
      let A := derivSymm f f_is_real_C2 z 1 Complex.I
      rw [A]
      let C := l₂ f_is_real_C2 z 1 Complex.I
      rw [C]
    simp
    rw [t₂]

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

    simp
    rw [← mul_assoc]
    simp