-- Mathlib/Analysis/Complex/RealDeriv.lean
theorem HasDerivAt.real_of_complex (h : HasDerivAt e e' z) :
    HasDerivAt (fun x : ℝ => (e x).re) e'.re z

Proof state:
case h.e'_9
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))

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_9
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.comp ((ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')).comp ofRealCLM)) 1

Tactic:
rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply]

Result:
case h.e'_9
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))

Proof state:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
A : HasFDerivAt ofReal ofRealCLM z
⊢ HasDerivAt (fun x => (e ↑x).re) e'.re z

Tactic:
have B :
  HasFDerivAt e ((ContinuousLinearMap.smulRight 1 e' : ℂ →L[ℂ] ℂ).restrictScalars ℝ)
    (ofRealCLM z) :=
  h.hasFDerivAt.restrictScalars ℝ

Result:
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

Proof state:
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

Tactic:
convert (C.comp z (B.comp z A)).hasDerivAt

Result:
case h.e'_9
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.comp ((ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')).comp ofRealCLM)) 1

Proof state:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
⊢ HasDerivAt (fun x => (e ↑x).re) e'.re z

Tactic:
have A : HasFDerivAt ((↑) : ℝ → ℂ) ofRealCLM z := ofRealCLM.hasFDerivAt

Result:
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
A : HasFDerivAt ofReal ofRealCLM z
⊢ HasDerivAt (fun x => (e ↑x).re) e'.re z

Proof state:
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

Tactic:
have C : HasFDerivAt re reCLM (e (ofRealCLM z)) := reCLM.hasFDerivAt

Result:
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