awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∃ (x : ℂ), ∀ᶠ (x : ℂ) in 𝓝 x, x ∉ f '' U
⊢ ¬Dense (f '' U)

Tactic:
simp only [Dense, not_forall, mem_closure_iff_frequently, not_frequently]

Premises used: mem_closure_iff_frequently, Dense, Filter.not_frequently, Classical.not_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
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
refine_1 : ∀ (x : ℂ) (hx : x ∈ U), ∃ (x : ℂ), ∀ᶠ (x : ℂ) in 𝓝 x, x ∉ f '' U
⊢ ∃ (x : ℂ), ∀ᶠ (x : ℂ) in 𝓝 x, x ∉ f '' U

Tactic:
rcases hUc.nonempty with ⟨x, hx⟩

Premises used: IsSimplyConnected.nonempty
-- 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
x : ℂ
hx : x ∈ U
h : ∀ᶠ (x : ℂ) in 𝓝 (-f x), x ∉ f '' U
⊢ ∃ (x : ℂ), ∀ᶠ (x : ℂ) in 𝓝 x, x ∉ f '' U

Tactic:
use -f x
-- 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
x : ℂ
hx : x ∈ U
⊢ (2 * f x)⁻¹ ≠ 0

Tactic:
simpa using hf₀ x hx
-- 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
x : ℂ
hx : x ∈ U
rw : f '' U ∈ map f (𝓝 x)
⊢ f '' U ∈ 𝓝 (f x)

Tactic:
rw [← (hdf x hx).map_nhds_eq (by simpa using hf₀ x hx)]

Premises used: HasStrictDerivAt.map_nhds_eq
-- 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
x : ℂ
hx : x ∈ U
⊢ f '' U ∈ map f (𝓝 x)

Tactic:
Filter.image_mem_map <| hUo.mem_nhds hx

Premises used: Filter.image_mem_map, IsOpen.mem_nhds
-- 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
x : ℂ
hx : x ∈ U
⊢ f '' U ∈ map f (𝓝 x)

Tactic:
exact Filter.image_mem_map <| hUo.mem_nhds hx

Premises used: Filter.image_mem_map, IsOpen.mem_nhds
-- 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
x : ℂ
hx : x ∈ U
⊢ f '' U ∈ 𝓝 (f x)

Tactic:
have : f '' U ∈ 𝓝 (f x) := by
      rw [← (hdf x hx).map_nhds_eq (by simpa using hf₀ x hx)]
      exact Filter.image_mem_map <| hUo.mem_nhds hx
-- 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
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
h : ∀ᶠ (x : ℂ) in 𝓝 (f x), -x ∉ f '' U
⊢ ∀ᶠ (x : ℂ) in 𝓝 (-f x), x ∉ f '' U

Tactic:
rw [nhds_neg, eventually_neg]

Premises used: nhds_neg, Filter.eventually_neg
-- 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
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
h : ∀ a ∈ f '' U, -a ∉ f '' U
⊢ ∀ᶠ (x : ℂ) in 𝓝 (f x), -x ∉ f '' U

Tactic:
filter_upwards [this]
-- 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
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
a : ℂ
ha : a ∈ U
b : ℂ
hb : b ∈ U
hab : f b = -f a
rw : a = (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) (-f a)
⊢ a = b

Tactic:
rw [← hf_inv b, hab]
-- 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
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
a : ℂ
ha : a ∈ U
b : ℂ
hb : b ∈ U
hab : f b = -f a
⊢ a = (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) (-f a)

Tactic:
simp [hf_inv a]
-- 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
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
a : ℂ
ha : a ∈ U
b : ℂ
hb : b ∈ U
hab : f b = -f a
⊢ a ∈ U

Tactic:
obtain rfl : a = b := by
      rw [← hf_inv b, hab]
      simp [hf_inv a]

Premises used: rfl
-- 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
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
a : ℂ
ha : a ∈ U
b : ℂ
hb : b ∈ U
hab : f b = -f a
hb₁ : a ∈ U
⊢ f a = -f a

Tactic:
obtain rfl : a = b := by
      rw [← hf_inv b, hab]
      simp [hf_inv a]

Premises used: rfl
-- 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
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
a : ℂ
ha hb : a ∈ U
hab : f a = -f a
⊢ False

Tactic:
hf₀ a ha ?_
-- 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
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
a : ℂ
ha hb : a ∈ U
hab : f a = -f a
h : f a = 0
⊢ False

Tactic:
refine hf₀ a ha ?_
-- 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
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
a : ℂ
ha hb : a ∈ U
hab : f a = -f a
⊢ f a = 0

Tactic:
linear_combination hab / 2
-- 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
z : ℂ
hz : z ∈ U
⊢ deriv f z ≠ 0

Tactic:
simpa [(hdf z hz).hasDerivAt.deriv] using hf₀ z hz

Premises used: HasDerivAt.deriv, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
rcases :
  ∀ (f : ℂ → ℂ) (hf_inj : Injective f) (hfd : ¬Dense (f '' U)) (hdf : ∀ z ∈ U, deriv f z ≠ 0),
    ∃ (f : ℂ → ℂ), MapsTo f U (ball 0 1) ∧ InjOn f U ∧ ∀ z ∈ U, deriv f z ≠ 0
⊢ ∃ (f : ℂ → ℂ), MapsTo f U (ball 0 1) ∧ InjOn f U ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
rcases exists_injective_not_dense_image_deriv_ne_zero hUo hUc hU with ⟨f, hf_inj, hfd, hdf⟩

Premises used: _private.0.Complex.exists_injective_not_dense_image_deriv_ne_zero
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
⊢ ∃ (x : ℂ) (ε : ℝ), 0 < ε ∧ ∀ a ∈ U, ε < dist (f a) x

Tactic:
simpa [Dense, mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall] using hfd

Premises used: Dense, Metric.nhds_basis_closedBall, mem_closure_iff_nhds_basis
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
obtain :
  ∀ (x : ℂ) (ε : ℝ) (hε₀ : 0 < ε) (hε : ∀ a ∈ U, ε < dist (f a) x),
    ∃ (f : ℂ → ℂ), MapsTo f U (ball 0 1) ∧ InjOn f U ∧ ∀ z ∈ U, deriv f z ≠ 0
⊢ ∃ (f : ℂ → ℂ), MapsTo f U (ball 0 1) ∧ InjOn f U ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
obtain ⟨x, ε, hε₀, hε⟩ : ∃ (x : ℂ) (ε : ℝ), 0 < ε ∧ ∀ a ∈ U, ε < dist (f a) x := by
    simpa [Dense, mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall] using hfd
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
z : ℂ
hz : z ∈ U
⊢ f z ≠ x

Tactic:
simpa using hε₀.trans (hε z hz)

Premises used: LT.lt.trans
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
⊢ ∀ z ∈ U, f z ≠ x

Tactic:
have hfx : ∀ z ∈ U, f z ≠ x := fun z hz ↦ by simpa using hε₀.trans (hε z hz)
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
h :
  MapsTo (β := ℂ) (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) U (ball 0 1) ∧
    InjOn (β := ℂ) (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) U ∧
      ∀ z ∈ U, Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z) 0
⊢ ∃ (f : ℂ → ℂ), MapsTo f U (ball 0 1) ∧ InjOn f U ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
use fun z ↦ ε / (f z - x)

Premises used: HSub.hSub, HDiv.hDiv, Complex.ofReal
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
⊢ MapsTo (β := ℂ) (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) U (ball 0 1) ∧
    InjOn (β := ℂ) (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) U ∧
      ∀ z ∈ U, Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z) 0

Tactic:
⟨?mapsTo, ?injOn, ?deriv⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
refine : MapsTo (β := ℂ) (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) U (ball 0 1)
refine₁ : InjOn (β := ℂ) (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) U
refine₂ : ∀ z ∈ U, Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z) 0
⊢ MapsTo (β := ℂ) (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) U (ball 0 1) ∧
    InjOn (β := ℂ) (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) U ∧
      ∀ z ∈ U, Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z) 0

Tactic:
refine ⟨?mapsTo, ?injOn, ?deriv⟩
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
rw : ε < ‖f z - x‖
rw₁ : 0 < ‖f z - x‖
⊢ Membership.mem (γ := Set ℂ) (ball 0 1) ((fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z)

Tactic:
rw [mem_ball_zero_iff, norm_div, norm_real, Real.norm_of_nonneg hε₀.le, div_lt_one₀]

Premises used: LT.lt.le, Complex.norm_real, norm_div, div_lt_one₀, mem_ball_zero_iff, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
⊢ ε < ‖f z - x‖

Tactic:
simpa [dist_eq_norm] using hε z hz

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
⊢ 0 < ‖f z - x‖

Tactic:
simpa [sub_eq_zero] using hfx z hz

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
⊢ MapsTo (β := ℂ) (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) U (ball 0 1)

Tactic:
case mapsTo =>
    intro z hz
    rw [mem_ball_zero_iff, norm_div, norm_real, Real.norm_of_nonneg hε₀.le, div_lt_one₀]
    · simpa [dist_eq_norm] using hε z hz
    · simpa [sub_eq_zero] using hfx z hz

Premises used: dist_eq_norm, sub_eq_zero, LT.lt.le, Complex.norm_real, norm_div, div_lt_one₀, mem_ball_zero_iff, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
w : ℂ
hw : w ∈ U
heq : Eq (α := ℂ) ((fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z) ((fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) w)
⊢ z = w

Tactic:
simpa [div_eq_mul_inv, hε₀.ne', hf_inj.eq_iff] using heq

Premises used: Function.Injective.eq_iff, div_eq_mul_inv, LT.lt.ne'
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
⊢ InjOn (β := ℂ) (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) U

Tactic:
case injOn =>
    intro z hz w hw heq
    simpa [div_eq_mul_inv, hε₀.ne', hf_inj.eq_iff] using heq

Premises used: Function.Injective.eq_iff, div_eq_mul_inv, LT.lt.ne'
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
⊢ DifferentiableAt ℂ f z

Tactic:
have hdz : DifferentiableAt ℂ f z := differentiableAt_of_deriv_ne_zero (hdf z hz)
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
hdz : DifferentiableAt ℂ f z
rw : (0 * (f z - x) - (↑ε : ℂ) * deriv f z) / HPow.hPow (β := ℕ) (f z - x) 2 ≠ 0
rw₁ : f z - x ≠ 0
⊢ Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z) 0

Tactic:
rw [(hasDerivAt_const _ _).fun_div (hdz.hasDerivAt.sub_const _) _ |>.deriv]

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.sub_const, HasDerivAt.fun_div
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
hdz : DifferentiableAt ℂ f z
⊢ (0 * (f z - x) - (↑ε : ℂ) * deriv f z) / HPow.hPow (β := ℕ) (f z - x) 2 ≠ 0

Tactic:
simp [*, ne_of_gt, sub_eq_zero]

Premises used: sub_eq_zero, ne_of_gt
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
hdz : DifferentiableAt ℂ f z
⊢ f z - x ≠ 0

Tactic:
simp [*, ne_of_gt, sub_eq_zero]

Premises used: sub_eq_zero, ne_of_gt
-- Module: Mathlib.Analysis.Complex.RiemannMapping
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
case case₁ : ∀ (z : ℂ) (hz : z ∈ U), Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z) 0
case₂ :
  ∀ (z : ℂ) (hz : z ∈ U) (hdz : DifferentiableAt ℂ f z), Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z) 0
⊢ ∀ z ∈ U, Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z) 0

Tactic:
case deriv =>
    intro z hz
    have hdz : DifferentiableAt ℂ f z := differentiableAt_of_deriv_ne_zero (hdf z hz)
    rw [(hasDerivAt_const _ _).fun_div (hdz.hasDerivAt.sub_const _) _ |>.deriv] <;>
      simp [*, ne_of_gt, sub_eq_zero]

Premises used: sub_eq_zero, deriv, ne_of_gt
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : z ∈ ball c R₁
⊢ 0 < R₁

Tactic:
have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
inr :
  ∀
    (this :
      ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
        (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
        (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
        ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1))
    (hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
wlog :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
wlog hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧
    MapsTo f (closedBall c R₁) (closedBall (f c) R₂) generalizing R₁

Premises used: Set.MapsTo, DifferentiableOn, Metric.closedBall, Complex
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this_1 :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
this : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
ge_of_tendsto ?_ this

Premises used: ge_of_tendsto
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this_1 :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
this : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
refine : Tendsto (fun (c_1 : ℝ) ↦ R₂ * (‖z - c‖ / c_1) ^ (n + 1)) (𝓝[<] R₁) (𝓝 (R₂ * (‖z - c‖ / R₁) ^ (n + 1)))
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
refine ge_of_tendsto ?_ this

Premises used: ge_of_tendsto
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this_1 :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
this : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
⊢ Tendsto (fun (c_1 : ℝ) ↦ R₂ * (‖z - c‖ / c_1) ^ (n + 1)) (𝓝[<] R₁) (𝓝 (R₂ * (‖z - c‖ / R₁) ^ (n + 1)))

Tactic:
ContinuousAt.continuousWithinAt ?_

Premises used: ContinuousWithinAt, ContinuousAt.continuousWithinAt
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this_1 :
  ∀ {R₁ : ℝ} (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂))
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁)
    (hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂)),
    ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
this : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
refine : ContinuousAt (Y := ℝ) (fun (c_1 : ℝ) ↦ R₂ * (‖z - c‖ / c_1) ^ (n + 1)) R₁
⊢ Tendsto (fun (c_1 : ℝ) ↦ R₂ * (‖z - c‖ / c_1) ^ (n + 1)) (𝓝[<] R₁) (𝓝 (R₂ * (‖z - c‖ / R₁) ^ (n + 1)))

Tactic:
refine ContinuousAt.continuousWithinAt ?_

Premises used: ContinuousAt.continuousWithinAt