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

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

Tactic:
simp

Result:
no goals

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

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

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

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

Tactic:
have A : HasStrictFDerivAt ((↑) : ℝ → ℂ) ofRealCLM z := ofRealCLM.hasStrictFDerivAt

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

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

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

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

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

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

Tactic:
have C : HasStrictFDerivAt re reCLM (e (ofRealCLM z)) := reCLM.hasStrictFDerivAt

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