awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
refine :
  (fderiv ℝ
          ((Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
            HSMul.hSMul (β := ℂ → ℂ) I
              (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I))
          x :
        (a : ℂ) → ℂ)
      I =
    HSMul.hSMul (β := ℂ) I
      ((fderiv ℝ
              ((Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
                HSMul.hSMul (β := ℂ → ℂ) I
                  (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I))
              x :
            (a : ℂ) → ℂ)
          1 :
        ℂ)
⊢ DifferentiableAt ℂ
    ((Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I))
    x

Tactic:
refine differentiableAt_complex_iff_differentiableAt_real.2 ⟨by fun_prop, ?_⟩

Premises used: Iff.mpr, differentiableAt_complex_iff_differentiableAt_real, And.intro
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
⊢ DifferentiableAt ℝ (F := ℂ)
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
⊢ DifferentiableAt ℝ
    (HSMul.hSMul (β := ℂ → ℂ) I
      (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I))
    x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
⊢ DifferentiableAt ℝ (F := ℂ)
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
rw :
  (fderiv ℝ (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x -
          HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
            (fderiv ℝ (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
              x) :
        (a : ℂ) → ℂ)
      I =
    HSMul.hSMul (β := ℂ) I
      ((fderiv ℝ (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x -
              HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
                (fderiv ℝ
                  (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x) :
            (a : ℂ) → ℂ)
          1 :
        ℂ)
⊢ (fderiv ℝ
          ((Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
            HSMul.hSMul (β := ℂ → ℂ) I
              (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I))
          x :
        (a : ℂ) → ℂ)
      I =
    HSMul.hSMul (β := ℂ) I
      ((fderiv ℝ
              ((Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
                HSMul.hSMul (β := ℂ → ℂ) I
                  (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I))
              x :
            (a : ℂ) → ℂ)
          1 :
        ℂ)

Tactic:
rw [fderiv_sub (by fun_prop) (by fun_prop), fderiv_const_smul (by fun_prop)]

Premises used: fderiv_sub, fderiv_const_smul
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
rw :
  (ContinuousLinearMap.comp (M₂ := ℝ) (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) 1) : ℝ →L[ℝ] ℂ)
            (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : ℂ →L[ℝ] ℝ) -
          HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
            (fderiv ℝ (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
              x) :
        (a : ℂ) → ℂ)
      I =
    HSMul.hSMul (β := ℂ) I
      ((ContinuousLinearMap.comp (M₂ := ℝ)
                (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) 1) : ℝ →L[ℝ] ℂ)
                (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : ℂ →L[ℝ] ℝ) -
              HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
                (fderiv ℝ
                  (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x) :
            (a : ℂ) → ℂ)
          1 :
        ℂ)
hg :
  DifferentiableAt ℝ (E := ℝ) (F := ℂ) ((⇑ofRealCLM : (a : ℝ) → ℂ) : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) 1 : ℝ)
hf₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x
⊢ (fderiv ℝ (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x -
          HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
            (fderiv ℝ (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
              x) :
        (a : ℂ) → ℂ)
      I =
    HSMul.hSMul (β := ℂ) I
      ((fderiv ℝ (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x -
              HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
                (fderiv ℝ
                  (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x) :
            (a : ℂ) → ℂ)
          1 :
        ℂ)

Tactic:
rw [fderiv_comp]

Premises used: fderiv_comp
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (E := ℝ) (F := ℂ) ((⇑ofRealCLM : (a : ℝ) → ℂ) : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) 1 : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (E := ℝ) (F := ℂ) ((⇑ofRealCLM : (a : ℝ) → ℂ) : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) 1 : ℝ)

Tactic:
try fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x

Tactic:
try fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
rw :
  (ContinuousLinearMap.comp (M₂ := ℝ) (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) 1) : ℝ →L[ℝ] ℂ)
            (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : ℂ →L[ℝ] ℝ) -
          HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
            (ContinuousLinearMap.comp (M₂ := ℝ)
              (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) I) : ℝ →L[ℝ] ℂ)
              (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x : ℂ →L[ℝ] ℝ)) :
        (a : ℂ) → ℂ)
      I =
    HSMul.hSMul (β := ℂ) I
      ((ContinuousLinearMap.comp (M₂ := ℝ)
                (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) 1) : ℝ →L[ℝ] ℂ)
                (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : ℂ →L[ℝ] ℝ) -
              HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
                (ContinuousLinearMap.comp (M₂ := ℝ)
                  (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) I) : ℝ →L[ℝ] ℂ)
                  (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x : ℂ →L[ℝ] ℝ)) :
            (a : ℂ) → ℂ)
          1 :
        ℂ)
hg :
  DifferentiableAt ℝ (E := ℝ) (F := ℂ) ((⇑ofRealCLM : (a : ℝ) → ℂ) : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) I : ℝ)
hf₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x
⊢ (ContinuousLinearMap.comp (M₂ := ℝ) (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) 1) : ℝ →L[ℝ] ℂ)
            (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : ℂ →L[ℝ] ℝ) -
          HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
            (fderiv ℝ (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
              x) :
        (a : ℂ) → ℂ)
      I =
    HSMul.hSMul (β := ℂ) I
      ((ContinuousLinearMap.comp (M₂ := ℝ)
                (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) 1) : ℝ →L[ℝ] ℂ)
                (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : ℂ →L[ℝ] ℝ) -
              HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
                (fderiv ℝ
                  (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x) :
            (a : ℂ) → ℂ)
          1 :
        ℂ)

Tactic:
rw [fderiv_comp]

Premises used: fderiv_comp
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (E := ℝ) (F := ℂ) ((⇑ofRealCLM : (a : ℝ) → ℂ) : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) I : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (E := ℝ) (F := ℂ) ((⇑ofRealCLM : (a : ℝ) → ℂ) : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) I : ℝ)

Tactic:
try fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x

Tactic:
try fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
repeat :
  (ContinuousLinearMap.comp (M₂ := ℝ) (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) 1) : ℝ →L[ℝ] ℂ)
            (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : ℂ →L[ℝ] ℝ) -
          HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
            (ContinuousLinearMap.comp (M₂ := ℝ)
              (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) I) : ℝ →L[ℝ] ℂ)
              (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x : ℂ →L[ℝ] ℝ)) :
        (a : ℂ) → ℂ)
      I =
    HSMul.hSMul (β := ℂ) I
      ((ContinuousLinearMap.comp (M₂ := ℝ)
                (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) 1) : ℝ →L[ℝ] ℂ)
                (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : ℂ →L[ℝ] ℝ) -
              HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
                (ContinuousLinearMap.comp (M₂ := ℝ)
                  (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) I) : ℝ →L[ℝ] ℂ)
                  (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x : ℂ →L[ℝ] ℝ)) :
            (a : ℂ) → ℂ)
          1 :
        ℂ)
⊢ (fderiv ℝ (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x -
          HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
            (fderiv ℝ (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
              x) :
        (a : ℂ) → ℂ)
      I =
    HSMul.hSMul (β := ℂ) I
      ((fderiv ℝ (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x -
              HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
                (fderiv ℝ
                  (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x) :
            (a : ℂ) → ℂ)
          1 :
        ℂ)

Tactic:
repeat rw [fderiv_comp]; all_goals try fun_prop

Premises used: fderiv_comp
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
simp :
  (↑((fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : (a : ℂ) → ℝ) I) : ℂ) -
      I * (↑((fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x : (a : ℂ) → ℝ) I) : ℂ) =
    I * (↑((fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : (a : ℂ) → ℝ) 1) : ℂ) -
      I * (I * (↑((fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x : (a : ℂ) → ℝ) 1) : ℂ))
⊢ (ContinuousLinearMap.comp (M₂ := ℝ) (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) 1) : ℝ →L[ℝ] ℂ)
            (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : ℂ →L[ℝ] ℝ) -
          HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
            (ContinuousLinearMap.comp (M₂ := ℝ)
              (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) I) : ℝ →L[ℝ] ℂ)
              (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x : ℂ →L[ℝ] ℝ)) :
        (a : ℂ) → ℂ)
      I =
    HSMul.hSMul (β := ℂ) I
      ((ContinuousLinearMap.comp (M₂ := ℝ)
                (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) 1) : ℝ →L[ℝ] ℂ)
                (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : ℂ →L[ℝ] ℝ) -
              HSMul.hSMul (β := ℂ →L[ℝ] ℂ) I
                (ContinuousLinearMap.comp (M₂ := ℝ)
                  (fderiv ℝ (⇑ofRealCLM : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) I) : ℝ →L[ℝ] ℂ)
                  (fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x : ℂ →L[ℝ] ℝ)) :
            (a : ℂ) → ℂ)
          1 :
        ℂ)

Tactic:
simp only [ContinuousLinearMap.fderiv, ContinuousLinearMap.coe_sub',
    ContinuousLinearMap.coe_comp', ContinuousLinearMap.coe_smul', Pi.sub_apply,
    Function.comp_apply, ofRealCLM_apply, Pi.smul_apply, smul_eq_mul, mul_sub]

Premises used: ContinuousLinearMap.coe_comp', ContinuousLinearMap.coe_smul', mul_sub, ContinuousLinearMap.fderiv, Complex.ofRealCLM_apply, Function.comp_apply, ContinuousLinearMap.coe_sub', smul_eq_mul, Pi.sub_apply, Pi.smul_apply
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
ring_nf :
  (↑((fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : (a : ℂ) → ℝ) I) : ℂ) -
      I * (↑((fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x : (a : ℂ) → ℝ) I) : ℂ) =
    I * (↑((fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : (a : ℂ) → ℝ) 1) : ℂ) -
      HPow.hPow (β := ℕ) I 2 * (↑((fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x : (a : ℂ) → ℝ) 1) : ℂ)
⊢ (↑((fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : (a : ℂ) → ℝ) I) : ℂ) -
      I * (↑((fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x : (a : ℂ) → ℝ) I) : ℂ) =
    I * (↑((fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x : (a : ℂ) → ℝ) 1) : ℂ) -
      I * (I * (↑((fderiv ℝ (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x : (a : ℂ) → ℝ) 1) : ℂ))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
⊢ DifferentiableAt ℝ (F := ℂ →L[ℝ] ℝ) (fderiv ℝ f) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (F := ℂ) (fun (x : ℂ) ↦ 1) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
h₁f : ContDiffAt ℝ 2 f x
⊢ DifferentiableAt ℝ (F := ℂ) (fun (x : ℂ) ↦ I) x

Tactic:
fun_prop