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.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 : ℂ → ℂ}

example (h : DifferentiableAt ℂ f z) : f z = 0 := by

  let A := fderiv ℂ f z
  let B := fderiv ℝ f

  let C : HasFDerivAt f (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) z := h.hasFDerivAt.restrictScalars ℝ
  let D := ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)
  let E := D 1
  let F := D Complex.I

  have : 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 : AR (Complex.I • 1) = Complex.I • (AR 1) := by
    exact this

  let f₂ := fun x ↦ lineDeriv ℝ f x ⟨0,1⟩
  have : lineDeriv ℝ f z Complex.I = (fderiv ℝ f z) Complex.I := by
    apply DifferentiableAt.lineDeriv_eq_fderiv
    apply h.restrictScalars ℝ

  have : D Complex.I = Complex.I * (D 1) := by
    -- x

    sorry

  have : HasFDerivAt f A z := by
    exact DifferentiableAt.hasFDerivAt h

  have : HasFDerivAt f (B z) z := by
    sorry


  sorry