awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
right₁ : DifferentiableOn ℝ f (ball z R)
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x
have right₂ : UniqueDiffOn ℝ (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)
right₁ : DifferentiableOn ℝ f (ball z R)
right₂ : UniqueDiffOn ℝ (ball z R)
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x
have right₃ : EqOn (β := ℂ →L[ℝ] ℝ) (fderivWithin ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) (ball z R)) (fderivWithin ℝ f (ball z R)) (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)
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)
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x
have right₄ : z ∈ 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)
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
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x
have right₅ : ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) z = f z
Tactic: apply (convex_ball z R).eqOn_of_fderivWithin_eq (𝕜 := ℝ) (x := 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
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
⊢ Eq (α := ℂ →L[ℝ] ℝ) (fderivWithin ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) (ball z R) y) (fderivWithin ℝ f (ball z R) y)
have h₄F : DifferentiableAt ℂ F y
Tactic: have h₄F := (hF.2 y hy).differentiableAt
-- 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)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
⊢ Eq (α := ℂ →L[ℝ] ℝ) (fderivWithin ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) (ball z R) y) (fderivWithin ℝ f (ball z R) y)
have h₅F : DifferentiableAt ℝ F y
Tactic: have h₅F := 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)
x : ℂ
hx : x ∈ ball z R
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
⊢ Eq (α := ℂ →L[ℝ] ℝ) (fderivWithin ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) (ball z R) y) (fderivWithin ℝ f (ball z R) y)
have right : Eq (α := ℂ →L[ℝ] ℝ) (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y)) (fderiv ℝ f 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 (𝕜 := ℝ)]
-- 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
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
⊢ Eq (α := ℂ →L[ℝ] ℝ) (reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y)) (fderiv ℝ f y)
have right : ∀ (a : ℂ),
  Eq (α := ℝ) ((reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y) : (a : ℂ) → ℝ) a : ℝ)
    ((fderiv ℝ f y : (a : ℂ) → ℝ) a : ℝ)
Tactic: ext a
-- 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
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
a : ℂ
⊢ Eq (α := ℝ) ((reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y) : (a : ℂ) → ℝ) a : ℝ)
    ((fderiv ℝ f y : (a : ℂ) → ℝ) a : ℝ)
have right : Eq (α := ℝ) ((reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y) : (a : ℂ) → ℝ) a : ℝ)
  ((fderiv ℝ f y : (a : ℂ) → ℝ) (HSMul.hSMul (β := ℂ) a.re 1 + a.im • I) : ℝ)
Tactic: nth_rw 2 [(by simp : a = a.re • (1 : ℂ) + a.im • (I : ℂ))]
-- 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
y : ℂ
hy : y ∈ ball z R
h₄F : DifferentiableAt ℂ F y
h₅F : DifferentiableAt ℝ F y
a : ℂ
⊢ Eq (α := ℝ) ((reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ F y) : (a : ℂ) → ℝ) a : ℝ)
    ((fderiv ℝ f y : (a : ℂ) → ℝ) (HSMul.hSMul (β := ℂ) a.re 1 + a.im • I) : ℝ)
have 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 : ℝ)
Tactic: rw [map_add, map_smul, map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (hypothesis)
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)
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F univ ∧ (fun (z : ℂ) ↦ (F z).re) = f
have hg : Differentiable ℂ g
Tactic: have hg : Differentiable ℂ g :=
    fun x ↦ (HarmonicAt.differentiableAt_complex_partial (hf x (mem_univ x)))
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 : ℂ → ℂ), AnalyticOnNhd ℂ F univ ∧ (fun (z : ℂ) ↦ (F z).re) = f
have 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
Tactic: obtain ⟨F, hF⟩ := hg.isExactOn_univ.with_val_at 0 (f 0)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (hypothesis)
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
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F univ ∧ (fun (z : ℂ) ↦ (F z).re) = f
have h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
Tactic: have h₁F : ∀ z₁, HasDerivAt F (g z₁) z₁ := by simp_all
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (hypothesis)
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₁
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F univ ∧ (fun (z : ℂ) ↦ (F z).re) = f
have h₂F : Differentiable ℂ F
Tactic: have h₂F : Differentiable ℂ F := fun x ↦ (h₁F x).differentiableAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (hypothesis)
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
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F univ ∧ (fun (z : ℂ) ↦ (F z).re) = f
have h₃F : Differentiable ℝ F
Tactic: have h₃F : Differentiable ℝ F := h₂F.restrictScalars (𝕜 := ℝ)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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
⊢ ∃ (F : ℂ → ℂ), AnalyticOnNhd ℂ F univ ∧ (fun (z : ℂ) ↦ (F z).re) = f
have right : (fun (z : ℂ) ↦ (F z).re) = f
Tactic: use F, (h₂F.differentiableOn).analyticOnNhd isOpen_univ
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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
⊢ (fun (z : ℂ) ↦ (F z).re) = f
have right : ∀ (x : ℂ), (F x).re = f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 : ℂ
⊢ (F x).re = f x
have right : ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x
Tactic: rw [← Complex.reCLM_apply, ← Function.comp_apply (f := reCLM)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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 : ℂ
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x
have refine : DifferentiableOn ℝ f univ
Tactic: refine (convex_univ).eqOn_of_fderivWithin_eq (𝕜 := ℝ) (x := 0) (by fun_prop) ?hd ?_ ?heq ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x
have right : UniqueDiffOn ℝ (E := ℂ) univ
Tactic: refine (convex_univ).eqOn_of_fderivWithin_eq (𝕜 := ℝ) (x := 0) (by fun_prop) ?hd ?_ ?heq ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x
have refine₁ : EqOn (β := ℂ →L[ℝ] ℝ) (fderivWithin ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) univ) (fderivWithin ℝ f univ) univ
Tactic: refine (convex_univ).eqOn_of_fderivWithin_eq (𝕜 := ℝ) (x := 0) (by fun_prop) ?hd ?_ ?heq ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x
have right₁ : Membership.mem (γ := Set ℂ) univ 0
Tactic: refine (convex_univ).eqOn_of_fderivWithin_eq (𝕜 := ℝ) (x := 0) (by fun_prop) ?hd ?_ ?heq ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x
have right₂ : ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) 0 = f 0
Tactic: refine (convex_univ).eqOn_of_fderivWithin_eq (𝕜 := ℝ) (x := 0) (by fun_prop) ?hd ?_ ?heq ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) x = f x
have right₃ : Membership.mem (γ := Set ℂ) univ x
Tactic: refine (convex_univ).eqOn_of_fderivWithin_eq (𝕜 := ℝ) (x := 0) (by fun_prop) ?hd ?_ ?heq ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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
⊢ Eq (α := ℂ →L[ℝ] ℝ) (fderivWithin ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) univ y) (fderivWithin ℝ f univ y)
have simp : Eq (α := ℂ →L[ℝ] ℝ) (fderiv ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) y) (fderiv ℝ f y)
Tactic: simp only [fderivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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
⊢ Eq (α := ℂ →L[ℝ] ℝ) (fderiv ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) y) (fderiv ℝ f y)
have rw : Eq (α := ℂ →L[ℝ] ℝ) (fderiv ℝ (⇑reCLM : (a : ℂ) → ℝ) (F y) ∘SL fderiv ℝ F y) (fderiv ℝ f y)
Tactic: rw [fderiv_comp y (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
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
⊢ Eq (α := ℂ →L[ℝ] ℝ) (fderiv ℝ (⇑reCLM : (a : ℂ) → ℝ) (F y) ∘SL fderiv ℝ F y) (fderiv ℝ f y)
have h : ∀ (x : ℂ),
  Eq (α := ℝ) ((fderiv ℝ (⇑reCLM : (a : ℂ) → ℝ) (F y) ∘SL fderiv ℝ F y : (a : ℂ) → ℝ) x : ℝ)
    ((fderiv ℝ f y : (a : ℂ) → ℝ) x : ℝ)
Tactic: ext x