awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h₄F : DifferentiableAt ℂ F y
⊢ DifferentiableAt ℝ F y

Tactic:
have h₅F := 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)
x : ℂ
hx : x ∈ ball z R
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
⊢ DifferentiableAt ℝ (F := ℝ) (⇑reCLM : (a : ℂ) → ℝ) (F y)

Tactic:
fun_prop
-- 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
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
right : Eq (α := ℂ →L[ℝ] ℝ) (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y)) (fderiv ℝ f y)
⊢ Eq (α := ℂ →L[ℝ] ℝ) (fderivWithin ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) (ball z R) y) (fderivWithin ℝ f (ball z R) y)

Tactic:
rw [fderivWithin_eq_fderiv (isOpen_ball.uniqueDiffWithinAt hy)
      (reCLM.differentiableAt.comp y h₅F), fderivWithin_eq_fderiv
      (isOpen_ball.uniqueDiffWithinAt hy) ((hf y hy).1.differentiableAt two_ne_zero), fderiv_comp y
      (by fun_prop) h₅F, ContinuousLinearMap.fderiv, h₄F.fderiv_restrictScalars (𝕜 := ℝ)]

Premises used: Real, ContDiffAt.differentiableAt, ContinuousLinearMap.fderiv, IsOpen.uniqueDiffWithinAt, fderivWithin_eq_fderiv, DifferentiableAt.fderiv_restrictScalars, ContinuousLinearMap.differentiableAt, two_ne_zero, Metric.isOpen_ball, fderiv_comp, And.left, Complex.reCLM, DifferentiableAt.comp
-- 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
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
right :
  ∀ (a : ℂ),
    Eq (α := ℝ) ((reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y) : (a : ℂ) → ℝ) a : ℝ)
      ((fderiv ℝ f y : (a : ℂ) → ℝ) a : ℝ)
⊢ Eq (α := ℂ →L[ℝ] ℝ) (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y)) (fderiv ℝ f y)

Tactic:
ext a
-- 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
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
a : ℂ
⊢ a = HSMul.hSMul (β := ℂ) a.re 1 + a.im • I

Tactic:
simp
-- 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
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
a : ℂ
right :
  Eq (α := ℝ) ((reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y) : (a : ℂ) → ℝ) a : ℝ)
    ((fderiv ℝ f y : (a : ℂ) → ℝ) (HSMul.hSMul (β := ℂ) a.re 1 + a.im • I) : ℝ)
⊢ Eq (α := ℝ) ((reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y) : (a : ℂ) → ℝ) a : ℝ)
    ((fderiv ℝ f y : (a : ℂ) → ℝ) a : ℝ)

Tactic:
nth_rw 2 [(by simp : a = a.re • (1 : ℂ) + a.im • (I : ℂ))]
-- 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
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
a : ℂ
right :
  (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y) : (a : ℂ) → ℝ) a =
    HSMul.hSMul (β := ℝ) a.re ((fderiv ℝ f y : (a : ℂ) → ℝ) 1 : ℝ) +
      HSMul.hSMul (β := ℝ) a.im ((fderiv ℝ f y : (a : ℂ) → ℝ) I : ℝ)
⊢ Eq (α := ℝ) ((reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y) : (a : ℂ) → ℝ) a : ℝ)
    ((fderiv ℝ f y : (a : ℂ) → ℝ) (HSMul.hSMul (β := ℂ) a.re 1 + a.im • I) : ℝ)

Tactic:
rw [map_add, map_smul, map_smul]

Premises used: map_add, map_smul
-- 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
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
a : ℂ
⊢ (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y) : (a : ℂ) → ℝ) a =
    HSMul.hSMul (β := ℝ) a.re ((fderiv ℝ f y : (a : ℂ) → ℝ) 1 : ℝ) +
      HSMul.hSMul (β := ℝ) a.im ((fderiv ℝ f y : (a : ℂ) → ℝ) I : ℝ)

Tactic:
simp [HasDerivAt.deriv (hF.2 y hy), g]

Premises used: HasDerivAt.deriv, And.right
-- 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
⊢ z ∈ ball z R

Tactic:
simp_all
-- 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
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) z = f z

Tactic:
simp_all
-- 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
⊢ x ∈ ball z R

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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)
⊢ Differentiable ℂ g

Tactic:
have hg : Differentiable ℂ g :=
    fun x ↦ (HarmonicAt.differentiableAt_complex_partial (hf x (mem_univ x)))
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
obtain :
  ∀ (F : ℂ → ℂ) (hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x),
    ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F univ ∧ (fun (z : ℂ) ↦ (F z).re) = f
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F univ ∧ (fun (z : ℂ) ↦ (F z).re) = f

Tactic:
obtain ⟨F, hF⟩ := hg.isExactOn_univ.with_val_at 0 (f 0)

Premises used: Differentiable.isExactOn_univ, Complex.ofReal, Complex.IsExactOn.with_val_at, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
⊢ ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
⊢ ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁

Tactic:
have h₁F : ∀ z₁, HasDerivAt F (g z₁) z₁ := by simp_all
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
⊢ Differentiable ℂ F

Tactic:
have h₂F : Differentiable ℂ F := fun x ↦ (h₁F x).differentiableAt
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
⊢ Differentiable ℝ F

Tactic:
have h₃F : Differentiable ℝ F := h₂F.restrictScalars (𝕜 := ℝ)
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
right : (fun (z : ℂ) ↦ (F z).re) = f
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F univ ∧ (fun (z : ℂ) ↦ (F z).re) = f

Tactic:
use F, (h₂F.differentiableOn).analyticOnNhd isOpen_univ

Premises used: isOpen_univ, Differentiable.differentiableOn, DifferentiableOn.analyticOnNhd
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
right : ∀ (x : ℂ), (F x).re = f x
⊢ (fun (z : ℂ) ↦ (F z).re) = f

Tactic:
ext x
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x : ℂ
right : ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x
⊢ (F x).re = f x

Tactic:
rw [← Complex.reCLM_apply, ← Function.comp_apply (f := reCLM)]

Premises used: Function.comp_apply, Complex.reCLM_apply
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x : ℂ
⊢ DifferentiableOn ℝ (F := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) univ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x : ℂ
refine : DifferentiableOn ℝ f univ
right : UniqueDiffOn ℝ (E := ℂ) univ
refine₁ : EqOn (β := ℂ →L[ℝ] ℝ) (fderivWithin ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) univ) (fderivWithin ℝ f univ) univ
right₁ : Membership.mem (γ := Set ℂ) univ 0
right₂ : ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) 0 = f 0
right₃ : Membership.mem (γ := Set ℂ) univ x
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x

Tactic:
refine (convex_univ).eqOn_of_fderivWithin_eq (𝕜 := ℝ) (x := 0) (by fun_prop) ?hd ?_ ?heq ?_ ?_ ?_

Premises used: convex_univ, Convex.eqOn_of_fderivWithin_eq
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x : ℂ
⊢ DifferentiableOn ℝ f univ

Tactic:
hf.contDiffOn.differentiableOn two_ne_zero

Premises used: ContDiffOn.differentiableOn, InnerProductSpace.HarmonicOnNhd.contDiffOn, two_ne_zero
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x : ℂ
⊢ DifferentiableOn ℝ f univ

Tactic:
exact hf.contDiffOn.differentiableOn two_ne_zero

Premises used: ContDiffOn.differentiableOn, InnerProductSpace.HarmonicOnNhd.contDiffOn, two_ne_zero
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x : ℂ
⊢ DifferentiableOn ℝ f univ

Tactic:
case hd => exact hf.contDiffOn.differentiableOn two_ne_zero

Premises used: ContDiffOn.differentiableOn, InnerProductSpace.HarmonicOnNhd.contDiffOn, two_ne_zero
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x y : ℂ
hy : Membership.mem (γ := Set ℂ) univ y
simp : Eq (α := ℂ →L[ℝ] ℝ) (fderiv ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) y) (fderiv ℝ f y)
⊢ Eq (α := ℂ →L[ℝ] ℝ) (fderivWithin ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) univ y) (fderivWithin ℝ f univ y)

Tactic:
simp only [fderivWithin_univ]

Premises used: fderivWithin_univ
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x y : ℂ
hy : Membership.mem (γ := Set ℂ) univ y
⊢ DifferentiableAt ℝ (F := ℝ) (⇑reCLM : (a : ℂ) → ℝ) (F y)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x y : ℂ
hy : Membership.mem (γ := Set ℂ) univ y
⊢ DifferentiableAt ℝ F y

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x y : ℂ
hy : Membership.mem (γ := Set ℂ) univ y
rw : Eq (α := ℂ →L[ℝ] ℝ) (fderiv ℝ (⇑reCLM : (a : ℂ) → ℝ) (F y) ∘SL fderiv ℝ F y) (fderiv ℝ f y)
⊢ Eq (α := ℂ →L[ℝ] ℝ) (fderiv ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) y) (fderiv ℝ f y)

Tactic:
rw [fderiv_comp y (by fun_prop) (by fun_prop)]

Premises used: fderiv_comp
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
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 : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x y : ℂ
hy : Membership.mem (γ := Set ℂ) univ y
h :
  ∀ (x : ℂ),
    Eq (α := ℝ) ((fderiv ℝ (⇑reCLM : (a : ℂ) → ℝ) (F y) ∘SL fderiv ℝ F y : (a : ℂ) → ℝ) x : ℝ)
      ((fderiv ℝ f y : (a : ℂ) → ℝ) x : ℝ)
⊢ Eq (α := ℂ →L[ℝ] ℝ) (fderiv ℝ (⇑reCLM : (a : ℂ) → ℝ) (F y) ∘SL fderiv ℝ F y) (fderiv ℝ f y)

Tactic:
ext x