6. Chapter 6.2 Complex differentiability and Cauchy-Riemann condition🔗

import Mathlib.Tactic
import Mathlib.Data.Complex.Basic

section ComplexDifferentiability

Definition 6.2.1. Let f : ℂ → ℂ be a complex function defined in a domain D. Given a point z₀ ∈ D, we say that f is complex differentiable at z₀ if there exists a complex constant w₀ such that

f(z₀ + Δz) ≈ f(z₀) + w₀ · Δz

in the sense that the error is o(Δz) as Δz → 0. The constant w₀ is called the derivative of f at z₀.

In Mathlib, this is captured by HasDerivAt f w₀ z₀, which asserts that:

‖f(z₀ + h) - f(z₀) - w₀ • h‖ / ‖h‖ → 0 as h → 0.

open Complex Filter

def IsComplexDiffAt (f : ℂ → ℂ) (w₀ : ℂ) (z₀ : ℂ) : Prop :=
  HasDerivAt f w₀ z₀

We prove the equivalence with the classical limit definition:

Theorem 6.2.2. Complex function f is complex differentiable at z₀ with derivative w₀ if and only if

\lim_{h → 0} (f(z_0 + h) - f(z_0)) / h = w_0.

theorem isComplexDiffAt_iff_limit
  (f : ℂ → ℂ) (w₀ : ℂ) (z₀ : ℂ) :
  IsComplexDiffAt f w₀ z₀ ↔
    Tendsto (fun h =>
    (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)
  := byf:ℂ → ℂw₀:ℂz₀:ℂ⊢ IsComplexDiffAt f w₀ z₀ ↔ Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)
  convert hasDerivAt_iff_tendsto_slope_zero using 1h.e'_2.af:ℂ → ℂw₀:ℂz₀:ℂ⊢ Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀) ↔
  Tendsto (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) (nhdsWithin 0 {0}ᶜ) (nhds w₀);
  norm_num [ div_eq_inv_mul ]All goals completed! 🐙

/--  Theorem 6.2.2
  A complex function `f` is complex differentiable at `z₀`
  if and only if the limit
  `lim_{h → 0} (f(z₀ + h) - f(z₀)) / h` exists
-/
theorem complex_differentiableAt_iff_limit_exists
  (f : ℂ → ℂ) (z₀ : ℂ) :
    DifferentiableAt ℂ f z₀ ↔
      ∃ w₀ : ℂ, Tendsto (fun h =>
      (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)
  := byf:ℂ → ℂz₀:ℂ⊢ DifferentiableAt ℂ f z₀ ↔ ∃ w₀, Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)
  constructormpf:ℂ → ℂz₀:ℂ⊢ DifferentiableAt ℂ f z₀ → ∃ w₀, Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)mprf:ℂ → ℂz₀:ℂ⊢ (∃ w₀, Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)) → DifferentiableAt ℂ f z₀ <;>mpf:ℂ → ℂz₀:ℂ⊢ DifferentiableAt ℂ f z₀ → ∃ w₀, Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)mprf:ℂ → ℂz₀:ℂ⊢ (∃ w₀, Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)) → DifferentiableAt ℂ f z₀
  intro hmprf:ℂ → ℂz₀:ℂh:∃ w₀, Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)⊢ DifferentiableAt ℂ f z₀
  ·mpf:ℂ → ℂz₀:ℂh:DifferentiableAt ℂ f z₀⊢ ∃ w₀, Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀) convert isComplexDiffAt_iff_limit f ( deriv f z₀ ) z₀
      |>.1 ( h.hasDerivAt ) using 1af:ℂ → ℂz₀:ℂh:DifferentiableAt ℂ f z₀⊢ (∃ w₀, Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)) ↔
  Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds (deriv f z₀));
    constructora.mpf:ℂ → ℂz₀:ℂh:DifferentiableAt ℂ f z₀⊢ (∃ w₀, Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)) →
  Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds (deriv f z₀))a.mprf:ℂ → ℂz₀:ℂh:DifferentiableAt ℂ f z₀⊢ Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds (deriv f z₀)) →
  ∃ w₀, Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀);
    ·a.mpf:ℂ → ℂz₀:ℂh:DifferentiableAt ℂ f z₀⊢ (∃ w₀, Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)) →
  Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds (deriv f z₀)) exact fun _ =>
        hasDerivAt_iff_tendsto_slope_zero.mp h.hasDerivAt
        |> fun h => h.congr fun x
           => byf:ℂ → ℂz₀:ℂh✝:DifferentiableAt ℂ f z₀x✝:∃ w₀, Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)h:Tendsto (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) (nhdsWithin 0 {0}ᶜ) (nhds (deriv f z₀))x:ℂ⊢ x⁻¹ • (f (z₀ + x) - f z₀) = (f (z₀ + x) - f z₀) / x simp  [ div_eq_inv_mul ]All goals completed! 🐙;
    ·a.mprf:ℂ → ℂz₀:ℂh:DifferentiableAt ℂ f z₀⊢ Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds (deriv f z₀)) →
  ∃ w₀, Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀) exact fun h => ⟨ _, h ⟩All goals completed! 🐙;
  ·mprf:ℂ → ℂz₀:ℂh:∃ w₀, Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)⊢ DifferentiableAt ℂ f z₀ obtain ⟨ w₀, hw₀ ⟩ := hmprf:ℂ → ℂz₀:ℂw₀:ℂhw₀:Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)⊢ DifferentiableAt ℂ f z₀;
    specialize hw₀mprf:ℂ → ℂz₀:ℂw₀:ℂhw₀:Tendsto (fun h => (f (z₀ + h) - f z₀) / h) (nhdsWithin 0 {0}ᶜ) (nhds w₀)⊢ DifferentiableAt ℂ f z₀;
    simp_all [ div_eq_inv_mul ]mprf:ℂ → ℂz₀:ℂw₀:ℂhw₀:Tendsto (fun h => h⁻¹ * (f (z₀ + h) - f z₀)) (nhdsWithin 0 {0}ᶜ) (nhds w₀)⊢ DifferentiableAt ℂ f z₀ ;
    refine' ⟨ _, hasDerivAt_iff_tendsto_slope_zero.mpr _ ⟩mpr.refine'_1f:ℂ → ℂz₀:ℂw₀:ℂhw₀:Tendsto (fun h => h⁻¹ * (f (z₀ + h) - f z₀)) (nhdsWithin 0 {0}ᶜ) (nhds w₀)⊢ ℂmpr.refine'_2f:ℂ → ℂz₀:ℂw₀:ℂhw₀:Tendsto (fun h => h⁻¹ * (f (z₀ + h) - f z₀)) (nhdsWithin 0 {0}ᶜ) (nhds w₀)⊢ Tendsto (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) (nhdsWithin 0 {0}ᶜ) (nhds ?mpr.refine'_1)
    exacts [ w₀, hw₀ ]All goals completed! 🐙

Next, we prove another equivalent condition for complex differentiability expressed in terms of Cauchy-Riemann equation.

The function defined by multiplying a complex constant c from the left is linear in two senses. It is both \mathbb{R}-linear and is \mathbb{C}-linear. We distinguish them by two different definitions. The Cauchy-Riemann condition is a consequence of studying complex differentiable function as a real-linear function.

/-- Multiplication by `c` is an ℝ-linear continuous map
    `ℂ →L[ℝ] ℂ`. -/
noncomputable def ContLinearMap.mulLeftReal (c : ℂ)
  : ℂ →L[ℝ] ℂ where
  toFun z := c * z
  map_add' x y := byc:ℂx:ℂy:ℂ⊢ c * (x + y) = c * x + c * y ringAll goals completed! 🐙
  map_smul' r x := byc:ℂr:ℝx:ℂ⊢ c * r • x = (RingHom.id ℝ) r • (c * x) exact mul_smul_comm r c xAll goals completed! 🐙
  cont := continuous_const.mul continuous_id

/-- Multiplication by `c` is a ℂ-linear continuous map
    `ℂ →L[ℂ] ℂ`. -/
noncomputable def ContLinearMap.mulLeftComplex
  (c : ℂ) : ℂ →L[ℂ] ℂ where
  toFun z := c * z
  map_add' x y := byc:ℂx:ℂy:ℂ⊢ c * (x + y) = c * x + c * y ringAll goals completed! 🐙
  map_smul' r x := byc:ℂr:ℂx:ℂ⊢ c * r • x = (RingHom.id ℂ) r • (c * x) simpc:ℂr:ℂx:ℂ⊢ c * (r * x) = r * (c * x); ringAll goals completed! 🐙
  cont := continuous_const.mul continuous_id

Two helper functions to be used in the proof of the main theorem.

@[simp]
lemma ContLinearMap.mulLeftReal_apply (c z : ℂ) :
    ContLinearMap.mulLeftReal c z = c * z := rfl

@[simp]
lemma ContLinearMap.mulLeftComplex_apply (c z : ℂ) :
    ContLinearMap.mulLeftComplex c z = c * z := rfl

We need some lemmas about real-linear and complex-linear functions.

/-- Every ℂ-linear map ℂ → ℂ is multiplication
    by a constant -/
lemma ContLinearMap.complex_apply_eq_mul
  (L : ℂ →L[ℂ] ℂ) (z : ℂ) :
  L z = L 1 * z := byL:ℂ →L[ℂ] ℂz:ℂ⊢ L z = L 1 * z
    convert L.map_smul z 1 using 1h.e'_2L:ℂ →L[ℂ] ℂz:ℂ⊢ L z = L (z • 1)h.e'_3L:ℂ →L[ℂ] ℂz:ℂ⊢ L 1 * z = z • L 1 <;>h.e'_2L:ℂ →L[ℂ] ℂz:ℂ⊢ L z = L (z • 1)h.e'_3L:ℂ →L[ℂ] ℂz:ℂ⊢ L 1 * z = z • L 1
    simp [mul_comm]All goals completed! 🐙

/-- Suppose two functions are equal, and one of them
  is real linear and the other one is complex linear.
  Then if the first one has deriative,
  the second one also has derivative  -/
lemma hasFDerivAt_complex_real {f : ℂ → ℂ}
  {L₁ : ℂ →L[ℂ] ℂ} {L₂ : ℂ →L[ℝ] ℂ}
    {z₀ : ℂ} (h : HasFDerivAt f L₁ z₀)
    (heq : ∀ z, L₁ z = L₂ z) :
    HasFDerivAt f L₂ z₀ := byf:ℂ → ℂL₁:ℂ →L[ℂ] ℂL₂:ℂ →L[ℝ] ℂz₀:ℂh:HasFDerivAt f L₁ z₀heq:∀ (z : ℂ), L₁ z = L₂ z⊢ HasFDerivAt f L₂ z₀
  rw [hasFDerivAt_iff_isLittleO_nhds_zero] at *f:ℂ → ℂL₁:ℂ →L[ℂ] ℂL₂:ℂ →L[ℝ] ℂz₀:ℂh:(fun h => f (z₀ + h) - f z₀ - L₁ h) =o[nhds 0] fun h => hheq:∀ (z : ℂ), L₁ z = L₂ z⊢ (fun h => f (z₀ + h) - f z₀ - L₂ h) =o[nhds 0] fun h => h;
  simp_allAll goals completed! 🐙


lemma hasFDerivAt_real_complex {f : ℂ → ℂ}
  {L₁ : ℂ →L[ℝ] ℂ} {L₂ : ℂ →L[ℂ] ℂ}
  {z₀ : ℂ} (h : HasFDerivAt f L₁ z₀)
  (heq : ∀ z, L₁ z = L₂ z) :
    HasFDerivAt f L₂ z₀ := byf:ℂ → ℂL₁:ℂ →L[ℝ] ℂL₂:ℂ →L[ℂ] ℂz₀:ℂh:HasFDerivAt f L₁ z₀heq:∀ (z : ℂ), L₁ z = L₂ z⊢ HasFDerivAt f L₂ z₀
  rw [hasFDerivAt_iff_isLittleO_nhds_zero] at *f:ℂ → ℂL₁:ℂ →L[ℝ] ℂL₂:ℂ →L[ℂ] ℂz₀:ℂh:(fun h => f (z₀ + h) - f z₀ - L₁ h) =o[nhds 0] fun h => hheq:∀ (z : ℂ), L₁ z = L₂ z⊢ (fun h => f (z₀ + h) - f z₀ - L₂ h) =o[nhds 0] fun h => h;
  simp_allAll goals completed! 🐙

/-- Helper lemmas for ℝ-linear maps on ℂ -/
lemma clm_real_apply_eq (L : ℂ →L[ℝ] ℂ) (z : ℂ) :
    L z = z.re • L 1 + z.im • L I := byL:ℂ →L[ℝ] ℂz:ℂ⊢ L z = z.re • L 1 + z.im • L I
  convert L.map_add (z.re • 1) (z.im • Complex.I) using 1h.e'_2L:ℂ →L[ℝ] ℂz:ℂ⊢ L z = L (z.re • 1 + z.im • I)h.e'_3L:ℂ →L[ℝ] ℂz:ℂ⊢ z.re • L 1 + z.im • L I = L (z.re • 1) + L (z.im • I)
  ·h.e'_2L:ℂ →L[ℝ] ℂz:ℂ⊢ L z = L (z.re • 1 + z.im • I) norm_numAll goals completed! 🐙;
  ·h.e'_3L:ℂ →L[ℝ] ℂz:ℂ⊢ z.re • L 1 + z.im • L I = L (z.re • 1) + L (z.im • I) rw [map_smul, map_smul]All goals completed! 🐙

/-- Real continuous linear map is complex linear if CR -/
lemma clm_real_is_mul_of_CR (L : ℂ →L[ℝ] ℂ)
    (h1 : (L 1).re = (L I).im) (h2: (L I).re = -(L 1).im) :
    ∀ z, L z = (L 1) * z := byL:ℂ →L[ℝ] ℂh1:(L 1).re = (L I).imh2:(L I).re = -(L 1).im⊢ ∀ (z : ℂ), L z = L 1 * z
  intro zL:ℂ →L[ℝ] ℂh1:(L 1).re = (L I).imh2:(L I).re = -(L 1).imz:ℂ⊢ L z = L 1 * z;
  exact (byL:ℂ →L[ℝ] ℂh1:(L 1).re = (L I).imh2:(L I).re = -(L 1).imz:ℂ⊢ L z = L 1 * z
    convert clm_real_apply_eq L z using 1h.e'_3L:ℂ →L[ℝ] ℂh1:(L 1).re = (L I).imh2:(L I).re = -(L 1).imz:ℂ⊢ L 1 * z = z.re • L 1 + z.im • L I ;
    simp [ *, Complex.ext_iff, mul_comm ]h.e'_3L:ℂ →L[ℝ] ℂh1:(L 1).re = (L I).imh2:(L I).re = -(L 1).imz:ℂ⊢ z.re * (L I).im - z.im * (L 1).im = z.re * (L I).im + -(z.im * (L 1).im) ; ringAll goals completed! 🐙;)

Theorem 6.2.4. Suppose f(z) = u(x, y)+iv(x, y) is a complex function defined on a domain which contains z_0 = x_0 + iy_0. Then, f is complex differentiable at z_0 = x_0+iy_0 if and only if

the vector function (u(x, y), v(x, y)) is real-differentiable at (x_0, y_0),
the partial derivatives satisfy the Cauchy-Riemann equations

u_x = v_y, u_y = -v_x at (x_0,y_0)

/--  An equivalent condition for complex differentiability
-/
theorem complex_diff_iff_real_diff_and_CR
  (f : ℂ → ℂ) (z₀ : ℂ) :
    DifferentiableAt ℂ f z₀ ↔
    DifferentiableAt ℝ f z₀ ∧
    let u_x := (fderiv ℝ f z₀ 1).re
    let v_x := (fderiv ℝ f z₀ 1).im
    let u_y := (fderiv ℝ f z₀ I).re
    let v_y := (fderiv ℝ f z₀ I).im
    u_x = v_y ∧ u_y = -v_x := byf:ℂ → ℂz₀:ℂ⊢ DifferentiableAt ℂ f z₀ ↔
  DifferentiableAt ℝ f z₀ ∧
    let u_x := ((fderiv ℝ f z₀) 1).re;
    let v_x := ((fderiv ℝ f z₀) 1).im;
    let u_y := ((fderiv ℝ f z₀) I).re;
    let v_y := ((fderiv ℝ f z₀) I).im;
    u_x = v_y ∧ u_y = -v_x
  constructormpf:ℂ → ℂz₀:ℂ⊢ DifferentiableAt ℂ f z₀ →
  DifferentiableAt ℝ f z₀ ∧
    let u_x := ((fderiv ℝ f z₀) 1).re;
    let v_x := ((fderiv ℝ f z₀) 1).im;
    let u_y := ((fderiv ℝ f z₀) I).re;
    let v_y := ((fderiv ℝ f z₀) I).im;
    u_x = v_y ∧ u_y = -v_xmprf:ℂ → ℂz₀:ℂ⊢ (DifferentiableAt ℝ f z₀ ∧
    let u_x := ((fderiv ℝ f z₀) 1).re;
    let v_x := ((fderiv ℝ f z₀) 1).im;
    let u_y := ((fderiv ℝ f z₀) I).re;
    let v_y := ((fderiv ℝ f z₀) I).im;
    u_x = v_y ∧ u_y = -v_x) →
  DifferentiableAt ℂ f z₀
  ·mpf:ℂ → ℂz₀:ℂ⊢ DifferentiableAt ℂ f z₀ →
  DifferentiableAt ℝ f z₀ ∧
    let u_x := ((fderiv ℝ f z₀) 1).re;
    let v_x := ((fderiv ℝ f z₀) 1).im;
    let u_y := ((fderiv ℝ f z₀) I).re;
    let v_y := ((fderiv ℝ f z₀) I).im;
    u_x = v_y ∧ u_y = -v_x -- Forward: ℂ-differentiable → ℝ-differentiable + CR
    intro hfmpf:ℂ → ℂz₀:ℂhf:DifferentiableAt ℂ f z₀⊢ DifferentiableAt ℝ f z₀ ∧
  let u_x := ((fderiv ℝ f z₀) 1).re;
  let v_x := ((fderiv ℝ f z₀) 1).im;
  let u_y := ((fderiv ℝ f z₀) I).re;
  let v_y := ((fderiv ℝ f z₀) I).im;
  u_x = v_y ∧ u_y = -v_x
    obtain ⟨L, hL⟩ := hfmpf:ℂ → ℂz₀:ℂL:ℂ →L[ℂ] ℂhL:HasFDerivAt f L z₀⊢ DifferentiableAt ℝ f z₀ ∧
  let u_x := ((fderiv ℝ f z₀) 1).re;
  let v_x := ((fderiv ℝ f z₀) 1).im;
  let u_y := ((fderiv ℝ f z₀) I).re;
  let v_y := ((fderiv ℝ f z₀) I).im;
  u_x = v_y ∧ u_y = -v_x
    let c := L 1mpf:ℂ → ℂz₀:ℂL:ℂ →L[ℂ] ℂhL:HasFDerivAt f L z₀c:ℂ := L 1⊢ DifferentiableAt ℝ f z₀ ∧
  let u_x := ((fderiv ℝ f z₀) 1).re;
  let v_x := ((fderiv ℝ f z₀) 1).im;
  let u_y := ((fderiv ℝ f z₀) I).re;
  let v_y := ((fderiv ℝ f z₀) I).im;
  u_x = v_y ∧ u_y = -v_x
    -- Transfer to ℝ-HasFDerivAt via mulLeftReal
    have hL_real : HasFDerivAt f
      (ContLinearMap.mulLeftReal c) z₀ :=
      hasFDerivAt_complex_real hL (fun z => byf:ℂ → ℂz₀:ℂL:ℂ →L[ℂ] ℂhL:HasFDerivAt f L z₀c:ℂ := L 1z:ℂ⊢ L z = (ContLinearMap.mulLeftReal c) z
        show L z = c * zf:ℂ → ℂz₀:ℂL:ℂ →L[ℂ] ℂhL:HasFDerivAt f L z₀c:ℂ := L 1z:ℂ⊢ L z = c * z
        exact ContLinearMap.complex_apply_eq_mul L zAll goals completed! 🐙)
    constructormp.leftf:ℂ → ℂz₀:ℂL:ℂ →L[ℂ] ℂhL:HasFDerivAt f L z₀c:ℂ := L 1hL_real:HasFDerivAt f (ContLinearMap.mulLeftReal c) z₀⊢ DifferentiableAt ℝ f z₀mp.rightf:ℂ → ℂz₀:ℂL:ℂ →L[ℂ] ℂhL:HasFDerivAt f L z₀c:ℂ := L 1hL_real:HasFDerivAt f (ContLinearMap.mulLeftReal c) z₀⊢ let u_x := ((fderiv ℝ f z₀) 1).re;
let v_x := ((fderiv ℝ f z₀) 1).im;
let u_y := ((fderiv ℝ f z₀) I).re;
let v_y := ((fderiv ℝ f z₀) I).im;
u_x = v_y ∧ u_y = -v_x
    ·mp.leftf:ℂ → ℂz₀:ℂL:ℂ →L[ℂ] ℂhL:HasFDerivAt f L z₀c:ℂ := L 1hL_real:HasFDerivAt f (ContLinearMap.mulLeftReal c) z₀⊢ DifferentiableAt ℝ f z₀ exact hL_real.differentiableAtAll goals completed! 🐙
    ·mp.rightf:ℂ → ℂz₀:ℂL:ℂ →L[ℂ] ℂhL:HasFDerivAt f L z₀c:ℂ := L 1hL_real:HasFDerivAt f (ContLinearMap.mulLeftReal c) z₀⊢ let u_x := ((fderiv ℝ f z₀) 1).re;
let v_x := ((fderiv ℝ f z₀) 1).im;
let u_y := ((fderiv ℝ f z₀) I).re;
let v_y := ((fderiv ℝ f z₀) I).im;
u_x = v_y ∧ u_y = -v_x -- CR equations
      have h_eq : fderiv ℝ f z₀ =
        ContLinearMap.mulLeftReal c := hL_real.fderivmp.rightf:ℂ → ℂz₀:ℂL:ℂ →L[ℂ] ℂhL:HasFDerivAt f L z₀c:ℂ := L 1hL_real:HasFDerivAt f (ContLinearMap.mulLeftReal c) z₀h_eq:fderiv ℝ f z₀ = ContLinearMap.mulLeftReal c⊢ let u_x := ((fderiv ℝ f z₀) 1).re;
let v_x := ((fderiv ℝ f z₀) 1).im;
let u_y := ((fderiv ℝ f z₀) I).re;
let v_y := ((fderiv ℝ f z₀) I).im;
u_x = v_y ∧ u_y = -v_x
      simp only [h_eq,
        ContLinearMap.mulLeftReal_apply]mp.rightf:ℂ → ℂz₀:ℂL:ℂ →L[ℂ] ℂhL:HasFDerivAt f L z₀c:ℂ := L 1hL_real:HasFDerivAt f (ContLinearMap.mulLeftReal c) z₀h_eq:fderiv ℝ f z₀ = ContLinearMap.mulLeftReal c⊢ (c * 1).re = (c * I).im ∧ (c * I).re = -(c * 1).im
      constructormp.right.leftf:ℂ → ℂz₀:ℂL:ℂ →L[ℂ] ℂhL:HasFDerivAt f L z₀c:ℂ := L 1hL_real:HasFDerivAt f (ContLinearMap.mulLeftReal c) z₀h_eq:fderiv ℝ f z₀ = ContLinearMap.mulLeftReal c⊢ (c * 1).re = (c * I).immp.right.rightf:ℂ → ℂz₀:ℂL:ℂ →L[ℂ] ℂhL:HasFDerivAt f L z₀c:ℂ := L 1hL_real:HasFDerivAt f (ContLinearMap.mulLeftReal c) z₀h_eq:fderiv ℝ f z₀ = ContLinearMap.mulLeftReal c⊢ (c * I).re = -(c * 1).im <;>mp.right.leftf:ℂ → ℂz₀:ℂL:ℂ →L[ℂ] ℂhL:HasFDerivAt f L z₀c:ℂ := L 1hL_real:HasFDerivAt f (ContLinearMap.mulLeftReal c) z₀h_eq:fderiv ℝ f z₀ = ContLinearMap.mulLeftReal c⊢ (c * 1).re = (c * I).immp.right.rightf:ℂ → ℂz₀:ℂL:ℂ →L[ℂ] ℂhL:HasFDerivAt f L z₀c:ℂ := L 1hL_real:HasFDerivAt f (ContLinearMap.mulLeftReal c) z₀h_eq:fderiv ℝ f z₀ = ContLinearMap.mulLeftReal c⊢ (c * I).re = -(c * 1).im simp [mul_comm]All goals completed! 🐙
  ·mprf:ℂ → ℂz₀:ℂ⊢ (DifferentiableAt ℝ f z₀ ∧
    let u_x := ((fderiv ℝ f z₀) 1).re;
    let v_x := ((fderiv ℝ f z₀) 1).im;
    let u_y := ((fderiv ℝ f z₀) I).re;
    let v_y := ((fderiv ℝ f z₀) I).im;
    u_x = v_y ∧ u_y = -v_x) →
  DifferentiableAt ℂ f z₀ -- Backward: ℝ-differentiable + CR → ℂ-differentiable
    rintro ⟨hf_real, h1, h2⟩mprf:ℂ → ℂz₀:ℂhf_real:DifferentiableAt ℝ f z₀h1:((fderiv ℝ f z₀) 1).re = ((fderiv ℝ f z₀) I).imh2:((fderiv ℝ f z₀) I).re = -((fderiv ℝ f z₀) 1).im⊢ DifferentiableAt ℂ f z₀
    have h_mul : ∀ z : ℂ, fderiv ℝ f z₀ z =
      (fderiv ℝ f z₀ 1) * z :=
      clm_real_is_mul_of_CR (fderiv ℝ f z₀) h1 h2mprf:ℂ → ℂz₀:ℂhf_real:DifferentiableAt ℝ f z₀h1:((fderiv ℝ f z₀) 1).re = ((fderiv ℝ f z₀) I).imh2:((fderiv ℝ f z₀) I).re = -((fderiv ℝ f z₀) 1).imh_mul:∀ (z : ℂ), (fderiv ℝ f z₀) z = (fderiv ℝ f z₀) 1 * z⊢ DifferentiableAt ℂ f z₀
    have h_complex : HasFDerivAt f
      (ContLinearMap.mulLeftComplex
      (fderiv ℝ f z₀ 1)) z₀ :=
      hasFDerivAt_real_complex hf_real.hasFDerivAt
      (fun z => byf:ℂ → ℂz₀:ℂhf_real:DifferentiableAt ℝ f z₀h1:((fderiv ℝ f z₀) 1).re = ((fderiv ℝ f z₀) I).imh2:((fderiv ℝ f z₀) I).re = -((fderiv ℝ f z₀) 1).imh_mul:∀ (z : ℂ), (fderiv ℝ f z₀) z = (fderiv ℝ f z₀) 1 * zz:ℂ⊢ (fderiv ℝ f z₀) z = (ContLinearMap.mulLeftComplex ((fderiv ℝ f z₀) 1)) z simp [h_mul z]All goals completed! 🐙)
    exact h_complex.differentiableAtAll goals completed! 🐙

As a corollary, we obtain a necessary condition for complex differentiability.

Theorem 6.2.3. If a complex function is complex differentiable at a point, then it satisfies Cauchy-Riemann equation.

theorem complex_diff_implies_CR
  (f : ℂ → ℂ) (z₀ : ℂ) :
    DifferentiableAt ℂ f z₀ →
    DifferentiableAt ℝ f z₀ ∧
    let u_x := (fderiv ℝ f z₀ 1).re
    let v_x := (fderiv ℝ f z₀ 1).im
    let u_y := (fderiv ℝ f z₀ I).re
    let v_y := (fderiv ℝ f z₀ I).im
    u_x = v_y ∧ u_y = -v_x := byf:ℂ → ℂz₀:ℂ⊢ DifferentiableAt ℂ f z₀ →
  DifferentiableAt ℝ f z₀ ∧
    let u_x := ((fderiv ℝ f z₀) 1).re;
    let v_x := ((fderiv ℝ f z₀) 1).im;
    let u_y := ((fderiv ℝ f z₀) I).re;
    let v_y := ((fderiv ℝ f z₀) I).im;
    u_x = v_y ∧ u_y = -v_x
  intro hf:ℂ → ℂz₀:ℂh:DifferentiableAt ℂ f z₀⊢ DifferentiableAt ℝ f z₀ ∧
  let u_x := ((fderiv ℝ f z₀) 1).re;
  let v_x := ((fderiv ℝ f z₀) 1).im;
  let u_y := ((fderiv ℝ f z₀) I).re;
  let v_y := ((fderiv ℝ f z₀) I).im;
  u_x = v_y ∧ u_y = -v_x
  exact (complex_diff_iff_real_diff_and_CR f z₀).mp hAll goals completed! 🐙

end ComplexDifferentiability