nevanlinna/nevanlinna/cauchyRiemann.lean

import Mathlib.Analysis.Calculus.Conformal.NormedSpace
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.Analysis.Calculus.Deriv.Linear
import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.Calculus.FDeriv.Comp
import Mathlib.Analysis.Calculus.FDeriv.Linear
import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
import Mathlib.Analysis.Calculus.LineDeriv.Basic
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Complex.CauchyIntegral
import Mathlib.Analysis.Complex.Conformal
import Mathlib.Analysis.Complex.RealDeriv

variable {z : ℂ} {f : ℂ → ℂ}

theorem CauchyRiemann₁ : (DifferentiableAt ℂ f z)
  → (fderiv ℝ f z) Complex.I = Complex.I * (fderiv ℝ f z) 1 := by
  intro h
  let A := fderiv ℂ f z
  have t₁ : A (Complex.I • 1) = Complex.I • (A 1) := by
    exact ContinuousLinearMap.map_smul_of_tower A Complex.I 1
  let AR := (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))
  have t₂ : AR (Complex.I • 1) = Complex.I • (AR 1) := by
    exact t₁
  have t₂a : Complex.I * (AR 1) = Complex.I • (AR 1) := by
    exact rfl
  rw [← t₂a] at t₂
  have t₂b : Complex.I • 1 = Complex.I := by
    simp
  have t₂c : AR Complex.I = Complex.I • (AR 1) := by
    simp at t₂
    exact t₂
  let C : HasFDerivAt f (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) z := h.hasFDerivAt.restrictScalars ℝ
  have t₃ : fderiv ℝ f z = ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z) := by
    exact DifferentiableAt.fderiv_restrictScalars ℝ h
  rw [t₃]
  exact t₂c

theorem CauchyRiemann₂ : (DifferentiableAt ℂ f z)
  → lineDeriv ℝ f z Complex.I = Complex.I * lineDeriv ℝ f z 1 := by
  intro h

  have : lineDeriv ℝ f z Complex.I = (fderiv ℝ f z) Complex.I := by
    apply DifferentiableAt.lineDeriv_eq_fderiv
    apply h.restrictScalars ℝ
  rw [this]

  have : lineDeriv ℝ f z 1 = (fderiv ℝ f z) 1 := by
    apply DifferentiableAt.lineDeriv_eq_fderiv
    apply h.restrictScalars ℝ
  rw [this]

  exact CauchyRiemann₁ h

theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
  → lineDeriv ℝ (Complex.reCLM ∘ f) z 1 = lineDeriv ℝ (Complex.imCLM ∘ f) z Complex.I := by

  -- Proof starts here
  intro h

  have t₀₀ : DifferentiableAt ℝ f z := by
    exact h.restrictScalars ℝ

  have t₀₁ : DifferentiableAt ℝ Complex.reCLM (f z) := by
    have : ∀ w, DifferentiableAt ℝ Complex.reCLM w := by
      intro w
      refine Differentiable.differentiableAt ?h
      exact ContinuousLinearMap.differentiable (Complex.reCLM : ℂ →L[ℝ] ℝ)
    exact this (f z)

  have t₁ : DifferentiableAt ℝ (Complex.reCLM ∘ f) z := by
    apply t₀₁.comp
    exact t₀₀

  have t₂ : lineDeriv ℝ (Complex.reCLM ∘ f) z 1 = (fderiv ℝ (Complex.reCLM ∘ f) z) 1 := by
    apply DifferentiableAt.lineDeriv_eq_fderiv
    exact t₁
  rw [t₂]

  have s₀₀ : DifferentiableAt ℝ f z := by
    exact h.restrictScalars ℝ

  have s₀₁ : DifferentiableAt ℝ Complex.imCLM (f z) := by
    have : ∀ w, DifferentiableAt ℝ Complex.imCLM w := by
      intro w
      apply Differentiable.differentiableAt
      exact ContinuousLinearMap.differentiable (Complex.imCLM : ℂ →L[ℝ] ℝ)
    exact this (f z)

  have s₁ : DifferentiableAt ℝ (Complex.im ∘ f) z := by
    apply s₀₁.comp
    exact s₀₀

  have s₂ : lineDeriv ℝ (Complex.imCLM ∘ f) z Complex.I = (fderiv ℝ (Complex.imCLM ∘ f) z) Complex.I := by
    apply DifferentiableAt.lineDeriv_eq_fderiv
    exact s₁
  rw [s₂]

  rw [fderiv.comp, fderiv.comp]
  simp
  rw [CauchyRiemann₁ h]

  have u₁ : ∀ w, fderiv ℝ Complex.reCLM w = Complex.reCLM := by
    exact fun w => ContinuousLinearMap.fderiv Complex.reCLM

  --rw [u₁ (f z)]
  have u₂ : ∀ w, fderiv ℝ Complex.imCLM w = Complex.imCLM := by
    exact fun w => ContinuousLinearMap.fderiv Complex.imCLM
  -- rw [u₂ (f z)]
  rw [Complex.I_mul]


  -- DifferentiableAt ℝ Complex.im (f z)
  exact Complex.imCLM.differentiableAt


  -- DifferentiableAt ℝ f z
  exact t₀₀

  -- DifferentiableAt ℝ Complex.re (f z)
  exact Complex.reCLM.differentiableAt

  -- DifferentiableAt ℝ f z
  exact t₀₀