awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
funProp : ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (closedBall 0 R) x → (↑q : ℂ) * x - W ≠ 0
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑q : ℂ) / ((↑q : ℂ) * z - W)) (closedBall 0 R)

Tactic:
fun_prop (disch := aesop)
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0

Tactic:
have h0 : ∮ (z : ℂ) in C(0, R), z⁻¹ • ((q * z) / (q * z - W)) • f z = 0 := calc
    ∮ (z : ℂ) in C(0, R), z⁻¹ • ((q * z) / (q * z - W)) • f z
    _ = ∮ (z : ℂ) in C(0, R), (q / (q * z - W)) • f z := by
      apply circleIntegral.integral_congr hR.le fun z hz ↦ ?_
      have hz : z ≠ 0 := by aesop
      match_scalars
      field
    _ = 0 := by
      apply DifferentiableOn.diffContOnCl ?_ |>.smul hf |>.circleIntegral_eq_zero hR.le
      rw [closure_ball 0 hR.ne']
      fun_prop (disch := aesop)
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
apply :
  ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) (sphere 0 |R|) z),
    ((z + w) / (z - w)).re • f z = (z / (z - w) - q • z / (q • z - W)) • f z
⊢ Eq.{u_1 + 1} (α := E) (Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R)
    (Real.circleAverage (fun (z : ℂ) ↦ (z / (z - w) - q • z / (q • z - W)) • f z) 0 R)

Tactic:
apply circleAverage_congr_sphere fun z hz ↦ ?_

Premises used: Real.circleAverage_congr_sphere
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |R|) z
⊢ ‖z‖ = R

Tactic:
simpa [abs_of_pos hR] using hz

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |R|) z
⊢ ‖z‖ = R

Tactic:
have hzR : ‖z‖ = R := by simpa [abs_of_pos hR] using hz
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |R|) z
hzR : ‖z‖ = R
match_scalars : HMul.hMul (α := ℂ) (↑((z + w) / (z - w)).re : ℂ) 1 = (z / (z - w) - q • z / (q • z - W)) * 1
⊢ ((z + w) / (z - w)).re • f z = (z / (z - w) - q • z / (q • z - W)) • f z

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |R|) z
hzR : ‖z‖ = R
simp :
  (↑((z + w) / (z - w)).re : ℂ) =
    z / (z - w) - (↑‖w‖ : ℂ) / (↑R : ℂ) * z / ((↑‖w‖ : ℂ) / (↑R : ℂ) * z - (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I))
⊢ HMul.hMul (α := ℂ) (↑((z + w) / (z - w)).re : ℂ) 1 = (z / (z - w) - q • z / (q • z - W)) * 1

Tactic:
simp only [q, W, real_smul, ofReal_div, coe_algebraMap, mul_one]

Premises used: Complex.real_smul, Complex.coe_algebraMap, Complex.ofReal_div, mul_one
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |R|) z
hzR : ‖z‖ = R
rw :
  (↑R : ℂ) * cexp ((↑z.arg : ℂ) * I) / ((↑R : ℂ) * cexp ((↑z.arg : ℂ) * I) - w) -
      (↑‖w‖ : ℂ) * cexp ((↑z.arg : ℂ) * I) /
        ((↑‖w‖ : ℂ) * cexp ((↑z.arg : ℂ) * I) - (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)) =
    (↑R : ℂ) * cexp ((↑z.arg : ℂ) * I) / ((↑R : ℂ) * cexp ((↑z.arg : ℂ) * I) - w) -
      (↑‖w‖ : ℂ) / (↑R : ℂ) * ((↑R : ℂ) * cexp ((↑z.arg : ℂ) * I)) /
        ((↑‖w‖ : ℂ) / (↑R : ℂ) * ((↑R : ℂ) * cexp ((↑z.arg : ℂ) * I)) - (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I))
⊢ (↑((z + w) / (z - w)).re : ℂ) =
    z / (z - w) - (↑‖w‖ : ℂ) / (↑R : ℂ) * z / ((↑‖w‖ : ℂ) / (↑R : ℂ) * z - (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I))

Tactic:
rw [← norm_mul_exp_arg_mul_I w, ← norm_mul_exp_arg_mul_I z, hzR,
        ← circleAverage_re_smul_on_ball_zero_aux, norm_mul_exp_arg_mul_I w]

Premises used: Complex.norm_mul_exp_arg_mul_I, _private.0.circleAverage_re_smul_on_ball_zero_aux
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |R|) z
hzR : ‖z‖ = R
⊢ (↑R : ℂ) * cexp ((↑z.arg : ℂ) * I) / ((↑R : ℂ) * cexp ((↑z.arg : ℂ) * I) - w) -
      (↑‖w‖ : ℂ) * cexp ((↑z.arg : ℂ) * I) /
        ((↑‖w‖ : ℂ) * cexp ((↑z.arg : ℂ) * I) - (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)) =
    (↑R : ℂ) * cexp ((↑z.arg : ℂ) * I) / ((↑R : ℂ) * cexp ((↑z.arg : ℂ) * I) - w) -
      (↑‖w‖ : ℂ) / (↑R : ℂ) * ((↑R : ℂ) * cexp ((↑z.arg : ℂ) * I)) /
        ((↑‖w‖ : ℂ) / (↑R : ℂ) * ((↑R : ℂ) * cexp ((↑z.arg : ℂ) * I)) - (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I))

Tactic:
field [hR.ne.symm]

Premises used: Ne.symm, LT.lt.ne
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
simp_rw :
  Real.circleAverage (fun (z : ℂ) ↦ (z / (z - w)) • f z - (q • z / (q • z - W)) • f z) 0 R =
    HSub.hSub (α := E) (Real.circleAverage (fun (z : ℂ) ↦ (z / (z - w)) • f z) 0 R)
      (Real.circleAverage (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) 0 R)
⊢ Real.circleAverage (fun (z : ℂ) ↦ (z / (z - w) - q • z / (q • z - W)) • f z) 0 R =
    HSub.hSub (α := E) (Real.circleAverage (fun (z : ℂ) ↦ (z / (z - w)) • f z) 0 R)
      (Real.circleAverage (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) 0 R)

Tactic:
simp_rw [sub_smul]

Premises used: sub_smul
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
⊢ ∀ (z : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 R) z → z - w ≠ 0

Tactic:
aesop (add simp sub_eq_zero)

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
⊢ ∀ (z : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 R) z → z - w ≠ 0

Tactic:
have h₁ : ∀ z ∈ sphere 0 R, z - w ≠ 0 := by aesop (add simp sub_eq_zero)
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
h₁ : ∀ (z : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 R) z → z - w ≠ 0
⊢ ContinuousOn f (sphere 0 R)

Tactic:
have h₃ : ContinuousOn f (sphere 0 R) :=
        hf.2.mono <| sphere_subset_closedBall.trans_eq (closure_ball 0 hR.ne').symm
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
h₁ : ∀ (z : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 R) z → z - w ≠ 0
h₃ : ContinuousOn f (sphere 0 R)
hf₁ : CircleIntegrable.{u_1} (E := E) (fun (z : ℂ) ↦ (z / (z - w)) • f z) 0 R
hf₂ : CircleIntegrable.{u_1} (E := E) (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) 0 R
⊢ Real.circleAverage (fun (z : ℂ) ↦ (z / (z - w)) • f z - (q • z / (q • z - W)) • f z) 0 R =
    HSub.hSub (α := E) (Real.circleAverage (fun (z : ℂ) ↦ (z / (z - w)) • f z) 0 R)
      (Real.circleAverage (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) 0 R)

Tactic:
rw [circleAverage_fun_sub]

Premises used: Real.circleAverage_fun_sub
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
h₁ : ∀ (z : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 R) z → z - w ≠ 0
h₃ : ContinuousOn f (sphere 0 R)
hf₁ : ContinuousOn.{0, u_1} (Y := E) (fun (z : ℂ) ↦ (z / (z - w)) • f z) (sphere 0 R)
⊢ CircleIntegrable.{u_1} (E := E) (fun (z : ℂ) ↦ (z / (z - w)) • f z) 0 R

Tactic:
apply ContinuousOn.circleIntegrable hR.le

Premises used: ContinuousOn.circleIntegrable, LT.lt.le
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
h₁ : ∀ (z : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 R) z → z - w ≠ 0
h₃ : ContinuousOn f (sphere 0 R)
funProp : ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 R) x → x - w ≠ 0
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (z : ℂ) ↦ (z / (z - w)) • f z) (sphere 0 R)

Tactic:
fun_prop (disch := aesop)
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
h₁ : ∀ (z : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 R) z → z - w ≠ 0
h₃ : ContinuousOn f (sphere 0 R)
hf₂ : ContinuousOn.{0, u_1} (Y := E) (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) (sphere 0 R)
⊢ CircleIntegrable.{u_1} (E := E) (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) 0 R

Tactic:
apply ContinuousOn.circleIntegrable hR.le

Premises used: ContinuousOn.circleIntegrable, LT.lt.le
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
h₁ : ∀ (z : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 R) z → z - w ≠ 0
h₃ : ContinuousOn f (sphere 0 R)
⊢ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 R) x → q • x - W ≠ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
h₁ : ∀ (z : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 R) z → z - w ≠ 0
h₃ : ContinuousOn f (sphere 0 R)
funProp : ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 R) x → q • x - W ≠ 0
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) (sphere 0 R)

Tactic:
fun_prop (disch := aesop)
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
rw :
  ∀ (hf : DiffContOnCl ℂ f (ball 0 |R|)) (hw : Membership.mem (γ := Set ℂ) (ball 0 |R|) w) (hR : 0 < R) (h₁w : w ≠ 0),
    let W := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I);
    let q := ‖w‖ / R;
    ∀ (h₁q : 0 < q) (h₂q : q < 1) (η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0)
      (h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0),
      HSub.hSub (α := E) (Real.circleAverage (fun (z : ℂ) ↦ (z / (z - w)) • f z) 0 R)
          (Real.circleAverage (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) 0 R) =
        f w
⊢ HSub.hSub (α := E) (Real.circleAverage (fun (z : ℂ) ↦ (z / (z - w)) • f z) 0 R)
      (Real.circleAverage (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) 0 R) =
    f w

Tactic:
rw [← abs_of_pos hR] at hw hf

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 |R|)
hw : Membership.mem (γ := Set ℂ) (ball 0 |R|) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
⊢ HSub.hSub (α := E) (Real.circleAverage (fun (z : ℂ) ↦ (z / (z - w)) • f z) 0 R)
      (Real.circleAverage (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) 0 R) =
    f w

Tactic:
simp [← hf.circleAverage_smul_div hw, circleAverage_eq_circleIntegral (ne_of_lt hR).symm, h0]

Premises used: Real.circleAverage_eq_circleIntegral, Ne.symm, DiffContOnCl.circleAverage_smul_div, ne_of_lt
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
h0 : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z) 0
calc :
  Eq.{u_1 + 1} (α := E) (Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R)
    (Real.circleAverage (fun (z : ℂ) ↦ (z / (z - w) - q • z / (q • z - W)) • f z) 0 R)
calc₁ :
  Real.circleAverage (fun (z : ℂ) ↦ (z / (z - w) - q • z / (q • z - W)) • f z) 0 R =
    HSub.hSub (α := E) (Real.circleAverage (fun (z : ℂ) ↦ (z / (z - w)) • f z) 0 R)
      (Real.circleAverage (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) 0 R)
calc₂ :
  HSub.hSub (α := E) (Real.circleAverage (fun (z : ℂ) ↦ (z / (z - w)) • f z) 0 R)
      (Real.circleAverage (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) 0 R) =
    f w
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R = f w

Tactic:
calc Real.circleAverage (fun z ↦ ((z + w) / (z - w)).re • f z) 0 R
    _ = Real.circleAverage (fun z ↦ (z / (z - w) - (q • z) / (q • z - W)) • f z) 0 R := by
      apply circleAverage_congr_sphere fun z hz ↦ ?_
      have hzR : ‖z‖ = R := by simpa [abs_of_pos hR] using hz
      match_scalars
      simp only [q, W, real_smul, ofReal_div, coe_algebraMap, mul_one]
      rw [← norm_mul_exp_arg_mul_I w, ← norm_mul_exp_arg_mul_I z, hzR,
        ← circleAverage_re_smul_on_ball_zero_aux, norm_mul_exp_arg_mul_I w]
      field [hR.ne.symm]
    _ = Real.circleAverage (fun z ↦ (z / (z - w)) • f z) 0 R
        - Real.circleAverage (fun z ↦ ((q • z) / (q • z - W)) • f z) 0 R := by
      simp_rw [sub_smul]
      have h₁ : ∀ z ∈ sphere 0 R, z - w ≠ 0 := by aesop (add simp sub_eq_zero)
      have h₃ : ContinuousOn f (sphere 0 R) :=
        hf.2.mono <| sphere_subset_closedBall.trans_eq (closure_ball 0 hR.ne').symm
      rw [circleAverage_fun_sub]
      all_goals
        apply ContinuousOn.circleIntegrable hR.le
        fun_prop (disch := aesop)
    _ = f w := by
      rw [← abs_of_pos hR] at hw hf
      simp [← hf.circleAverage_smul_div hw, circleAverage_eq_circleIntegral (ne_of_lt hR).symm, h0]

Premises used: HSub.hSub, HDiv.hDiv, Complex.re, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat, Real.circleAverage
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
inl : ∀ (hR : R ≤ 0), Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
inr : ∀ (hR : 0 < R), Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
⊢ Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
rcases le_or_gt R 0 with hR | hR

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : R ≤ 0
⊢ Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
simp_all [ball_eq_empty.2 hR]

Premises used: Iff.mpr, Metric.ball_eq_empty
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ z + c) (closure (ball 0 R))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
x : ℂ
⊢ Membership.mem (γ := Set ℂ) (ball 0 R) x → (fun (z : ℂ) ↦ z + c) x ∈ ball c R

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ DiffContOnCl.{0, 0, u_1} ℂ (F := E) (fun (z : ℂ) ↦ f (z + c)) (ball 0 R)

Tactic:
have h₁g : DiffContOnCl ℂ (fun z ↦ f (z + c)) (ball 0 R) :=
    hf.comp (DifferentiableOn.diffContOnCl <| by fun_prop) (by intro; aesop)
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
h₁g : DiffContOnCl.{0, 0, u_1} ℂ (F := E) (fun (z : ℂ) ↦ f (z + c)) (ball 0 R)
⊢ Membership.mem (γ := Set ℂ) (ball 0 R) (w - c)

Tactic:
simpa using mem_ball_iff_norm.1 hw

Premises used: mem_ball_iff_norm, Iff.mp
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst_2 : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
h₁g : DiffContOnCl.{0, 0, u_1} ℂ (F := E) (fun (z : ℂ) ↦ f (z + c)) (ball 0 R)
⊢ Membership.mem (γ := Set ℂ) (ball 0 R) (w - c)

Tactic:
have h₂g : w - c ∈ ball 0 R := by simpa using mem_ball_iff_norm.1 hw