awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
hRs : closedBall c (↑R : ℝ) ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
z : ℂ
hz : z ∈ closedBall c (↑R : ℝ)
inl :
  ∀ (hd : ∀ᶠ (z : ℂ) in 𝓝[≠] z, DifferentiableAt ℂ f z) (hc : ContinuousAt f z)
    (hRs : closedBall z (↑R : ℝ) ∩ {z}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x})
    (hz : z ∈ closedBall z (↑R : ℝ)), ContinuousAt f z
⊢ ContinuousAt f z
have inr : ∀ (hne : z ≠ c), ContinuousAt f z
Tactic: rcases eq_or_ne z c with (rfl | hne)
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < (↑R : ℝ)
hRs : closedBall c (↑R : ℝ) ∩ {c}ᶜ ⊆ {x : ℂ | (fun (z : ℂ) ↦ DifferentiableAt ℂ f z) x}
⊢ AnalyticAt ℂ f c
have hc₁ : ContinuousOn f (closedBall c (↑R : ℝ))
Tactic: replace hc : ContinuousOn f (closedBall c R) := by
    refine fun z hz => ContinuousAt.continuousWithinAt ?_
    rcases eq_or_ne z c with (rfl | hne)
    exacts [hc, (hRs ⟨hz, hne⟩).continuousAt]
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hs : s ∈ 𝓝 c
⊢ DifferentiableOn ℂ f (s \ {c}) ∧ ContinuousAt f c ↔ DifferentiableOn ℂ f s
have refine : DifferentiableOn ℂ f (s \ {c}) ∧ ContinuousAt f c → DifferentiableOn ℂ f s
Tactic: refine ⟨?_, fun hd => ⟨hd.mono diff_subset, (hd.differentiableAt hs).continuousAt⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hs : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
hc : ContinuousAt f c
x : ℂ
hx : x ∈ s
⊢ DifferentiableWithinAt ℂ f s x
have inl : ∀ (hs : s ∈ 𝓝 x) (hd : DifferentiableOn ℂ f (s \ {x})) (hc : ContinuousAt f x), DifferentiableWithinAt ℂ f s x
Tactic: rcases eq_or_ne x c with (rfl | hne)
Cleared hypotheses: c, hs, hd, hc
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hs : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
hc : ContinuousAt f c
x : ℂ
hx : x ∈ s
inl : ∀ (hs : s ∈ 𝓝 x) (hd : DifferentiableOn ℂ f (s \ {x})) (hc : ContinuousAt f x), DifferentiableWithinAt ℂ f s x
⊢ DifferentiableWithinAt ℂ f s x
have inr : ∀ (hne : x ≠ c), DifferentiableWithinAt ℂ f s x
Tactic: rcases eq_or_ne x c with (rfl | hne)
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
x : ℂ
hx : x ∈ s
hs : s ∈ 𝓝 x
hd : DifferentiableOn ℂ f (s \ {x})
hc : ContinuousAt f x
⊢ DifferentiableWithinAt ℂ f s x
have inl : ∀ᶠ (z : ℂ) in 𝓝[≠] x, DifferentiableAt ℂ f z
Tactic: refine (analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt
      ?_ hc).differentiableAt.differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
x : ℂ
hx : x ∈ s
hs : s ∈ 𝓝 x
hd : DifferentiableOn ℂ f (s \ {x})
hc : ContinuousAt f x
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] x, DifferentiableAt ℂ f z
have inl : ∀ (z : ℂ) (hz : s ∈ 𝓝 z) (hzx : Membership.mem (γ := Set ℂ) {x}ᶜ z), DifferentiableAt ℂ f z
Tactic: refine eventually_nhdsWithin_iff.2 ((eventually_mem_nhds_iff.2 hs).mono fun z hz hzx => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
this : DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c
⊢ DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c ((𝓝[≠] c).limUnder f)) s
have this₁ : DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c (deriv (fun (x : ℂ) ↦ (x - c) • f x) c)) s
Tactic: rw [differentiableOn_compl_singleton_and_continuousAt_iff hc, ← differentiableOn_dslope hc,
      dslope_sub_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
this : DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c (deriv (fun (x : ℂ) ↦ (x - c) • f x) c)) s
⊢ DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c ((𝓝[≠] c).limUnder f)) s
have hc₁ : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c))
Tactic: have hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c)) :=
      continuousAt_update_same.mp (this.continuousOn.continuousAt hc)
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
⊢ DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c ((𝓝[≠] c).limUnder f)) s
have suffices : DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c
Tactic: suffices DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c by
    rw [differentiableOn_compl_singleton_and_continuousAt_iff hc, ← differentiableOn_dslope hc,
      dslope_sub_smul] at this
    have hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c)) :=
      continuousAt_update_same.mp (this.continuousOn.continuousAt hc)
    rwa [hc.limUnder_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
⊢ DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c
have refine : ContinuousAt F c
Tactic: refine ⟨(differentiableOn_id.sub_const _).smul hd, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
⊢ ContinuousAt F c
have rw : ContinuousWithinAt F {c}ᶜ c
Tactic: rw [← continuousWithinAt_compl_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
⊢ ContinuousWithinAt F {c}ᶜ c
have H : Tendsto.{0, u} (β := E) (fun (x : ℂ) ↦ (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[≠] c) (𝓝 0)
Tactic: have H := ho.tendsto_inv_smul_nhds_zero
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
F : ℂ → E := fun (z : ℂ) ↦ (z - c) • f z
H : Tendsto.{0, u} (β := E) (fun (x : ℂ) ↦ (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[≠] c) (𝓝 0)
⊢ ContinuousWithinAt F {c}ᶜ c
have H' : Tendsto (fun (z : ℂ) ↦ (z - c) • f c) (𝓝[≠] c) (𝓝 (F c))
Tactic: have H' : Tendsto (fun z => (z - c) • f c) (𝓝[≠] c) (𝓝 (F c)) :=
    (continuousWithinAt_id.tendsto.sub tendsto_const_nhds).smul tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
⊢ Tendsto f (𝓝[≠] c) (𝓝 ((𝓝[≠] c).limUnder f))
have hd₁ : ∀ᶠ (x : ℂ) in 𝓝 c, Membership.mem (γ := Set ℂ) {c}ᶜ x → DifferentiableAt ℂ f x
Tactic: rw [eventually_nhdsWithin_iff] at hd
Cleared hypotheses: hd, ho
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, Membership.mem (γ := Set ℂ) {c}ᶜ x → DifferentiableAt ℂ f x
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
⊢ Tendsto f (𝓝[≠] c) (𝓝 ((𝓝[≠] c).limUnder f))
have this : DifferentiableOn ℂ f ({z : ℂ | z ≠ c → DifferentiableAt ℂ f z} \ {c})
Tactic: have : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c}) := fun z hz =>
    (hz.1 hz.2).differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, Membership.mem (γ := Set ℂ) {c}ᶜ x → DifferentiableAt ℂ f x
ho : IsLittleO.{0, u, 0} (E := E) (F := ℂ) (𝓝[≠] c) (fun (z : ℂ) ↦ f z - f c) fun (z : ℂ) ↦ (z - c)⁻¹
this : DifferentiableOn ℂ f ({z : ℂ | z ≠ c → DifferentiableAt ℂ f z} \ {c})
⊢ Tendsto f (𝓝[≠] c) (𝓝 ((𝓝[≠] c).limUnder f))
have H : DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ E) f c ((𝓝[≠] c).limUnder f))
  {x : ℂ | (fun (x : ℂ) ↦ Membership.mem (γ := Set ℂ) {c}ᶜ x → DifferentiableAt ℂ f x) x}
Tactic: have H := differentiableOn_update_limUnder_of_isLittleO hd this ho
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) = deriv f w₀
have hf' : DifferentiableOn ℂ (dslope f w₀) U
Tactic: have hf' : DifferentiableOn ℂ (dslope f w₀) U :=
    (differentiableOn_dslope (hU.mem_nhds ((ball_subset_closedBall.trans hc) hw₀))).mpr hf
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) = deriv f w₀
have h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
Tactic: have h0 := (hf'.diffContOnCl_ball hc).two_pi_i_inv_smul_circleIntegral_sub_inv_smul hw₀
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) = deriv f w₀
have rw : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) =
  HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z)
Tactic: rw [← dslope_same, ← h0]
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) =
    HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z)
have e_a : Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z)
  (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z)
have trans : Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z)
  (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • (f z - f w₀))
Tactic: trans ∮ z in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
trans :
  Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • (f z - f w₀))
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z)
have trans₁ : Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • (f z - f w₀))
  (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z)
Tactic: trans ∮ z in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹) (sphere c R)
have refine : ∀ (w : ℂ) (hw : w ∈ sphere c R) (h : HPow.hPow (β := ℕ) (w - w₀) 2 = 0), False
Tactic: refine ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • (f z - f w₀))
have h1 : ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹) (sphere c R)
Tactic: have h1 : ContinuousOn (fun z : ℂ => ((z - w₀) ^ 2)⁻¹) (sphere c R) := by
      refine ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => ?_
      exact sphere_disjoint_ball.ne_of_mem hw hw₀ (sub_eq_zero.mp (sq_eq_zero_iff.mp h))
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹) (sphere c R)
⊢ CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) c R
have refine : ContinuousOn.{0, u} (Y := E) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) (sphere c R)
Tactic: refine ContinuousOn.circleIntegrable (pos_of_mem_ball hw₀).le ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹) (sphere c R)
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • (f z - f w₀))
have h2 : CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) c R
Tactic: have h2 : CircleIntegrable (fun z : ℂ => ((z - w₀) ^ 2)⁻¹ • f z) c R := by
      refine ContinuousOn.circleIntegrable (pos_of_mem_ball hw₀).le ?_
      exact h1.smul (hf.continuousOn.mono (sphere_subset_closedBall.trans hc))
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹) (sphere c R)
h2 : CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) c R
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • (f z - f w₀))
have h3 : CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f w₀) c R
Tactic: have h3 : CircleIntegrable (fun z : ℂ => ((z - w₀) ^ 2)⁻¹ • f w₀) c R :=
      ContinuousOn.circleIntegrable (pos_of_mem_ball hw₀).le (h1.smul continuousOn_const)
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹) (sphere c R)
h2 : CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) c R
h3 : CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f w₀) c R
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • (f z - f w₀))
have h4 : Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹) 0
Tactic: have h4 : (∮ z : ℂ in C(c, R), ((z - w₀) ^ 2)⁻¹) = 0 := by
      simpa using circleIntegral.integral_sub_zpow_of_ne (by decide : (-2 : ℤ) ≠ -1) c w₀ R
-- Lean 4 proof step from Mathlib.Analysis.Complex.RemovableSingularity (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • (f z - f w₀))
    (∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z)
have refine : ∀ (z : ℂ) (hz : z ∈ sphere c R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • (f z - f w₀) = (z - w₀)⁻¹ • dslope f w₀ z
Tactic: refine circleIntegral.integral_congr (pos_of_mem_ball hw₀).le fun z hz => ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
have inr : ∀
  (this :
    ∀ {U : Set ℂ} (hUo : IsOpen U) (hUc : IsSimplyConnected U) (hU : U ≠ univ) (hU₀ : 0 ∉ U),
      ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0)
  (hU₀ : ¬0 ∉ U), ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
Tactic: wlog hU₀ : 0 ∉ U
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
inr :
  ∀
    (this :
      ∀ {U : Set ℂ} (hUo : IsOpen U) (hUc : IsSimplyConnected U) (hU : U ≠ univ) (hU₀ : 0 ∉ U),
        ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0)
    (hU₀ : ¬0 ∉ U), ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
have wlog : ∀ {U : Set ℂ} (hUo : IsOpen U) (hUc : IsSimplyConnected U) (hU : U ≠ univ) (hU₀ : 0 ∉ U),
  ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
Tactic: wlog hU₀ : 0 ∉ U
Cleared hypotheses: U, hUo, hUc, hU
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (hypothesis)
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
this :
  ∀ {U : Set ℂ} (hUo : IsOpen U) (hUc : IsSimplyConnected U) (hU : U ≠ univ) (hU₀ : 0 ∉ U),
    ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
hU₀ : ¬0 ∉ U
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
have hU₁ : ∃ (a : ℂ), a ∉ U
Tactic: rw [ne_univ_iff_exists_notMem] at hU
Cleared hypotheses: this, hU₀
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU_1 : U ≠ univ
hU : ∃ (a : ℂ), a ∉ U
this :
  ∀ {U : Set ℂ} (hUo : IsOpen U) (hUc : IsSimplyConnected U) (hU : U ≠ univ) (hU₀ : 0 ∉ U),
    ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
hU₀ : ¬0 ∉ U
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
have inr : ∀ (a : ℂ) (ha : a ∉ U), ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
Tactic: rcases hU with ⟨a, ha⟩
Cleared hypotheses: hU