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
⊢ (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 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 :
      ℂ)
Tactic: repeat rw [fderiv_comp]; all_goals 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
            (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 :
        ℂ)
have 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) : ℂ))
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]
-- 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 ℝ (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) : ℂ))
have 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) : ℂ)
Tactic: ring_nf
-- 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 := ℂ →L[ℝ] ℝ) (fderiv ℝ f) 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 ℝ (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) : ℂ)
have rw : (↑((HAdd.hAdd (α := ℂ →L[ℝ] ℝ) (fderiv ℝ f x ∘SL fderiv ℝ (fun (x : ℂ) ↦ 1) x)
              ((ContinuousLinearMap.flip (fderiv ℝ (fderiv ℝ f) x) : (a : ℂ) → ℂ →L[ℝ] ℝ) 1) :
            (a : ℂ) → ℝ)
          I) :
      ℂ) -
    I *
      (↑((HAdd.hAdd (α := ℂ →L[ℝ] ℝ) (β := ℂ →L[ℝ] ℝ) (fderiv ℝ f x ∘SL fderiv ℝ (fun (x : ℂ) ↦ I) x)
                ((ContinuousLinearMap.flip (fderiv ℝ (fderiv ℝ f) x) : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) :
              (a : ℂ) → ℝ)
            I) :
        ℂ) =
  I *
      (↑((HAdd.hAdd (α := ℂ →L[ℝ] ℝ) (fderiv ℝ f x ∘SL fderiv ℝ (fun (x : ℂ) ↦ 1) x)
                ((ContinuousLinearMap.flip (fderiv ℝ (fderiv ℝ f) x) : (a : ℂ) → ℂ →L[ℝ] ℝ) 1) :
              (a : ℂ) → ℝ)
            1) :
        ℂ) -
    HPow.hPow (β := ℕ) I 2 *
      (↑((HAdd.hAdd (α := ℂ →L[ℝ] ℝ) (β := ℂ →L[ℝ] ℝ) (fderiv ℝ f x ∘SL fderiv ℝ (fun (x : ℂ) ↦ I) x)
                ((ContinuousLinearMap.flip (fderiv ℝ (fderiv ℝ f) x) : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) :
              (a : ℂ) → ℝ)
            1) :
        ℂ)
Tactic: rw [fderiv_clm_apply (by fun_prop) (by fun_prop), fderiv_clm_apply (by fun_prop) (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
⊢ (↑((HAdd.hAdd (α := ℂ →L[ℝ] ℝ) (fderiv ℝ f x ∘SL fderiv ℝ (fun (x : ℂ) ↦ 1) x)
                ((ContinuousLinearMap.flip (fderiv ℝ (fderiv ℝ f) x) : (a : ℂ) → ℂ →L[ℝ] ℝ) 1) :
              (a : ℂ) → ℝ)
            I) :
        ℂ) -
      I *
        (↑((HAdd.hAdd (α := ℂ →L[ℝ] ℝ) (β := ℂ →L[ℝ] ℝ) (fderiv ℝ f x ∘SL fderiv ℝ (fun (x : ℂ) ↦ I) x)
                  ((ContinuousLinearMap.flip (fderiv ℝ (fderiv ℝ f) x) : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) :
                (a : ℂ) → ℝ)
              I) :
          ℂ) =
    I *
        (↑((HAdd.hAdd (α := ℂ →L[ℝ] ℝ) (fderiv ℝ f x ∘SL fderiv ℝ (fun (x : ℂ) ↦ 1) x)
                  ((ContinuousLinearMap.flip (fderiv ℝ (fderiv ℝ f) x) : (a : ℂ) → ℂ →L[ℝ] ℝ) 1) :
                (a : ℂ) → ℝ)
              1) :
          ℂ) -
      HPow.hPow (β := ℕ) I 2 *
        (↑((HAdd.hAdd (α := ℂ →L[ℝ] ℝ) (β := ℂ →L[ℝ] ℝ) (fderiv ℝ f x ∘SL fderiv ℝ (fun (x : ℂ) ↦ I) x)
                  ((ContinuousLinearMap.flip (fderiv ℝ (fderiv ℝ f) x) : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) :
                (a : ℂ) → ℝ)
              1) :
          ℂ)
have simp : (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) 1) : ℂ) -
    I * (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) I) : ℂ) =
  I * (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) 1) : ℂ) +
    (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) I) : ℂ)
Tactic: simp only [fderiv_fun_const, Pi.zero_apply, ContinuousLinearMap.comp_zero, zero_add,
    ContinuousLinearMap.flip_apply, I_sq, neg_mul, one_mul, sub_neg_eq_add]
-- 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 ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) 1) : ℂ) -
      I * (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) I) : ℂ) =
    I * (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) 1) : ℂ) +
      (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) I) : ℂ)
have rw : (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) 1) : ℂ) +
    -(I * (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) I) : ℂ)) =
  (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) I) : ℂ) +
    I * (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) 1) : ℂ)
Tactic: rw [add_comm, sub_eq_add_neg]
-- 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 ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) 1) : ℂ) +
      -(I * (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) I) : ℂ)) =
    (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) I) : ℂ) +
      I * (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) 1) : ℂ)
have e_a : (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) 1) : ℂ) =
  (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) I) : ℂ)
Tactic: congr 1
-- 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
e_a :
  (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) 1) : ℂ) =
    (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) I) : ℂ)
⊢ (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) 1) : ℂ) +
      -(I * (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) I) : ℂ)) =
    (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) I) : ℂ) +
      I * (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) 1) : ℂ)
have e_a₁ : -(I * (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) I) : ℂ)) =
  I * (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) 1) : ℂ)
Tactic: congr 1
-- 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 ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) 1) : ℂ) =
    (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) I) : ℂ)
have e_a : Eq (α := ℝ) ((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) 1 : ℝ)
  (((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) I : ℝ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (hypothesis)
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
⊢ -(I * (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) I) : ℂ)) =
    I * (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) 1) : ℂ)
have h₂f : Laplacian.laplacian f x = 0 x
Tactic: have h₂f := hf.2.eq_of_nhds
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (hypothesis)
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
h₂f : Laplacian.laplacian f x = 0 x
⊢ -(I * (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) I) : ℂ)) =
    I * (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) 1) : ℂ)
have h₂f₁ : Eq (α := ℝ) (((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) 1 : ℝ)
  (-(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) I : ℝ)
Tactic: simp only [laplacian_eq_iteratedFDeriv_complexPlane, iteratedFDeriv_two_apply, Fin.isValue,
      Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, Pi.zero_apply,
      add_eq_zero_iff_eq_neg] at h₂f
Cleared hypotheses: h₂f
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
Goal:
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)
have pos : ∀ (hR : R ≤ 0), ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)
Tactic: by_cases hR : R ≤ 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
Goal:
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
pos : ∀ (hR : R ≤ 0), ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)
have neg : ∀ (hR : ¬R ≤ 0), ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)
Tactic: by_cases hR : R ≤ 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (hypothesis)
Goal:
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ :=
  (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)
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)
have hg : DifferentiableOn ℂ g (ball z R)
Tactic: have hg : DifferentiableOn ℂ g (ball z R) :=
    fun x hx ↦ (HarmonicAt.differentiableAt_complex_partial (hf x hx)).differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
Goal:
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ :=
  (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)
hg : DifferentiableOn ℂ g (ball z R)
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)
have neg : ∀ (F : ℂ → ℂ) (hF : F z = (↑(f z) : ℂ) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x),
  ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)
Tactic: obtain ⟨F, hF⟩ := hg.isExactOn_ball.with_val_at z (f z)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (hypothesis)
Goal:
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ :=
  (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)
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = (↑(f z) : ℂ) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)
have h₁F : DifferentiableOn ℂ F (ball z R)
Tactic: have h₁F : DifferentiableOn ℂ F (ball z R) :=
    fun x hx ↦ (hF.2 x hx).differentiableAt.differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (hypothesis)
Goal:
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ :=
  (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)
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = (↑(f z) : ℂ) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)
have h₂F : DifferentiableOn ℝ F (ball z R)
Tactic: have h₂F : DifferentiableOn ℝ F (ball z R) := h₁F.restrictScalars (𝕜 := ℝ) (𝕜' := ℂ)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
Goal:
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ :=
  (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)
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = (↑(f z) : ℂ) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)
have right : EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)
Tactic: use F, h₁F.analyticOnNhd isOpen_ball
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
Goal:
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ :=
  (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)
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = (↑(f z) : ℂ) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
⊢ EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)
have right : EqOn ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) f (ball z R)
Tactic: rw [(by aesop : (fun z ↦ (F z).re) = Complex.reCLM ∘ F)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
Goal:
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ :=
  (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)
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = (↑(f z) : ℂ) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x
have right : DifferentiableOn ℝ (F := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) (ball z R)
Tactic: apply (convex_ball z R).eqOn_of_fderivWithin_eq (𝕜 := ℝ) (x := z)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
Goal:
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ :=
  (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)
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = (↑(f z) : ℂ) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
right : DifferentiableOn ℝ (F := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) (ball z R)
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x
have right₁ : DifferentiableOn ℝ f (ball z R)
Tactic: apply (convex_ball z R).eqOn_of_fderivWithin_eq (𝕜 := ℝ) (x := z)