awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 ℝ
    ((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
have funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 ℂ
    ((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
have 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 :
      ℂ)
Tactic: refine differentiableAt_complex_iff_differentiableAt_real.2 ⟨by fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 := ℂ)
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x
have funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 ℝ
    (HSMul.hSMul (β := ℂ → ℂ) I
      (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I))
    x
have funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 := ℂ)
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x
have funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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
⊢ (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 :
        ℂ)
have 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 :
      ℂ)
Tactic: rw [fderiv_sub (by fun_prop) (by fun_prop), fderiv_const_smul (by fun_prop)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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
⊢ (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 :
        ℂ)
have 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 :
      ℂ)
Tactic: rw [fderiv_comp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 :
        ℂ)
⊢ (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 :
        ℂ)
have hg : DifferentiableAt ℝ (E := ℝ) (F := ℂ) ((⇑ofRealCLM : (a : ℝ) → ℂ) : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) 1 : ℝ)
Tactic: rw [fderiv_comp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 : ℝ)
⊢ (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 :
        ℂ)
have hf₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x
Tactic: rw [fderiv_comp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x
have funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) x
have funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
Tactic: try fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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
⊢ (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 :
        ℂ)
have 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 :
      ℂ)
Tactic: rw [fderiv_comp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 :
        ℂ)
⊢ (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 :
        ℂ)
have hg : DifferentiableAt ℝ (E := ℝ) (F := ℂ) ((⇑ofRealCLM : (a : ℝ) → ℂ) : (a : ℝ) → ℂ) ((fderiv ℝ f x : (a : ℂ) → ℝ) I : ℝ)
Tactic: rw [fderiv_comp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 : ℝ)
⊢ (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 :
        ℂ)
have hf₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x
Tactic: rw [fderiv_comp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x
have funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I) x
have funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
Tactic: try fun_prop