e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
A : HasStrictFDerivAt ofReal' ofRealClm z
⊢ HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
⊢ HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
have A : HasStrictFDerivAt ((↑) : ℝ → ℂ) ofRealClm z := ofRealClm.hasStrictFDerivAt
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
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
A : HasStrictFDerivAt ofReal' ofRealClm z
⊢ HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
have B :
  HasStrictFDerivAt e ((ContinuousLinearMap.smulRight 1 e' : ℂ →L[ℂ] ℂ).restrictScalars ℝ)
    (ofRealClm z) :=
  h.hasStrictFDerivAt.restrictScalars ℝ
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
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
have C : HasStrictFDerivAt re reClm (e (ofRealClm z)) := reClm.hasStrictFDerivAt
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
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
convert (C.comp z (B.comp z A)).hasStrictDerivAt
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))
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
rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply]
no goals
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))
simp