awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
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)
refine : ContinuousOn.{0, u} (Y := E) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) (sphere c R)
⊢ CircleIntegrable.{u} (E := E) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) c R

Tactic:
refine ContinuousOn.circleIntegrable (pos_of_mem_ball hw₀).le ?_

Premises used: ContinuousOn.circleIntegrable, LT.lt.le, Metric.pos_of_mem_ball
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
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)
⊢ ContinuousOn.{0, u} (Y := E) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) (sphere c R)

Tactic:
h1.smul (hf.continuousOn.mono (sphere_subset_closedBall.trans hc))

Premises used: DifferentiableOn.continuousOn, HasSubset.Subset.trans, ContinuousOn.smul, ContinuousOn.mono, Metric.sphere_subset_closedBall
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
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)
⊢ ContinuousOn.{0, u} (Y := E) (fun (z : ℂ) ↦ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • f z) (sphere c R)

Tactic:
exact h1.smul (hf.continuousOn.mono (sphere_subset_closedBall.trans hc))

Premises used: DifferentiableOn.continuousOn, HasSubset.Subset.trans, ContinuousOn.smul, ContinuousOn.mono, Metric.sphere_subset_closedBall
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
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

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))
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
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
⊢ 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)
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
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
⊢ Ne (α := ℤ) (-2) (-1)

Tactic:
decide
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
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 (α := ℂ) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹) 0

Tactic:
simpa using circleIntegral.integral_sub_zpow_of_ne (by decide : (-2 : ℤ) ≠ -1) c w₀ R

Premises used: circleIntegral.integral_sub_zpow_of_ne
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
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 (α := ℂ) (∮ (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
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
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
h4 : Eq (α := ℂ) (∮ (z : ℂ) in C(c, R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹) 0
⊢ 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:
simp only [smul_sub, circleIntegral.integral_sub h2 h3, h4, circleIntegral.integral_smul_const,
      zero_smul, sub_zero]

Premises used: sub_zero, circleIntegral.integral_sub, smul_sub, zero_smul, circleIntegral.integral_smul_const
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
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)

Tactic:
circleIntegral.integral_congr (pos_of_mem_ball hw₀).le fun z hz => ?_

Premises used: circleIntegral.integral_congr, LT.lt.le, Metric.pos_of_mem_ball
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
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₀
refine : ∀ (z : ℂ) (hz : z ∈ sphere c R), (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • (f z - f w₀) = (z - w₀)⁻¹ • dslope f w₀ z
⊢ 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:
refine circleIntegral.integral_congr (pos_of_mem_ball hw₀).le fun z hz => ?_

Premises used: circleIntegral.integral_congr, LT.lt.le, Metric.pos_of_mem_ball
-- Module: Mathlib.Analysis.Complex.RemovableSingularity
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₀
z : ℂ
hz : z ∈ sphere c R
⊢ (HPow.hPow (β := ℕ) (z - w₀) 2)⁻¹ • (f z - f w₀) = (z - w₀)⁻¹ • dslope f w₀ z

Tactic:
simp only [dslope_of_ne, Metric.sphere_disjoint_ball.ne_of_mem hz hw₀, slope, ← smul_assoc, sq,
      mul_inv, Ne, not_false_iff, vsub_eq_sub, smul_eq_mul]

Premises used: smul_assoc, mul_inv, Ne, sq, slope, dslope_of_ne, smul_eq_mul, Metric.sphere_disjoint_ball, not_false_iff, Disjoint.ne_of_mem, vsub_eq_sub
-- Module: Mathlib.Analysis.Complex.RiemannMapping
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
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
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
wlog hU₀ : 0 ∉ U
-- Module: Mathlib.Analysis.Complex.RiemannMapping
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
⊢ ∃ (a : ℂ), a ∉ U

Tactic:
rw [ne_univ_iff_exists_notMem] at hU

Premises used: Set.ne_univ_iff_exists_notMem
-- Module: Mathlib.Analysis.Complex.RiemannMapping
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
hU₁ : ∃ (a : ℂ), a ∉ U
⊢ ∀ {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:
rw [ne_univ_iff_exists_notMem] at hU

Premises used: Set.ne_univ_iff_exists_notMem
-- Module: Mathlib.Analysis.Complex.RiemannMapping
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
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
⊢ ¬0 ∉ U

Tactic:
rw [ne_univ_iff_exists_notMem] at hU

Premises used: Set.ne_univ_iff_exists_notMem
-- Module: Mathlib.Analysis.Complex.RiemannMapping
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
inr : ∀ (a : ℂ) (ha : a ∉ 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

Tactic:
rcases hU with ⟨a, ha⟩
-- Module: Mathlib.Analysis.Complex.RiemannMapping
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
a : ℂ
ha : a ∉ U
⊢ IsSimplyConnected (-a +ᵥ U)

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.RiemannMapping
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
a : ℂ
ha : a ∉ U
⊢ -a +ᵥ U ≠ univ

Tactic:
simp [hU]
-- Module: Mathlib.Analysis.Complex.RiemannMapping
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
a : ℂ
ha : a ∉ U
⊢ 0 ∉ -a +ᵥ U

Tactic:
simpa [mem_vadd_set_iff_neg_vadd_mem]

Premises used: Set.mem_vadd_set_iff_neg_vadd_mem
-- Module: Mathlib.Analysis.Complex.RiemannMapping
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
a : ℂ
ha : a ∉ U
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' (-a +ᵥ U)) ∧ ∀ z ∈ -a +ᵥ U, deriv f z ≠ 0

Tactic:
specialize this (hUo.vadd (-a)) (by simpa) (by simp [hU])
      (by simpa [mem_vadd_set_iff_neg_vadd_mem])

Premises used: IsOpen.vadd, Neg.neg
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : ¬0 ∉ U
a : ℂ
ha : a ∉ U
this : ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' (-a +ᵥ U)) ∧ ∀ z ∈ -a +ᵥ U, deriv f z ≠ 0
inr :
  ∀ (f : ℂ → ℂ) (hf_inj : Injective f) (hf_dense : ¬Dense (f '' (-a +ᵥ U))) (hdf : ∀ z ∈ -a +ᵥ U, deriv f z ≠ 0),
    ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
rcases this with ⟨f, hf_inj, hf_dense, hdf⟩
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : ¬0 ∉ U
a : ℂ
ha : a ∉ U
f : ℂ → ℂ
hf_inj : Injective f
hf_dense : ¬Dense (f '' (-a +ᵥ U))
hdf : ∀ z ∈ -a +ᵥ U, deriv f z ≠ 0
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
⟨f ∘ (-a + ·), hf_inj.comp (add_right_injective (-a)), ?_, fun z hz ↦ ?_⟩

Premises used: add_right_injective, Function.comp, Function.Injective.comp, HAdd.hAdd, And.intro, Exists.intro, Neg.neg
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : ¬0 ∉ U
a : ℂ
ha : a ∉ U
f : ℂ → ℂ
hf_inj : Injective f
hf_dense : ¬Dense (f '' (-a +ᵥ U))
hdf : ∀ z ∈ -a +ᵥ U, deriv f z ≠ 0
inr : ¬Dense ((f ∘ fun (x : ℂ) ↦ -a + x) '' U)
inr₁ : ∀ (z : ℂ) (hz : z ∈ U), deriv (f ∘ fun (x : ℂ) ↦ -a + x) z ≠ 0
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
refine ⟨f ∘ (-a + ·), hf_inj.comp (add_right_injective (-a)), ?_, fun z hz ↦ ?_⟩
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : ¬0 ∉ U
a : ℂ
ha : a ∉ U
f : ℂ → ℂ
hf_inj : Injective f
hf_dense : ¬Dense (f '' (-a +ᵥ U))
hdf : ∀ z ∈ -a +ᵥ U, deriv f z ≠ 0
⊢ ¬Dense ((f ∘ fun (x : ℂ) ↦ -a + x) '' U)

Tactic:
simpa only [← image_vadd, Set.image_image] using hf_dense

Premises used: Set.image_image, Set.image_vadd
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : ¬0 ∉ U
a : ℂ
ha : a ∉ U
f : ℂ → ℂ
hf_inj : Injective f
hf_dense : ¬Dense (f '' (-a +ᵥ U))
hdf : ∀ z ∈ -a +ᵥ U, deriv f z ≠ 0
z : ℂ
hz : z ∈ U
⊢ deriv (f ∘ fun (x : ℂ) ↦ -a + x) z ≠ 0

Tactic:
simpa [Function.comp_def, deriv_comp_const_add] using hdf (-a + z) (mapsTo_image _ _ hz)

Premises used: Set.mapsTo_image, Function.comp_def, HAdd.hAdd, deriv_comp_const_add, Neg.neg
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ rwa rwa₁ rwa₂ rwa₃ : 0 ∉ U
⊢ 0 ∉ id '' U

Tactic:
rwa [image_id]

Premises used: Set.image_id
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
rcases :
  ∀ (f : ℂ → ℂ) (hfc : ContinuousOn f U) (hf_inv : ∀ (x : ℂ), HPow.hPow (β := ℕ) (f x) 2 = id x),
    ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
rcases exists_continuousOn_pow_eq hUc hUo continuousOn_id (by rwa [image_id]) two_ne_zero
    with ⟨f, hfc, hf_inv⟩

Premises used: two_ne_zero, Complex.exists_continuousOn_pow_eq, continuousOn_id
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : ∀ (x : ℂ), HPow.hPow (β := ℕ) (f x) 2 = id x
⊢ LeftInverse (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) f

Tactic:
replace hf_inv : LeftInverse (· ^ 2) f := hf_inv
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) f
z : ℂ
hz : z ∈ U
hfz : f z = 0
⊢ False

Tactic:
simpa [hfz, (ne_of_mem_of_not_mem hz hU₀).symm] using hf_inv z

Premises used: Ne.symm, ne_of_mem_of_not_mem
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) f
⊢ ∀ z ∈ U, f z ≠ 0

Tactic:
have hf₀ : ∀ z ∈ U, f z ≠ 0 := by
    intro z hz hfz
    simpa [hfz, (ne_of_mem_of_not_mem hz hU₀).symm] using hf_inv z
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
hz : z ∈ U
hg : ContinuousAt f z
hf : HasStrictDerivAt (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) (2 * f z) (f z)
hf' : 2 * f z ≠ 0
hfg : ∀ᶠ (y : ℂ) in 𝓝 z, HPow.hPow (β := ℕ) (f y) 2 = y
f₁ : ℂ → ℂ
⊢ HasStrictDerivAt f (2 * f z)⁻¹ z

Tactic:
apply HasStrictDerivAt.of_local_left_inverse

Premises used: HasStrictDerivAt.of_local_left_inverse
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
hz : z ∈ U
⊢ ContinuousAt f z

Tactic:
hfc.continuousAt <| hUo.mem_nhds hz

Premises used: IsOpen.mem_nhds, ContinuousOn.continuousAt
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
hz : z ∈ U
⊢ ContinuousAt f z

Tactic:
exact hfc.continuousAt <| hUo.mem_nhds hz

Premises used: IsOpen.mem_nhds, ContinuousOn.continuousAt
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
hz : z ∈ U
⊢ HasStrictDerivAt (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) (2 * f z) (f z)

Tactic:
simpa using hasStrictDerivAt_pow 2 (f z)

Premises used: OfNat.ofNat, hasStrictDerivAt_pow
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
hz : z ∈ U
⊢ 2 * f z ≠ 0

Tactic:
simpa using hf₀ z hz
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
hz : z ∈ U
⊢ ∀ᶠ (y : ℂ) in 𝓝 z, HPow.hPow (β := ℕ) (f y) 2 = y

Tactic:
.of_forall hf_inv

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
hz : z ∈ U
⊢ ∀ᶠ (y : ℂ) in 𝓝 z, HPow.hPow (β := ℕ) (f y) 2 = y

Tactic:
exact .of_forall hf_inv
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
⊢ ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z

Tactic:
have hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z := by
    intro z hz
    apply HasStrictDerivAt.of_local_left_inverse
    · exact hfc.continuousAt <| hUo.mem_nhds hz
    · simpa using hasStrictDerivAt_pow 2 (f z)
    · simpa using hf₀ z hz
    · exact .of_forall hf_inv
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
⟨f, hf_inv.injective, ?_, fun z hz ↦ ?_⟩

Premises used: Function.LeftInverse.injective, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
refine_1 : ¬Dense (f '' U)
refine_2 : ∀ (z : ℂ) (hz : z ∈ U), deriv f z ≠ 0
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
refine ⟨f, hf_inv.injective, ?_, fun z hz ↦ ?_⟩