awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
h₁w : ¬‖w - c‖ = 0
⊢ ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (‖z - c‖ + ‖w - c‖) / (‖z - c‖ - ‖w - c‖)

Tactic:
simpa using re_herglotzRieszKernel_le_aux (w - c).arg (z - c).arg ‖w - c‖ ‖z - c‖
    (by simpa using h₁w) (mem_ball_iff_norm.1 hw)

Premises used: Norm.norm, HSub.hSub, Complex.arg, _private.0.re_herglotzRieszKernel_le_aux, mem_ball_iff_norm, Iff.mp
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
rw :
  (R - r) / (R + r) ≤
    (HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I)‖ 2 - HPow.hPow (β := ℕ) ‖(↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2) /
      HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2
⊢ (R - r) / (R + r) ≤
    (((↑R : ℂ) * cexp ((↑θ : ℂ) * I) + (↑r : ℂ) * cexp ((↑φ : ℂ) * I)) /
        ((↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I))).re

Tactic:
rw [poissonKernel_eq_re_herglotzRieszKernel_aux]

Premises used: _private.0.poissonKernel_eq_re_herglotzRieszKernel_aux
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
simp :
  (R - r) / (R + r) ≤
    (R + r) * (R - r) / HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2
⊢ (R - r) / (R + r) ≤
    (HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I)‖ 2 - HPow.hPow (β := ℕ) ‖(↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2) /
      HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2

Tactic:
simp only [Complex.norm_mul, norm_real, norm_eq_abs, norm_exp_ofReal_mul_I, mul_one, sq_abs,
    sq_sub_sq]

Premises used: Complex.norm_real, sq_abs, mul_one, Complex.norm_exp_ofReal_mul_I, Complex.norm_mul, Real.norm_eq_abs, sq_sub_sq
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
field_simp :
  1 / (R + r) ≤ (R + r) / HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp (I * (↑φ : ℂ))‖ 2
⊢ (R - r) / (R + r) ≤
    (R + r) * (R - r) / HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2

Tactic:
field_simp [sub_pos.mpr h₂]

Premises used: Iff.mpr, sub_pos
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
simp : 1 / (R + r) ≤ (R + r) / HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2
⊢ 1 / (R + r) ≤ (R + r) / HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp (I * (↑φ : ℂ))‖ 2

Tactic:
simp only [mul_comm I]

Premises used: mul_comm, Complex.I
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
positivity positivity₁ positivity₂ positivity₃ : 0 < R → 0 < R + r
⊢ 0 < R + r

Tactic:
positivity [h₁.trans h₂]

Premises used: LT.lt.trans
-- Module: Mathlib.Analysis.Complex.Poisson
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)
rw₁ : 0 < HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2
⊢ 1 / (R + r) ≤ (R + r) / 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]

Premises used: Complex.normSq_eq_norm_sq, Complex.normSq_sub, div_le_div_iff₀
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ ¬‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I)‖ = ‖(↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖

Tactic:
simpa [abs_of_pos, h₁, h₁.trans h₂] using h₂.ne'

Premises used: LT.lt.ne', LT.lt.trans, abs_of_pos
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 0 < HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2

Tactic:
simpa [sq_pos_iff, sub_eq_zero] using
    (mt <| congr_arg (‖·‖)) <| by simpa [abs_of_pos, h₁, h₁.trans h₂] using h₂.ne'

Premises used: Norm.norm, sub_eq_zero, mt, congr_arg, sq_pos_iff
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 0 < HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2

Tactic:
case hpos => simpa [sq_pos_iff, sub_eq_zero] using
    (mt <| congr_arg (‖·‖)) <| by simpa [abs_of_pos, h₁, h₁.trans h₂] using h₂.ne'

Premises used: Norm.norm, sub_eq_zero, mt, congr_arg, sq_pos_iff
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ ‖-HMul.hMul (β := ℂ) ((↑R : ℂ) * cexp ((↑θ : ℂ) * I))
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑r : ℂ) * cexp ((↑φ : ℂ) * I)) : ℂ)‖ ≤
    R * r

Tactic:
simp [abs_of_pos, h₁, h₁.trans h₂]

Premises used: LT.lt.trans, abs_of_pos
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ (-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₂]
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
key :
  (-HMul.hMul (β := ℂ) ((↑R : ℂ) * cexp ((↑θ : ℂ) * I))
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑r : ℂ) * cexp ((↑φ : ℂ) * I)) : ℂ)).re ≤
    R * r
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)
⊢ 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]

Premises used: sub_eq_add_neg, Complex.neg_re, mul_neg
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
key :
  (-HMul.hMul (β := ℂ) ((↑R : ℂ) * cexp ((↑θ : ℂ) * I))
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑r : ℂ) * cexp ((↑φ : ℂ) * I)) : ℂ)).re ≤
    R * r
bc : LE.le (α := ℝ) 0 2
⊢ 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:
gcongr
-- Module: Mathlib.Analysis.Complex.Poisson
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 * (R * r) = (R + r) * (R + r)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
key :
  (-HMul.hMul (β := ℂ) ((↑R : ℂ) * cexp ((↑θ : ℂ) * I))
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑r : ℂ) * cexp ((↑φ : ℂ) * I)) : ℂ)).re ≤
    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)

Tactic:
simpa using calc
    R ^ 2 + r ^ 2 - 2 * (R * cexp (θ * I) * (starRingEnd ℂ) (r * cexp (φ * I))).re
    _ ≤ R ^ 2 + r ^ 2 + 2 * (R * r) := by rw [sub_eq_add_neg, ← mul_neg, ← neg_re]; gcongr
    _ = (R + r) * (R + r) := by ring

Premises used: HMul.hMul, Complex.ofReal, Complex.re, HAdd.hAdd, Complex.exp, Complex, starRingEnd, DFunLike.coe, Complex.I
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
R : ℝ
w c z : ℂ
hz : z ∈ sphere c R
hw : w ∈ ball c R
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
⊢ (R - ‖w - c‖) / (R + ‖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]

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Poisson
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
neg : ∀ (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

Tactic:
by_cases h₁w : ‖w - c‖ = 0
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
h₁w : ‖w - c‖ = 0
⊢ (‖z - c‖ - ‖w - c‖) / (‖z - c‖ + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
h₁w : ¬‖w - c‖ = 0
⊢ (‖z - c‖ - ‖w - c‖) / (‖z - c‖ + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re

Tactic:
simpa using le_re_herglotzRieszKernel_aux (z - c).arg (w - c).arg ‖w - c‖ ‖z - c‖
    (by simpa using h₁w) (mem_ball_iff_norm.1 hw)

Premises used: Norm.norm, HSub.hSub, Complex.arg, mem_ball_iff_norm, _private.0.le_re_herglotzRieszKernel_aux, 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
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
inr : ∀ (hR : 0 < R), 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

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
hf : DiffContOnCl ℂ f (ball 0 R)
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : R ≤ 0
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + w) / (z - w)).re • f z) 0 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
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
inr₁ : ∀ (h₁w : w ≠ 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

Tactic:
obtain rfl | h₁w := eq_or_ne w 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Complex.Poisson
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

Tactic:
(circleAverage_congr_sphere fun z hz ↦ ?_).trans (abs_of_pos hR ▸ hf |>.circleAverage)

Premises used: Real.circleAverage_congr_sphere, Eq.trans
-- Module: Mathlib.Analysis.Complex.Poisson
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
inr : ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) (sphere 0 |R|) z), ((z + 0) / (z - 0)).re • f z = f z
⊢ Real.circleAverage (fun (z : ℂ) ↦ ((z + 0) / (z - 0)).re • f z) 0 R = f 0

Tactic:
refine (circleAverage_congr_sphere fun z hz ↦ ?_).trans (abs_of_pos hR ▸ hf |>.circleAverage)

Premises used: Real.circleAverage_congr_sphere, Eq.trans
-- Module: Mathlib.Analysis.Complex.Poisson
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
⊢ Membership.mem (γ := Set ℂ) (sphere 0 R) z

Tactic:
rw [abs_of_pos hR] at 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 : ℝ
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

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.Poisson
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

Tactic:
simp [div_self (a := z) (by aesop)]

Premises used: div_self
-- 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
⊢ 0 < q

Tactic:
positivity
-- 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
⊢ 0 < q

Tactic:
have h₁q : 0 < q := by positivity
-- 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
⊢ q < 1

Tactic:
simpa [← div_lt_one hR] using hw

Premises used: div_lt_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
⊢ q < 1

Tactic:
have h₂q : q < 1 := by simpa [← div_lt_one hR] using hw
-- 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
this : ‖(↑q : ℂ) * x‖ < ‖W‖
⊢ (↑q : ℂ) * x - W ≠ 0

Tactic:
grind
-- 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
suffices : ‖(↑q : ℂ) * x‖ < ‖W‖
⊢ (↑q : ℂ) * x - W ≠ 0

Tactic:
suffices ‖q * x‖ < ‖W‖ by grind
-- 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‖ = q * ‖x‖

Tactic:
simp [abs_of_pos h₁q]

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
ha : 0 ≤ q
⊢ q * ‖x‖ ≤ q * R

Tactic:
gcongr
-- 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
ha : 0 < R
⊢ q * R < 1 * R

Tactic:
gcongr
-- 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
⊢ 1 * R = ‖W‖

Tactic:
simp [W, abs_of_pos hR]

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₁ : ‖(↑q : ℂ) * x‖ = q * ‖x‖
q₂ : q * ‖x‖ ≤ q * R
q₃ : q * R < 1 * R
q₄ : 1 * R = ‖W‖
⊢ ‖(↑q : ℂ) * x‖ < ‖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]
-- 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

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]
-- 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
apply :
  ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z),
    z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z = ((↑q : ℂ) / ((↑q : ℂ) * z - W)) • f z
⊢ 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)

Tactic:
apply circleIntegral.integral_congr hR.le fun z hz ↦ ?_

Premises used: circleIntegral.integral_congr, 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
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
⊢ z ≠ 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
z : ℂ
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
⊢ z ≠ 0

Tactic:
have hz : z ≠ 0 := by 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
z : ℂ
hz_1 : Membership.mem (γ := Set ℂ) (sphere 0 R) z
hz : z ≠ 0
match_scalars : z⁻¹ * ((↑q : ℂ) * z / ((↑q : ℂ) * z - W) * 1) = (↑q : ℂ) / ((↑q : ℂ) * z - W) * 1
⊢ z⁻¹ • ((↑q : ℂ) * z / ((↑q : ℂ) * z - W)) • f z = ((↑q : ℂ) / ((↑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
z : ℂ
hz_1 : Membership.mem (γ := Set ℂ) (sphere 0 R) z
hz : z ≠ 0
⊢ z⁻¹ * ((↑q : ℂ) * z / ((↑q : ℂ) * z - W) * 1) = (↑q : ℂ) / ((↑q : ℂ) * z - W) * 1

Tactic:
field
-- 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
apply : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑q : ℂ) / ((↑q : ℂ) * z - W)) (closure (ball 0 R))
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(0, R), ((↑q : ℂ) / ((↑q : ℂ) * z - W)) • f z) 0

Tactic:
apply DifferentiableOn.diffContOnCl ?_ |>.smul hf |>.circleIntegral_eq_zero hR.le

Premises used: DiffContOnCl.smul, DiffContOnCl.circleIntegral_eq_zero, LT.lt.le, DifferentiableOn.diffContOnCl
-- 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
rw : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑q : ℂ) / ((↑q : ℂ) * z - W)) (closedBall 0 R)
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑q : ℂ) / ((↑q : ℂ) * z - W)) (closure (ball 0 R))

Tactic:
rw [closure_ball 0 hR.ne']

Premises used: LT.lt.ne', closure_ball, 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
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
⊢ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (closedBall 0 R) x → (↑q : ℂ) * x - W ≠ 0

Tactic:
aesop