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
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) :
          ℂ)
⊢ (↑((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:
rw [fderiv_clm_apply (by fun_prop) (by fun_prop), fderiv_clm_apply (by fun_prop) (by fun_prop)]

Premises used: fderiv_clm_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
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) : ℂ)
⊢ (↑((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:
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]

Premises used: ContinuousLinearMap.flip_apply, Pi.zero_apply, zero_add, ContinuousLinearMap.comp_zero, Complex.I_sq, neg_mul, fderiv_fun_const, one_mul, sub_neg_eq_add
-- 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 ℝ (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) : ℂ)
⊢ (↑((((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:
rw [add_comm, sub_eq_add_neg]

Premises used: sub_eq_add_neg, add_comm
-- 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
e_a :
  (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) 1) : ℂ) =
    (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) I) : ℂ)
e_a₁ :
  -(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[ℝ] ℝ) 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:
congr 1
-- 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
e_a :
  Eq (α := ℝ) ((((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) : ℂ) =
    (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) I) : ℂ)

Tactic:
norm_cast
-- 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
⊢ minSmoothness ℝ 2 ≤ 2

Tactic:
simp
-- 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
⊢ Eq (α := ℝ) ((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) 1 : ℝ)
    (((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) I : ℝ)

Tactic:
apply h₁f.isSymmSndFDerivAt (by simp)

Premises used: ContDiffAt.isSymmSndFDerivAt
-- 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
⊢ Laplacian.laplacian f x = 0 x

Tactic:
have h₂f := hf.2.eq_of_nhds
-- 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
h₂f : Laplacian.laplacian f x = 0 x
⊢ 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

Premises used: Matrix.cons_val_one, Matrix.cons_val_zero, Pi.zero_apply, add_eq_zero_iff_eq_neg, Matrix.cons_val_fin_one, Fin.isValue, InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane, iteratedFDeriv_two_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
h₂f :
  Eq (α := ℝ) (((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) 1 : ℝ)
    (-(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) I : ℝ)
⊢ -(I * (↑((((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) I : ℂ →L[ℝ] ℝ) : (a : ℂ) → ℝ) I) : ℂ)) =
    I * (↑(((fderiv ℝ (fderiv ℝ f) x : (a : ℂ) → ℂ →L[ℝ] ℝ) 1 : (a : ℂ) → ℝ) 1) : ℂ)

Tactic:
simp [h₂f]
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) x

Tactic:
DifferentiableOn.analyticAt (s := { x | HarmonicAt f x })
    (fun _ hy ↦ (HarmonicAt.differentiableAt_complex_partial hy).differentiableWithinAt)
    ((isOpen_setOf_harmonicAt f).mem_nhds hf)

Premises used: DifferentiableAt.differentiableWithinAt, HarmonicAt.differentiableAt_complex_partial, IsOpen.mem_nhds, InnerProductSpace.isOpen_setOf_harmonicAt, DifferentiableOn.analyticAt
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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)
neg : ∀ (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)

Tactic:
by_cases hR : R ≤ 0
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : R ≤ 0
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F (ball z R) ∧ EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)

Tactic:
simp [ball_eq_empty.2 hR]

Premises used: Iff.mpr, Metric.ball_eq_empty
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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)
⊢ DifferentiableOn ℂ g (ball z R)

Tactic:
have hg : DifferentiableOn ℂ g (ball z R) :=
    fun x hx ↦ (HarmonicAt.differentiableAt_complex_partial (hf x hx)).differentiableWithinAt
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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)
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)
⊢ ∃ (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)

Premises used: Complex.ofReal, DifferentiableOn.isExactOn_ball, Complex.IsExactOn.with_val_at
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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
⊢ DifferentiableOn ℂ F (ball z R)

Tactic:
have h₁F : DifferentiableOn ℂ F (ball z R) :=
    fun x hx ↦ (hF.2 x hx).differentiableAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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)
⊢ DifferentiableOn ℝ F (ball z R)

Tactic:
have h₂F : DifferentiableOn ℝ F (ball z R) := h₁F.restrictScalars (𝕜 := ℝ) (𝕜' := ℂ)
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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)
right : 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)

Tactic:
use F, h₁F.analyticOnNhd isOpen_ball

Premises used: Metric.isOpen_ball, DifferentiableOn.analyticOnNhd
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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)
⊢ Eq (α := (z : ℂ) → ℝ) (fun (z : ℂ) ↦ (F z).re) ((⇑reCLM : (a : ℂ) → ℝ) ∘ F)

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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)
right : EqOn ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) f (ball z R)
⊢ EqOn (fun (z : ℂ) ↦ (F z).re) f (ball z R)

Tactic:
rw [(by aesop : (fun z ↦ (F z).re) = Complex.reCLM ∘ F)]
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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)
right₁ : DifferentiableOn ℝ f (ball z R)
right₂ : UniqueDiffOn ℝ (ball z R)
right₃ :
  EqOn (β := ℂ →L[ℝ] ℝ) (fderivWithin ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) (ball z R)) (fderivWithin ℝ f (ball z R))
    (ball z R)
right₄ : z ∈ ball z R
right₅ : ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) z = f z
right₆ : x ∈ ball z R
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x

Tactic:
apply (convex_ball z R).eqOn_of_fderivWithin_eq (𝕜 := ℝ) (x := z)

Premises used: convex_ball, Convex.eqOn_of_fderivWithin_eq
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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
⊢ DifferentiableOn ℝ (F := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) (ball z R)

Tactic:
reCLM.differentiable.comp_differentiableOn h₂F

Premises used: Differentiable.comp_differentiableOn, ContinuousLinearMap.differentiable, Complex.reCLM
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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
⊢ DifferentiableOn ℝ (F := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) (ball z R)

Tactic:
exact reCLM.differentiable.comp_differentiableOn h₂F

Premises used: Differentiable.comp_differentiableOn, ContinuousLinearMap.differentiable, Complex.reCLM
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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
⊢ DifferentiableOn ℝ f (ball z R)

Tactic:
fun y hy ↦ (ContDiffAt.differentiableAt (hf y hy).1 two_ne_zero).differentiableWithinAt

Premises used: ContDiffAt.differentiableAt, DifferentiableAt.differentiableWithinAt, two_ne_zero, And.left, DifferentiableOn
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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
⊢ DifferentiableOn ℝ f (ball z R)

Tactic:
exact fun y hy ↦ (ContDiffAt.differentiableAt (hf y hy).1 two_ne_zero).differentiableWithinAt

Premises used: ContDiffAt.differentiableAt, DifferentiableAt.differentiableWithinAt, two_ne_zero, And.left
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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
⊢ UniqueDiffOn ℝ (ball z R)

Tactic:
isOpen_ball.uniqueDiffOn

Premises used: Metric.isOpen_ball, IsOpen.uniqueDiffOn
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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
⊢ UniqueDiffOn ℝ (ball z R)

Tactic:
exact isOpen_ball.uniqueDiffOn

Premises used: Metric.isOpen_ball, IsOpen.uniqueDiffOn
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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
y : ℂ
hy : y ∈ ball z R
⊢ DifferentiableAt ℂ F y

Tactic:
have h₄F := (hF.2 y hy).differentiableAt