awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 1 / (R + r) ≤ (R + r) / HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2
have rw : 1 *
    (HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I)‖ 2 + HPow.hPow (β := ℕ) ‖(↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2 -
      2 *
        (HMul.hMul (β := ℂ) ((↑R : ℂ) * cexp ((↑θ : ℂ) * I))
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑r : ℂ) * cexp ((↑φ : ℂ) * I)) : ℂ)).re) ≤
  (R + r) * (R + r)
Tactic: rw [div_le_div_iff₀ (by positivity [h₁.trans h₂]) ?hpos, ← normSq_eq_norm_sq, normSq_sub,
    normSq_eq_norm_sq, normSq_eq_norm_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
rw :
  1 *
      (HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I)‖ 2 + HPow.hPow (β := ℕ) ‖(↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2 -
        2 *
          (HMul.hMul (β := ℂ) ((↑R : ℂ) * cexp ((↑θ : ℂ) * I))
              ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑r : ℂ) * cexp ((↑φ : ℂ) * I)) : ℂ)).re) ≤
    (R + r) * (R + r)
⊢ 1 / (R + r) ≤ (R + r) / HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2
have rw₁ : 0 < HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2
Tactic: rw [div_le_div_iff₀ (by positivity [h₁.trans h₂]) ?hpos, ← normSq_eq_norm_sq, normSq_sub,
    normSq_eq_norm_sq, normSq_eq_norm_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (hypothesis)
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 1 *
      (HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I)‖ 2 + HPow.hPow (β := ℕ) ‖(↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2 -
        2 *
          (HMul.hMul (β := ℂ) ((↑R : ℂ) * cexp ((↑θ : ℂ) * I))
              ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑r : ℂ) * cexp ((↑φ : ℂ) * I)) : ℂ)).re) ≤
    (R + r) * (R + r)
have key : (-HMul.hMul (β := ℂ) ((↑R : ℂ) * cexp ((↑θ : ℂ) * I))
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑r : ℂ) * cexp ((↑φ : ℂ) * I)) : ℂ)).re ≤
  R * r
Tactic: have key := calc
    (-(R * cexp (θ * I) * (starRingEnd ℂ) (r * cexp (φ * I)))).re ≤ _ := re_le_norm _
    _ ≤ R * r := by simp [abs_of_pos, h₁, h₁.trans h₂]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
key :
  (-HMul.hMul (β := ℂ) ((↑R : ℂ) * cexp ((↑θ : ℂ) * I))
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑r : ℂ) * cexp ((↑φ : ℂ) * I)) : ℂ)).re ≤
    R * r
⊢ HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 -
      2 *
        (HMul.hMul (β := ℂ) ((↑R : ℂ) * cexp ((↑θ : ℂ) * I))
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑r : ℂ) * cexp ((↑φ : ℂ) * I)) : ℂ)).re ≤
    HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 + 2 * (R * r)
have rw : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 +
    2 *
      (-HMul.hMul (β := ℂ) ((↑R : ℂ) * cexp ((↑θ : ℂ) * I))
            ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑r : ℂ) * cexp ((↑φ : ℂ) * I)) : ℂ)).re ≤
  HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 + 2 * (R * r)
Tactic: rw [sub_eq_add_neg, ← mul_neg, ← neg_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
key :
  (-HMul.hMul (β := ℂ) ((↑R : ℂ) * cexp ((↑θ : ℂ) * I))
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑r : ℂ) * cexp ((↑φ : ℂ) * I)) : ℂ)).re ≤
    R * r
⊢ HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 +
      2 *
        (-HMul.hMul (β := ℂ) ((↑R : ℂ) * cexp ((↑θ : ℂ) * I))
              ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑r : ℂ) * cexp ((↑φ : ℂ) * I)) : ℂ)).re ≤
    HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 + 2 * (R * r)
have bc : LE.le (α := ℝ) 0 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
R : ℝ
w c z : ℂ
hz : z ∈ sphere c R
hw : w ∈ ball c R
⊢ (R - ‖w - c‖) / (R + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re
have obtain : ∀ (η₂ : z - c ≠ 0) (hz : z ∈ sphere c ‖z - c‖) (hw : w ∈ ball c ‖z - c‖) (η₀ : 0 < ‖z - c‖),
  (‖z - c‖ - ‖w - c‖) / (‖z - c‖ + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re
Tactic: obtain ⟨η₀, rfl, η₂⟩ : 0 < R ∧ R = ‖z - c‖ ∧ z - c ≠ 0 := by
    grind [ball_eq_empty, mem_sphere, dist_eq_norm, norm_pos_iff]
Cleared hypotheses: R, hz, hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
⊢ (‖z - c‖ - ‖w - c‖) / (‖z - c‖ + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re
have pos : ∀ (h₁w : ‖w - c‖ = 0), (‖z - c‖ - ‖w - c‖) / (‖z - c‖ + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re
Tactic: by_cases h₁w : ‖w - c‖ = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
pos : ∀ (h₁w : ‖w - c‖ = 0), (‖z - c‖ - ‖w - c‖) / (‖z - c‖ + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re
⊢ (‖z - c‖ - ‖w - c‖) / (‖z - c‖ + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re
have neg : ∀ (h₁w : ¬‖w - c‖ = 0), (‖z - c‖ - ‖w - c‖) / (‖z - c‖ + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re
Tactic: by_cases h₁w : ‖w - c‖ = 0
-- 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
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
have inl : ∀ (hR : R ≤ 0), Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 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
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
inl : ∀ (hR : R ≤ 0), Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
have inr : ∀ (hR : 0 < R), Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 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
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
have inr : ∀ (hw : Membership.mem (γ := Set ℂ) (ball 0 R) 0),
  Real.circleAverage (fun (z : ℂ) ↦ ((z + 0) / (z - 0)).re • f z) 0 R = f 0
Tactic: obtain rfl | h₁w := eq_or_ne w 0
Cleared hypotheses: w, 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
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
inr :
  ∀ (hw : Membership.mem (γ := Set ℂ) (ball 0 R) 0),
    Real.circleAverage (fun (z : ℂ) ↦ ((z + 0) / (z - 0)).re • f z) 0 R = f 0
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
have inr₁ : ∀ (h₁w : w ≠ 0), Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
Tactic: obtain rfl | h₁w := eq_or_ne w 0
-- 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 : ℝ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hR : 0 < R
hw : Membership.mem (γ := Set ℂ) (ball 0 R) 0
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + 0) / (z - 0)).re • f z) 0 R = f 0
have inr : ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) (sphere 0 |R|) z), ((z + 0) / (z - 0)).re • f z = f z
Tactic: refine (circleAverage_congr_sphere fun z hz ↦ ?_).trans (abs_of_pos hR ▸ hf |>.circleAverage)
-- 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 : ℝ
inst_2 : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hR : 0 < R
hw : Membership.mem (γ := Set ℂ) (ball 0 R) 0
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |R|) z
⊢ ((z + 0) / (z - 0)).re • f z = f z
have hz₁ : Membership.mem (γ := Set ℂ) (sphere 0 R) z
Tactic: rw [abs_of_pos hR] at hz
Cleared hypotheses: hz
-- 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
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
have h₁q : 0 < q
Tactic: have h₁q : 0 < q := by positivity
-- 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
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
have h₂q : q < 1
Tactic: have h₂q : q < 1 := by simpa [← div_lt_one hR] using 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
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
have suffices : ‖(↑q : ℂ) * x‖ < ‖W‖
Tactic: suffices ‖q * x‖ < ‖W‖ by grind
-- 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‖ ≤ q * R
have ha : 0 ≤ q
Tactic: gcongr
-- 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‖
have q₁ : ‖(↑q : ℂ) * x‖ = q * ‖x‖
Tactic: calc
      ‖q * x‖ = q * ‖x‖ := by simp [abs_of_pos h₁q]
      _ ≤ q * R := by gcongr
      _ < 1 * R := by gcongr
      _ = ‖W‖ := by simp [W, abs_of_pos 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
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₁ : ‖(↑q : ℂ) * x‖ = q * ‖x‖
⊢ ‖(↑q : ℂ) * x‖ < ‖W‖
have q₂ : q * ‖x‖ ≤ q * R
Tactic: calc
      ‖q * x‖ = q * ‖x‖ := by simp [abs_of_pos h₁q]
      _ ≤ q * R := by gcongr
      _ < 1 * R := by gcongr
      _ = ‖W‖ := by simp [W, abs_of_pos 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
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₁ : ‖(↑q : ℂ) * x‖ = q * ‖x‖
q₂ : q * ‖x‖ ≤ q * R
⊢ ‖(↑q : ℂ) * x‖ < ‖W‖
have q₃ : q * R < 1 * R
Tactic: calc
      ‖q * x‖ = q * ‖x‖ := by simp [abs_of_pos h₁q]
      _ ≤ q * R := by gcongr
      _ < 1 * R := by gcongr
      _ = ‖W‖ := by simp [W, abs_of_pos 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
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₁ : ‖(↑q : ℂ) * x‖ = q * ‖x‖
q₂ : q * ‖x‖ ≤ q * R
q₃ : q * R < 1 * R
⊢ ‖(↑q : ℂ) * x‖ < ‖W‖
have q₄ : 1 * R = ‖W‖
Tactic: calc
      ‖q * x‖ = q * ‖x‖ := by simp [abs_of_pos h₁q]
      _ ≤ q * R := by gcongr
      _ < 1 * R := by gcongr
      _ = ‖W‖ := by simp [W, abs_of_pos 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
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
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
have η₀ : ∀ {x : ℂ} (h : ‖x‖ ≤ R), (↑q : ℂ) * x - W ≠ 0
Tactic: have η₀ {x : ℂ} (h : ‖x‖ ≤ R) : q * x - W ≠ 0 := by
    suffices ‖q * x‖ < ‖W‖ by grind
    calc
      ‖q * x‖ = q * ‖x‖ := by simp [abs_of_pos h₁q]
      _ ≤ q * R := by gcongr
      _ < 1 * R := by gcongr
      _ = ‖W‖ := by simp [W, abs_of_pos 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
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)
    (∮ (z : ℂ) in C(0, R), ((↑q : ℂ) / ((↑q : ℂ) * z - W)) • f z)
have apply : ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z),
  z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z = ((↑q : ℂ) / ((↑q : ℂ) * z - W)) • f z
Tactic: apply circleIntegral.integral_congr hR.le fun z hz ↦ ?_
-- 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
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
⊢ z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z = ((↑q : ℂ) / ((↑q : ℂ) * z - W)) • f z
have hz₁ : z ≠ 0
Tactic: have hz : z ≠ 0 := by 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
z : ℂ
hz_1 : Membership.mem (γ := Set ℂ) (sphere 0 R) z
hz : z ≠ 0
⊢ z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z = ((↑q : ℂ) / ((↑q : ℂ) * z - W)) • f z
have match_scalars : z⁻¹ * ((↑q : ℂ) * z / ((↑q : ℂ) * z - W) * 1) = (↑q : ℂ) / ((↑q : ℂ) * z - W) * 1
Tactic: match_scalars
-- 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
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), ((↑q : ℂ) / ((↑q : ℂ) * z - W)) • f z) 0
have apply : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑q : ℂ) / ((↑q : ℂ) * z - W)) (closure (ball 0 R))
Tactic: apply DifferentiableOn.diffContOnCl ?_ |>.smul hf |>.circleIntegral_eq_zero 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
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑q : ℂ) / ((↑q : ℂ) * z - W)) (closure (ball 0 R))
have rw : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑q : ℂ) / ((↑q : ℂ) * z - W)) (closedBall 0 R)
Tactic: rw [closure_ball 0 hR.ne']
-- 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
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑q : ℂ) / ((↑q : ℂ) * z - W)) (closedBall 0 R)
have funProp : ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (closedBall 0 R) x → (↑q : ℂ) * x - W ≠ 0
Tactic: fun_prop (disch := 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
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
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
have h0 : 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)
-- 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
⊢ 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)
have 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
Tactic: apply circleAverage_congr_sphere fun z hz ↦ ?_
-- 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
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
have hzR : ‖z‖ = R
Tactic: have hzR : ‖z‖ = R := by simpa [abs_of_pos hR] using hz
-- 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
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |R|) z
hzR : ‖z‖ = R
⊢ ((z + w) / (z - w)).re • f z = (z / (z - w) - q • z / (q • z - W)) • f z
have match_scalars : HMul.hMul (α := ℂ) (↑((z + w) / (z - w)).re : ℂ) 1 = (z / (z - w) - q • z / (q • z - W)) * 1
Tactic: match_scalars
-- 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
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |R|) z
hzR : ‖z‖ = R
⊢ HMul.hMul (α := ℂ) (↑((z + w) / (z - w)).re : ℂ) 1 = (z / (z - w) - q • z / (q • z - W)) * 1
have simp : (↑((z + w) / (z - w)).re : ℂ) =
  z / (z - w) - (↑‖w‖ : ℂ) / (↑R : ℂ) * z / ((↑‖w‖ : ℂ) / (↑R : ℂ) * z - (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I))
Tactic: simp only [q, W, real_smul, ofReal_div, coe_algebraMap, mul_one]
-- 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
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 |R|) z
hzR : ‖z‖ = R
⊢ (↑((z + w) / (z - w)).re : ℂ) =
    z / (z - w) - (↑‖w‖ : ℂ) / (↑R : ℂ) * z / ((↑‖w‖ : ℂ) / (↑R : ℂ) * z - (↑R : ℂ) * cexp ((↑w.arg : ℂ) * I))
have 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))
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]