awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
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
⊢ 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)
have 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)
Tactic: simp_rw [sub_smul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (hypothesis)
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
⊢ 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)
have h₁ : ∀ (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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (hypothesis)
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
⊢ 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)
have h₃ : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
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)
⊢ 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)
have hf₁ : CircleIntegrable.{u_1} (E := E) (fun (z : ℂ) ↦ (z / (z - w)) • f z) 0 R
Tactic: rw [circleAverage_fun_sub]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
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
⊢ 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)
have hf₂ : CircleIntegrable.{u_1} (E := E) (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) 0 R
Tactic: rw [circleAverage_fun_sub]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
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)
⊢ CircleIntegrable.{u_1} (E := E) (fun (z : ℂ) ↦ (z / (z - w)) • f z) 0 R
have hf₁ : ContinuousOn.{0, u_1} (Y := E) (fun (z : ℂ) ↦ (z / (z - w)) • f z) (sphere 0 R)
Tactic: apply ContinuousOn.circleIntegrable hR.le
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
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)
⊢ CircleIntegrable.{u_1} (E := E) (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) 0 R
have hf₂ : ContinuousOn.{0, u_1} (Y := E) (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) (sphere 0 R)
Tactic: apply ContinuousOn.circleIntegrable hR.le
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
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)
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (z : ℂ) ↦ (q • z / (q • z - W)) • f z) (sphere 0 R)
have funProp : ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (sphere 0 R) x → q • x - W ≠ 0
Tactic: fun_prop (disch := aesop)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
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
have 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
Tactic: rw [← abs_of_pos hR] at hw hf
Cleared hypotheses: hf, hw, hR, h₁w, W, q, h₁q, h₂q, η₀, h0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
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
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
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)
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
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)
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
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
⊢ Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
have inl : ∀ (hR : R ≤ 0), Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
Tactic: rcases le_or_gt R 0 with hR | hR
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
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
⊢ Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
have inr : ∀ (hR : 0 < R), Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
Tactic: rcases le_or_gt R 0 with hR | hR
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (hypothesis)
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
⊢ Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
have h₁g : 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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (hypothesis)
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)
⊢ Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
have h₂g : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
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
⊢ Real.circleAverage (poissonKernel c w • f) c R = f w
have simp_rw : Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
Tactic: simp_rw [poissonKernel_eq_re_herglotzRieszKernel]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
f : ℂ[X]
hf : 0 < f.degree
⊢ ∃ (z : ℂ), f.IsRoot z
have by_contra! : ∀ (hf' : ∀ (z : ℂ), ¬f.IsRoot z), False
Tactic: by_contra! hf'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (hypothesis)
Goal:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
⊢ False
have this : ∀ (z : ℂ), (eval z f)⁻¹ = 0
Tactic: have (z : ℂ) : (f.eval z)⁻¹ = 0 :=
    (f.differentiable.inv hf').apply_eq_of_tendsto_cocompact z <|
      Metric.cobounded_eq_cocompact (α := ℂ) ▸ (Filter.tendsto_inv₀_cobounded.comp <| by
        simpa only [tendsto_norm_atTop_iff_cobounded]
          using f.tendsto_norm_atTop hf tendsto_norm_cobounded_atTop)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (hypothesis)
Goal:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
this : ∀ (z : ℂ), (eval z f)⁻¹ = 0
⊢ False
have hf₁ : 0 < degree (R := ℂ) ((C : (a : ℂ) → ℂ[X]) 0)
Tactic: obtain rfl : f = C 0 := Polynomial.funext fun z ↦ inv_injective <| by simp [this]
Cleared hypotheses: f, hf, hf', this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (hypothesis)
Goal:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
this : ∀ (z : ℂ), (eval z f)⁻¹ = 0
hf₁ : 0 < degree (R := ℂ) ((C : (a : ℂ) → ℂ[X]) 0)
⊢ False
have hf'₁ : ∀ (z : ℂ), ¬IsRoot ((C : (a : ℂ) → ℂ[X]) 0) z
Tactic: obtain rfl : f = C 0 := Polynomial.funext fun z ↦ inv_injective <| by simp [this]
Cleared hypotheses: f, hf, hf', this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (hypothesis)
Goal:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
this : ∀ (z : ℂ), (eval z f)⁻¹ = 0
hf₁ : 0 < degree (R := ℂ) ((C : (a : ℂ) → ℂ[X]) 0)
hf'₁ : ∀ (z : ℂ), ¬IsRoot ((C : (a : ℂ) → ℂ[X]) 0) z
⊢ False
have this₁ : ∀ (z : ℂ), (eval z ((C : (a : ℂ) → ℂ[X]) 0))⁻¹ = 0
Tactic: obtain rfl : f = C 0 := Polynomial.funext fun z ↦ inv_injective <| by simp [this]
Cleared hypotheses: f, hf, hf', this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
have pos : ∀ (hp : p = 0),
  (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
pos :
  ∀ (hp : p = 0),
    (p.rootSet ℂ).toFinset.card =
      (p.rootSet ℝ).toFinset.card +
        Finset.card (α := (↑(p.rootSet ℂ) : Type))
          (Equiv.Perm.support
            ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
              ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
have neg : ∀ (hp : ¬p = 0),
  (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : p = 0
⊢ IsEmpty (↑(p.rootSet ℂ) : Type)
have rw : IsEmpty (↑∅ : Type)
Tactic: rw [hp, rootSet_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (hypothesis)
Goal:
p : ℚ[X]
hp : p = 0
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
have this : IsEmpty (↑(p.rootSet ℂ) : Type)
Tactic: haveI : IsEmpty (p.rootSet ℂ) := by rw [hp, rootSet_zero]; infer_instance
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : p = 0
this : IsEmpty (↑(p.rootSet ℂ) : Type)
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
have pos : (p.rootSet ℂ).toFinset.card = (p.rootSet ℝ).toFinset.card + Finset.card (α := (↑(p.rootSet ℂ) : Type)) ∅
Tactic: simp_rw [(galActionHom p ℂ _).support.eq_empty_of_isEmpty, hp, rootSet_zero,
      Set.toFinset_empty, Finset.card_empty]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Polynomial.Basic (goal)
Goal:
p : ℚ[X]
hp : p = 0
this : IsEmpty (↑(p.rootSet ℂ) : Type)
pos : (p.rootSet ℂ).toFinset.card = (p.rootSet ℝ).toFinset.card + Finset.card (α := (↑(p.rootSet ℂ) : Type)) ∅
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card +
      Finset.card (α := (↑(p.rootSet ℂ) : Type))
        (Equiv.Perm.support
          ((galActionHom p ℂ : (a : p.Gal) → Equiv.Perm (↑(p.rootSet ℂ) : Type))
            ((restrict p ℂ : (a : Gal(ℂ/ℚ)) → p.Gal) (AlgEquiv.restrictScalars ℚ conjAe) : p.Gal)))
have pos₁ : (rootSet (T := ℚ) 0 ℂ).toFinset.card =
  (rootSet (T := ℚ) 0 ℝ).toFinset.card + Finset.card (α := (↑(p.rootSet ℂ) : Type)) ∅
Tactic: simp_rw [(galActionHom p ℂ _).support.eq_empty_of_isEmpty, hp, rootSet_zero,
      Set.toFinset_empty, Finset.card_empty]