[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
⊢ HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
have A : HasStrictFDerivAt ((↑) : ℝ → ℂ) ofRealClm z := ofRealClm.hasStrictFDerivAt
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
A : HasStrictFDerivAt ofReal' ofRealClm z
⊢ HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
have B : HasStrictFDerivAt e ((ContinuousLinearMap.smulRight 1 e' : ℂ →L[ℂ] ℂ).restrictScalars ℝ) (ofRealClm z) :=
  h.hasStrictFDerivAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
A : HasStrictFDerivAt ofReal' ofRealClm z
B : HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
⊢ HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
have C : HasStrictFDerivAt re reClm (e (ofRealClm z)) := reClm.hasStrictFDerivAt
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
A : HasStrictFDerivAt ofReal' ofRealClm z
B : HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
C : HasStrictFDerivAt re reClm (e (↑ofRealClm z))
⊢ HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
convert (C.comp z (B.comp z A)).hasStrictDerivAt
[GOAL]
case h.e'_7
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
A : HasStrictFDerivAt ofReal' ofRealClm z
B : HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
C : HasStrictFDerivAt re reClm (e (↑ofRealClm z))
⊢ e'.re =
    ↑(ContinuousLinearMap.comp reClm
          (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e'))
            ofRealClm))
      1
[PROOFSTEP]
rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply]
[GOAL]
case h.e'_7
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
A : HasStrictFDerivAt ofReal' ofRealClm z
B : HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
C : HasStrictFDerivAt re reClm (e (↑ofRealClm z))
⊢ e'.re = ↑reClm (↑(ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm 1))
[PROOFSTEP]
simp
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
⊢ HasDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
have A : HasFDerivAt ((↑) : ℝ → ℂ) ofRealClm z := ofRealClm.hasFDerivAt
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
A : HasFDerivAt ofReal' ofRealClm z
⊢ HasDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
have B : HasFDerivAt e ((ContinuousLinearMap.smulRight 1 e' : ℂ →L[ℂ] ℂ).restrictScalars ℝ) (ofRealClm z) :=
  h.hasFDerivAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
A : HasFDerivAt ofReal' ofRealClm z
B : HasFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
⊢ HasDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
have C : HasFDerivAt re reClm (e (ofRealClm z)) := reClm.hasFDerivAt
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
A : HasFDerivAt ofReal' ofRealClm z
B : HasFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
C : HasFDerivAt re reClm (e (↑ofRealClm z))
⊢ HasDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
convert (C.comp z (B.comp z A)).hasDerivAt
[GOAL]
case h.e'_7
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
A : HasFDerivAt ofReal' ofRealClm z
B : HasFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
C : HasFDerivAt re reClm (e (↑ofRealClm z))
⊢ e'.re =
    ↑(ContinuousLinearMap.comp reClm
          (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e'))
            ofRealClm))
      1
[PROOFSTEP]
rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply]
[GOAL]
case h.e'_7
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
A : HasFDerivAt ofReal' ofRealClm z
B : HasFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
C : HasFDerivAt re reClm (e (↑ofRealClm z))
⊢ e'.re = ↑reClm (↑(ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm 1))
[PROOFSTEP]
simp
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
n : ℕ∞
h : ContDiffAt ℂ n e ↑z
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z
[PROOFSTEP]
have A : ContDiffAt ℝ n ((↑) : ℝ → ℂ) z := ofRealClm.contDiff.contDiffAt
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
n : ℕ∞
h : ContDiffAt ℂ n e ↑z
A : ContDiffAt ℝ n ofReal' z
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z
[PROOFSTEP]
have B : ContDiffAt ℝ n e z := h.restrict_scalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
n : ℕ∞
h : ContDiffAt ℂ n e ↑z
A : ContDiffAt ℝ n ofReal' z
B : ContDiffAt ℝ n e ↑z
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z
[PROOFSTEP]
have C : ContDiffAt ℝ n re (e z) := reClm.contDiff.contDiffAt
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
n : ℕ∞
h : ContDiffAt ℂ n e ↑z
A : ContDiffAt ℝ n ofReal' z
B : ContDiffAt ℝ n e ↑z
C : ContDiffAt ℝ n re (e ↑z)
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z
[PROOFSTEP]
exact C.comp z (B.comp z A)
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
x : ℂ
f' : E
h : HasStrictDerivAt f f' x
⊢ HasStrictFDerivAt f (ContinuousLinearMap.smulRight reClm f' + I • ContinuousLinearMap.smulRight imClm f') x
[PROOFSTEP]
simpa only [Complex.restrictScalars_one_smulRight'] using h.hasStrictFDerivAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
x : ℂ
f' : E
h : HasDerivAt f f' x
⊢ HasFDerivAt f (ContinuousLinearMap.smulRight reClm f' + I • ContinuousLinearMap.smulRight imClm f') x
[PROOFSTEP]
simpa only [Complex.restrictScalars_one_smulRight'] using h.hasFDerivAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
x : ℂ
f' : E
h : HasDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f (ContinuousLinearMap.smulRight reClm f' + I • ContinuousLinearMap.smulRight imClm f') s x
[PROOFSTEP]
simpa only [Complex.restrictScalars_one_smulRight'] using h.hasFDerivWithinAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h : HasStrictDerivAt f f' x
⊢ HasStrictFDerivAt f (f' • 1) x
[PROOFSTEP]
simpa only [Complex.restrictScalars_one_smulRight] using h.hasStrictFDerivAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h : HasDerivAt f f' x
⊢ HasFDerivAt f (f' • 1) x
[PROOFSTEP]
simpa only [Complex.restrictScalars_one_smulRight] using h.hasFDerivAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
s : Set ℂ
f' x : ℂ
h : HasDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f (f' • 1) s x
[PROOFSTEP]
simpa only [Complex.restrictScalars_one_smulRight] using h.hasFDerivWithinAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
hf : HasDerivAt e e' ↑z
⊢ HasDerivAt (fun y => e ↑y) e' z
[PROOFSTEP]
simpa only [ofRealClm_apply, ofReal_one, mul_one] using hf.comp z ofRealClm.hasDerivAt
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt f u z
⊢ HasDerivAt (fun y => ↑(f y)) (↑u) z
[PROOFSTEP]
simpa only [ofRealClm_apply, ofReal_one, real_smul, mul_one] using ofRealClm.hasDerivAt.scomp z hf
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ ConformalAt f z
[PROOFSTEP]
rw [conformalAt_iff_isConformalMap_fderiv, (h.hasFDerivAt.restrictScalars ℝ).fderiv]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ IsConformalMap (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))
[PROOFSTEP]
apply isConformalMap_complex_linear
[GOAL]
case nonzero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ fderiv ℂ f z ≠ 0
[PROOFSTEP]
simpa only [Ne.def, ext_ring_iff]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ ConformalAt f z ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
[PROOFSTEP]
rw [conformalAt_iff_isConformalMap_fderiv]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ IsConformalMap (fderiv ℝ f z) ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
[PROOFSTEP]
rw [isConformalMap_iff_is_complex_or_conj_linear]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ∧
      fderiv ℝ f z ≠ 0 ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
[PROOFSTEP]
apply and_congr_left
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ fderiv ℝ f z ≠ 0 →
    (((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
      DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z))
[PROOFSTEP]
intro h
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
[PROOFSTEP]
have h_diff := h.imp_symm fderiv_zero_of_not_differentiableAt
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
[PROOFSTEP]
apply or_congr
[GOAL]
case h.h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ map, restrictScalars ℝ map = fderiv ℝ f z) ↔ DifferentiableAt ℂ f z
[PROOFSTEP]
rw [differentiableAt_iff_restrictScalars ℝ h_diff]
[GOAL]
case h.h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
[PROOFSTEP]
rw [← conj_conj z] at h_diff 
[GOAL]
case h.h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
⊢ (∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
[PROOFSTEP]
rw [differentiableAt_iff_restrictScalars ℝ (h_diff.comp _ conjCle.differentiableAt)]
[GOAL]
case h.h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
⊢ (∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    ∃ g', restrictScalars ℝ g' = fderiv ℝ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
[PROOFSTEP]
refine' exists_congr fun g => rfl.congr _
[GOAL]
case h.h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
g : ℂ →L[ℂ] ℂ
⊢ comp (fderiv ℝ f z) ↑conjCle = fderiv ℝ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
[PROOFSTEP]
have : fderiv ℝ conj (conj z) = _ := conjCle.fderiv
[GOAL]
case h.h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
g : ℂ →L[ℂ] ℂ
this : fderiv ℝ (↑(starRingEnd ((fun x => ℂ) z))) (↑(starRingEnd ℂ) z) = ↑conjCle
⊢ comp (fderiv ℝ f z) ↑conjCle = fderiv ℝ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
[PROOFSTEP]
simp [fderiv.comp _ h_diff conjCle.differentiableAt, this, conj_conj]
