Update cauchyRiemann.lean

nevanlinna/cauchyRiemann.lean

@@ -22,74 +22,19 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
     ∧ (lineDeriv ℝ (Complex.reCLM ∘ f) z Complex.I = -lineDeriv ℝ (Complex.imCLM ∘ f) z 1)
    := by
 
-  -- Proof starts here
   intro h
 
-  have t₀₀ : DifferentiableAt ℝ f z := by
+  have ContinuousLinearMap.comp_lineDeriv : ∀ w : ℂ, ∀ l : ℂ →L[ℝ] ℝ, lineDeriv ℝ (l ∘ f) z w = l ((fderiv ℝ f z) w) := by
-    exact h.restrictScalars ℝ
+    intro w l
-  have t₀₁ : DifferentiableAt ℝ Complex.reCLM (f z) := by
+    rw [DifferentiableAt.lineDeriv_eq_fderiv]
-    have : ∀ w, DifferentiableAt ℝ Complex.reCLM w := by
+    rw [fderiv.comp]
-      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₁
-  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₁
-
-  constructor
-  · rw [t₂, s₂]
-    rw [fderiv.comp, fderiv.comp]
     simp
-    rw [CauchyRiemann₁ h]
+    fun_prop
-    rw [Complex.I_mul]
+    exact h.restrictScalars ℝ  
-    -- DifferentiableAt ℝ Complex.im (f z)
+    apply (ContinuousLinearMap.differentiableAt l).comp
-    exact Complex.imCLM.differentiableAt
+    exact h.restrictScalars ℝ
 
-    -- DifferentiableAt ℝ f z
+  repeat
-    exact t₀₀
+    rw [ContinuousLinearMap.comp_lineDeriv]
-
+  rw [CauchyRiemann₁ h, Complex.I_mul]
-    -- DifferentiableAt ℝ Complex.re (f z)
+  simp
-    exact Complex.reCLM.differentiableAt
-
-    -- DifferentiableAt ℝ f z
-    exact t₀₀
-  · have r₂ : lineDeriv ℝ (Complex.reCLM ∘ f) z Complex.I = (fderiv ℝ (Complex.reCLM ∘ f) z) Complex.I := by
-      apply DifferentiableAt.lineDeriv_eq_fderiv
-      exact t₁
-    have p₂ : lineDeriv ℝ (Complex.imCLM ∘ f) z 1 = (fderiv ℝ (Complex.imCLM ∘ f) z) 1 := by
-      apply DifferentiableAt.lineDeriv_eq_fderiv
-      exact s₁
-    rw [r₂, p₂]
-    rw [fderiv.comp, fderiv.comp]
-    simp
-    rw [CauchyRiemann₁ h]
-    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₀₀