awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w x : ℂ
hx : Membership.mem (γ := Set ℂ) {w}ᶜ x
h : R ≠ 0
this : x - w ≠ 0
⊢ (↑R : ℂ) * (x - w) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w x : ℂ
hx : Membership.mem (γ := Set ℂ) {w}ᶜ x
h : R ≠ 0
this : x - w ≠ 0
funProp : (↑R : ℂ) * (x - w) ≠ 0
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      (HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) /
        ((↑R : ℂ) * (z - w)))
    x

Tactic:
fun_prop (disch := positivity)
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ MeromorphicAt (E := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ MeromorphicAt (E := ℂ) (fun (z : ℂ) ↦ (↑R : ℂ) * (z - w)) w

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ MeromorphicAt (E := ℂ) (fun (z : ℂ) ↦ (↑R : ℂ)) w

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ MeromorphicAt (E := ℂ) (fun (z : ℂ) ↦ z - w) w

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
rw :
  meromorphicOrderAt (E := ℂ)
        (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w -
      (meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ (↑R : ℂ)) w + meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ z - w) w) =
    -1
⊢ meromorphicOrderAt (E := ℂ)
      (fun (z : ℂ) ↦
        (HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) /
          ((↑R : ℂ) * (z - w)))
      w =
    -1

Tactic:
rw [fun_meromorphicOrderAt_div (by fun_prop) (by fun_prop),
    fun_meromorphicOrderAt_mul (by fun_prop) (by fun_prop)]

Premises used: fun_meromorphicOrderAt_div, fun_meromorphicOrderAt_mul
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ meromorphicOrderAt (E := ℂ)
      (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w =
    0

Tactic:
(MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff ?_).2 ?_

Premises used: Iff.mpr, MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
refine_1 :
  MeromorphicNFAt (E := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w
refine_2 : HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) w ≠ 0
⊢ meromorphicOrderAt (E := ℂ)
      (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w =
    0

Tactic:
refine (MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff ?_).2 ?_

Premises used: Iff.mpr, MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
refine_1 :
  AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w
⊢ MeromorphicNFAt (E := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w

Tactic:
apply AnalyticAt.meromorphicNFAt

Premises used: AnalyticAt.meromorphicNFAt
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
refine_2 : ¬R = ‖w‖
⊢ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) w ≠ 0

Tactic:
rw [← normSq_eq_conj_mul_self, normSq_eq_norm_sq w, sub_ne_zero, ne_eq, ← ofReal_pow,
        ofReal_inj, sq_eq_sq₀ (pos_of_mem_ball h).le (norm_nonneg w)]

Premises used: sub_ne_zero, Complex.normSq_eq_norm_sq, LT.lt.le, ne_eq, Complex.ofReal_inj, Complex.normSq_eq_conj_mul_self, Metric.pos_of_mem_ball, sq_eq_sq₀, Complex.ofReal_pow, norm_nonneg
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ ‖w‖ < R

Tactic:
rw [mem_ball_iff_norm, sub_zero] at h

Premises used: sub_zero, mem_ball_iff_norm
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : ‖w‖ < R
⊢ ¬R = ‖w‖

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ meromorphicOrderAt (E := ℂ)
      (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w =
    0

Tactic:
have : meromorphicOrderAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w = 0 := by
    refine (MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff ?_).2 ?_
    · apply AnalyticAt.meromorphicNFAt
      fun_prop
    · rw [← normSq_eq_conj_mul_self, normSq_eq_norm_sq w, sub_ne_zero, ne_eq, ← ofReal_pow,
        ofReal_inj, sq_eq_sq₀ (pos_of_mem_ball h).le (norm_nonneg w)]
      rw [mem_ball_iff_norm, sub_zero] at h
      grind
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
this :
  meromorphicOrderAt (E := ℂ)
      (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w =
    0
⊢ meromorphicOrderAt (E := ℂ)
        (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w -
      (meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ (↑R : ℂ)) w + meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ z - w) w) =
    -1

Tactic:
simp [this, meromorphicOrderAt_const, (pos_of_mem_ball h).ne',
    meromorphicOrderAt_id_sub_const]

Premises used: meromorphicOrderAt_const, LT.lt.ne', meromorphicOrderAt_id_sub_const, Metric.pos_of_mem_ball
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
z : ℂ
hz : Membership.mem (γ := Set ℂ) Set.univ z
inl : ∀ (h : Membership.mem (γ := Set ℂ) (ball 0 R) z), MeromorphicNFAt (canonicalFactor R z) z
inr : ∀ (h₁ : z ≠ w), MeromorphicNFAt (canonicalFactor R w) z
⊢ MeromorphicNFAt (canonicalFactor R w) z

Tactic:
obtain (rfl | h₁) := eq_or_ne z w

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) Set.univ z
h : Membership.mem (γ := Set ℂ) (ball 0 R) z
inl :
  AnalyticAt ℂ (canonicalFactor R z) z ∨
    MeromorphicAt (canonicalFactor R z) z ∧ meromorphicOrderAt (canonicalFactor R z) z < 0 ∧ canonicalFactor R z z = 0
⊢ MeromorphicNFAt (canonicalFactor R z) z

Tactic:
rw [meromorphicNFAt_iff_analyticAt_or]

Premises used: meromorphicNFAt_iff_analyticAt_or
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) Set.univ z
h : Membership.mem (γ := Set ℂ) (ball 0 R) z
inl : MeromorphicAt (canonicalFactor R z) z ∧ meromorphicOrderAt (canonicalFactor R z) z < 0 ∧ canonicalFactor R z z = 0
⊢ AnalyticAt ℂ (canonicalFactor R z) z ∨
    MeromorphicAt (canonicalFactor R z) z ∧ meromorphicOrderAt (canonicalFactor R z) z < 0 ∧ canonicalFactor R z z = 0

Tactic:
right
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) Set.univ z
h : Membership.mem (γ := Set ℂ) (ball 0 R) z
⊢ canonicalFactor R z z = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) Set.univ z
h : Membership.mem (γ := Set ℂ) (ball 0 R) z
inl : meromorphicOrderAt (canonicalFactor R z) z < 0
⊢ MeromorphicAt (canonicalFactor R z) z ∧ meromorphicOrderAt (canonicalFactor R z) z < 0 ∧ canonicalFactor R z z = 0

Tactic:
refine ⟨meromorphicOn_canonicalFactor R z z (Set.mem_univ z), ?_, by simp⟩
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) Set.univ z
h : Membership.mem (γ := Set ℂ) (ball 0 R) z
⊢ LT.lt (α := ℤ) (-1) 0

Tactic:
lia
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) Set.univ z
h : Membership.mem (γ := Set ℂ) (ball 0 R) z
⊢ meromorphicOrderAt (canonicalFactor R z) z < 0

Tactic:
simpa [meromorphicOrderAt_canonicalFactor h] using WithTop.coe_lt_zero.mpr (by lia : -1 < 0)

Premises used: Iff.mpr, Complex.meromorphicOrderAt_canonicalFactor, WithTop.coe_lt_zero
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
z : ℂ
hz : Membership.mem (γ := Set ℂ) Set.univ z
h₁ : z ≠ w
⊢ MeromorphicNFAt (canonicalFactor R w) z

Tactic:
apply (analyticOnNhd_canonicalFactor R w z h₁).meromorphicNFAt

Premises used: AnalyticAt.meromorphicNFAt, Complex.analyticOnNhd_canonicalFactor
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
h₁z : Membership.mem (γ := Set ℂ) (closedBall 0 R) z
h₂z : z ≠ w
⊢ 0 < R ∧ z - w ≠ 0

Tactic:
grind [mem_ball_zero_iff, norm_nonneg]

Premises used: norm_nonneg, mem_ball_zero_iff
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
h₁z : Membership.mem (γ := Set ℂ) (closedBall 0 R) z
h₂z : z ≠ w
⊢ 0 < R

Tactic:
obtain ⟨hR, hzw⟩ : 0 < R ∧ z - w ≠ 0 := by grind [mem_ball_zero_iff, norm_nonneg]
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
h₁z : Membership.mem (γ := Set ℂ) (closedBall 0 R) z
h₂z : z ≠ w
hR : 0 < R
⊢ z - w ≠ 0

Tactic:
obtain ⟨hR, hzw⟩ : 0 < R ∧ z - w ≠ 0 := by grind [mem_ball_zero_iff, norm_nonneg]
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
h₁z : Membership.mem (γ := Set ℂ) (closedBall 0 R) z
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
⊢ ‖w‖ < R

Tactic:
simp only [mem_ball, dist_zero_right, mem_closedBall] at hw h₁z

Premises used: Metric.mem_ball, Metric.mem_closedBall, dist_zero_right
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
h₁z : Membership.mem (γ := Set ℂ) (closedBall 0 R) z
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw₁ : ‖w‖ < R
⊢ ‖z‖ ≤ R

Tactic:
simp only [mem_ball, dist_zero_right, mem_closedBall] at hw h₁z

Premises used: Metric.mem_ball, Metric.mem_closedBall, dist_zero_right
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
this : ‖HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z‖ < ‖HPow.hPow (β := ℕ) (↑R : ℂ) 2‖
⊢ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
suffices : ‖HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z‖ < ‖HPow.hPow (β := ℕ) (↑R : ℂ) 2‖
⊢ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z ≠ 0

Tactic:
suffices ‖conj w * z‖ < ‖(R : ℂ) ^ 2‖ by grind
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
this : ‖w‖ * ‖z‖ < R * R
⊢ ‖HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z‖ < ‖HPow.hPow (β := ℕ) (↑R : ℂ) 2‖

Tactic:
simpa [sq]

Premises used: sq
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
suffices : ‖w‖ * ‖z‖ < R * R
⊢ ‖HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z‖ < ‖HPow.hPow (β := ℕ) (↑R : ℂ) 2‖

Tactic:
suffices ‖w‖ * ‖z‖ < R * R by simpa [sq]
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
grw : ‖w‖ * R < R * R
⊢ ‖w‖ * ‖z‖ < R * R

Tactic:
grw [h₁z]
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
ha : 0 < R
⊢ ‖w‖ * R < R * R

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
⊢ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z ≠ 0

Tactic:
have h_num_ne_zero : R ^ 2 - conj w * z ≠ 0 := by
    suffices ‖conj w * z‖ < ‖(R : ℂ) ^ 2‖ by grind
    suffices ‖w‖ * ‖z‖ < R * R by simpa [sq]
    grw [h₁z]
    gcongr
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
h_num_ne_zero : HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z ≠ 0
⊢ (HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) / ((↑R : ℂ) * (z - w)) ≠
    0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
⊢ 0 < R ∧ z - w ≠ 0

Tactic:
grind [mem_ball_zero_iff, norm_nonneg, mem_sphere_zero_iff_norm]

Premises used: mem_sphere_zero_iff_norm, norm_nonneg, mem_ball_zero_iff
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
⊢ 0 < R

Tactic:
obtain ⟨hR, hzw⟩ : 0 < R ∧ z - w ≠ 0 := by
    grind [mem_ball_zero_iff, norm_nonneg, mem_sphere_zero_iff_norm]
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
hR : 0 < R
⊢ z - w ≠ 0

Tactic:
obtain ⟨hR, hzw⟩ : 0 < R ∧ z - w ≠ 0 := by
    grind [mem_ball_zero_iff, norm_nonneg, mem_sphere_zero_iff_norm]
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
hR : 0 < R
hzw : z - w ≠ 0
rw : ¬(↑R : ℂ) * (z - w) = 0
⊢ ‖(↑R : ℂ) * (z - w)‖ ≠ 0

Tactic:
rw [ne_eq, norm_eq_zero]

Premises used: norm_eq_zero, ne_eq
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
hR : 0 < R
hzw : z - w ≠ 0
⊢ ¬(↑R : ℂ) * (z - w) = 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
hR : 0 < R
hzw : z - w ≠ 0
rw : ‖HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z‖ = ‖(↑R : ℂ) * (z - w)‖
⊢ ‖canonicalFactor R w z‖ = 1

Tactic:
rw [canonicalFactor, norm_div, div_eq_iff (by rw [ne_eq, norm_eq_zero]; positivity), one_mul]

Premises used: div_eq_iff, norm_div, Complex.canonicalFactor, one_mul
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
hR : 0 < R
hzw : z - w ≠ 0
⊢ ‖z‖ = R

Tactic:
simpa [mem_sphere_zero_iff_norm] using hz

Premises used: mem_sphere_zero_iff_norm
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
hR : 0 < R
hzw : z - w ≠ 0
obtain :
  ∀ (hw : Membership.mem (γ := Set ℂ) (ball 0 ‖z‖) w) (hz : Membership.mem (γ := Set ℂ) (sphere 0 ‖z‖) z)
    (hR : 0 < ‖z‖),
    ‖HPow.hPow (β := ℕ) (↑‖z‖ : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z‖ =
      ‖(↑‖z‖ : ℂ) * (z - w)‖
⊢ ‖HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z‖ = ‖(↑R : ℂ) * (z - w)‖

Tactic:
obtain rfl := by simpa [mem_sphere_zero_iff_norm] using hz

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
w z : ℂ
hzw : z - w ≠ 0
hw : Membership.mem (γ := Set ℂ) (ball 0 ‖z‖) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 ‖z‖) z
hR : 0 < ‖z‖
rw :
  ‖z * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)‖ =
    ‖(↑‖z‖ : ℂ) * (z - w)‖
⊢ ‖HPow.hPow (β := ℕ) (↑‖z‖ : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z‖ =
    ‖(↑‖z‖ : ℂ) * (z - w)‖

Tactic:
rw [← ofReal_pow, ← normSq_eq_norm_sq, normSq_eq_conj_mul_self, ← sub_mul, mul_comm _ z]

Premises used: Complex.normSq_eq_norm_sq, sub_mul, mul_comm, Complex.normSq_eq_conj_mul_self, Complex.ofReal_pow
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
w z : ℂ
hzw : z - w ≠ 0
hw : Membership.mem (γ := Set ℂ) (ball 0 ‖z‖) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 ‖z‖) z
hR : 0 < ‖z‖
⊢ ‖z * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)‖ =
    ‖(↑‖z‖ : ℂ) * (z - w)‖

Tactic:
simp [← map_sub]

Premises used: map_sub
-- Module: Mathlib.Analysis.Complex.Cardinality
Goal:
rw : #(ℝ × ℝ) = 𝔠
rw₁ : lift.{0, 0} #ℝ * lift.{0, 0} #ℝ = 𝔠
rw₂ : #ℝ * #ℝ = 𝔠
rw₃ : 𝔠 * 𝔠 = 𝔠
rw₄ rw₅ : 𝔠 = 𝔠
⊢ #ℂ = 𝔠

Tactic:
rw [mk_congr Complex.equivRealProd, mk_prod, lift_id, mk_real, continuum_mul_self]

Premises used: Cardinal.continuum_mul_self, Cardinal.mk_real, Complex.equivRealProd, Cardinal.mk_congr, Cardinal.lift_id, Cardinal.mk_prod
-- Module: Mathlib.Analysis.Complex.Cardinality
Goal:
rw : #ℂ = 𝔠
rw₁ rw₂ : 𝔠 = 𝔠
⊢ #(↑Set.univ : Type) = 𝔠

Tactic:
rw [mk_univ, mk_complex]

Premises used: Cardinal.mk_univ, Cardinal.mk_complex
-- Module: Mathlib.Analysis.Complex.Cardinality
Goal:
rw : ℵ₀ < 𝔠
⊢ ¬Set.Countable (α := ℂ) Set.univ

Tactic:
rw [← le_aleph0_iff_set_countable, not_le, Cardinal.mk_univ_complex]

Premises used: not_le, Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_univ_complex
-- Module: Mathlib.Analysis.Complex.Cardinality
Goal:
⊢ ℵ₀ < 𝔠

Tactic:
apply cantor

Premises used: Cardinal.cantor
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (z : ℂ) ↦
      HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' z : (a : ℂ) → E) 1 : E)) ((f' z : (a : ℂ) → E) I : E))
    ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
⊢ ∀ (x y : ℝ), (↑x : ℂ) + (↑y : ℂ) * I = (e : (a : ℝ × ℝ) → ℂ) (x, y)

Tactic:
have he : ∀ x y : ℝ, ↑x + ↑y * I = e (x, y) := fun x y => (mk_eq_add_mul_I x y).symm
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (z : ℂ) ↦
      HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' z : (a : ℂ) → E) 1 : E)) ((f' z : (a : ℂ) → E) I : E))
    ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he : ∀ (x y : ℝ), (↑x : ℂ) + (↑y : ℂ) * I = (e : (a : ℝ × ℝ) → ℂ) (x, y)
⊢ Eq (α := ℂ) ((e : (a : ℝ × ℝ) → ℂ) (1, 0) : ℂ) (1 : ℂ)

Tactic:
have he₁ : e (1, 0) = 1 := rfl
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (z : ℂ) ↦
      HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' z : (a : ℂ) → E) 1 : E)) ((f' z : (a : ℂ) → E) I : E))
    ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he : ∀ (x y : ℝ), (↑x : ℂ) + (↑y : ℂ) * I = (e : (a : ℝ × ℝ) → ℂ) (x, y)
he₁ : Eq (α := ℂ) ((e : (a : ℝ × ℝ) → ℂ) (1, 0) : ℂ) (1 : ℂ)
⊢ (e : (a : ℝ × ℝ) → ℂ) (0, 1) = I

Tactic:
have he₂ : e (0, 1) = I := rfl
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (z : ℂ) ↦
      HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' z : (a : ℂ) → E) 1 : E)) ((f' z : (a : ℂ) → E) I : E))
    ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he : ∀ (x y : ℝ), (↑x : ℂ) + (↑y : ℂ) * I = (e : (a : ℝ × ℝ) → ℂ) (x, y)
he₁ : Eq (α := ℂ) ((e : (a : ℝ × ℝ) → ℂ) (1, 0) : ℂ) (1 : ℂ)
he₂ : (e : (a : ℝ × ℝ) → ℂ) (0, 1) = I
simp :
  ∀ (he : ∀ (x y : ℝ), True),
    HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((e : (a : ℝ × ℝ) → ℂ) (x, z.im)))
            (∫ (x : ℝ) in z.re..w.re, f ((e : (a : ℝ × ℝ) → ℂ) (x, w.im))) +
          HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((e : (a : ℝ × ℝ) → ℂ) (w.re, y))) -
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((e : (a : ℝ × ℝ) → ℂ) (z.re, y))) =
      ∫ (x : ℝ) in z.re..w.re,
        ∫ (y : ℝ) in z.im..w.im,
          HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' ((e : (a : ℝ × ℝ) → ℂ) (x, y)) : (a : ℂ) → E) 1 : E))
            ((f' ((e : (a : ℝ × ℝ) → ℂ) (x, y)) : (a : ℂ) → E) I : E)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I)) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' ((↑x : ℂ) + (↑y : ℂ) * I) : (a : ℂ) → E) 1 : E))
          ((f' ((↑x : ℂ) + (↑y : ℂ) * I) : (a : ℂ) → E) I : E)

Tactic:
simp only [he] at *