awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a : ℂ
ha : a ∉ U
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
have this₁ : ∃ (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])
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
have 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
Tactic: rcases this with ⟨f, hf_inj, hf_dense, hdf⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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
have inr : ¬Dense ((f ∘ fun (x : ℂ) ↦ -a + x) '' U)
Tactic: refine ⟨f ∘ (-a + ·), hf_inj.comp (add_right_injective (-a)), ?_, 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
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)
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
have inr₁ : ∀ (z : ℂ) (hz : z ∈ U), deriv (f ∘ fun (x : ℂ) ↦ -a + x) z ≠ 0
Tactic: refine ⟨f ∘ (-a + ·), hf_inj.comp (add_right_injective (-a)), ?_, 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
hU₀ : 0 ∉ U
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
have 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
Tactic: rcases exists_continuousOn_pow_eq hUc hUo continuousOn_id (by rwa [image_id]) two_ne_zero
    with ⟨f, hfc, hf_inv⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (hypothesis)
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
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
have hf_inv₁ : LeftInverse (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) f
Tactic: replace hf_inv : LeftInverse (· ^ 2) f := hf_inv
Cleared hypotheses: hf_inv
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (hypothesis)
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
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
have hf₀ : ∀ 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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 f (2 * f z)⁻¹ z
have hg : ContinuousAt f z
Tactic: apply HasStrictDerivAt.of_local_left_inverse
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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
⊢ HasStrictDerivAt f (2 * f z)⁻¹ z
have hf : HasStrictDerivAt (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) (2 * f z) (f z)
Tactic: apply HasStrictDerivAt.of_local_left_inverse
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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)
⊢ HasStrictDerivAt f (2 * f z)⁻¹ z
have hf' : 2 * f z ≠ 0
Tactic: apply HasStrictDerivAt.of_local_left_inverse
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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
⊢ HasStrictDerivAt f (2 * f z)⁻¹ z
have hfg : ∀ᶠ (y : ℂ) in 𝓝 z, HPow.hPow (β := ℕ) (f y) 2 = y
Tactic: apply HasStrictDerivAt.of_local_left_inverse
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (hypothesis)
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
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
have hdf : ∀ 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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
have refine_1 : ¬Dense (f '' U)
Tactic: refine ⟨f, hf_inv.injective, ?_, 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
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)
⊢ ∃ (f : ℂ → ℂ), Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
have refine_2 : ∀ (z : ℂ) (hz : z ∈ U), deriv f z ≠ 0
Tactic: refine ⟨f, hf_inv.injective, ?_, 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
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
⊢ ¬Dense (f '' U)
have refine_1 : ∃ (x : ℂ), ∀ᶠ (x : ℂ) in 𝓝 x, x ∉ f '' U
Tactic: simp only [Dense, not_forall, mem_closure_iff_frequently, not_frequently]
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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 : ℂ), ∀ᶠ (x : ℂ) in 𝓝 x, x ∉ f '' U
have refine_1 : ∀ (x : ℂ) (hx : x ∈ U), ∃ (x : ℂ), ∀ᶠ (x : ℂ) in 𝓝 x, x ∉ f '' U
Tactic: rcases hUc.nonempty with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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
⊢ ∃ (x : ℂ), ∀ᶠ (x : ℂ) in 𝓝 x, x ∉ f '' U
have h : ∀ᶠ (x : ℂ) in 𝓝 (-f x), x ∉ f '' U
Tactic: use -f x
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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)
have rw : f '' U ∈ map f (𝓝 x)
Tactic: rw [← (hdf x hx).map_nhds_eq (by simpa using hf₀ x hx)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (hypothesis)
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
⊢ ∀ᶠ (x : ℂ) in 𝓝 (-f x), x ∉ f '' U
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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)
⊢ ∀ᶠ (x : ℂ) in 𝓝 (-f x), x ∉ f '' U
have h : ∀ᶠ (x : ℂ) in 𝓝 (f x), -x ∉ f '' U
Tactic: rw [nhds_neg, eventually_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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)
⊢ ∀ᶠ (x : ℂ) in 𝓝 (f x), -x ∉ f '' U
have h : ∀ a ∈ f '' U, -a ∉ f '' U
Tactic: filter_upwards [this]
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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 = b
have rw : a = (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) x 2) (-f a)
Tactic: rw [← hf_inv b, hab]
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (hypothesis)
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
⊢ False
have hab₁ : f a = -f a
Tactic: obtain rfl : a = b := by
      rw [← hf_inv b, hab]
      simp [hf_inv a]
Cleared hypotheses: b, hb, hab
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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
have h : f a = 0
Tactic: refine hf₀ a ha ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
Goal:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
⊢ ∃ (f : ℂ → ℂ), MapsTo f U (ball 0 1) ∧ InjOn f U ∧ ∀ z ∈ U, deriv f z ≠ 0
have 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
Tactic: rcases exists_injective_not_dense_image_deriv_ne_zero hUo hUc hU with ⟨f, hf_inj, hfd, hdf⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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
⊢ ∃ (f : ℂ → ℂ), MapsTo f U (ball 0 1) ∧ InjOn f U ∧ ∀ z ∈ U, deriv f z ≠ 0
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (hypothesis)
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
⊢ ∃ (f : ℂ → ℂ), MapsTo f U (ball 0 1) ∧ InjOn f U ∧ ∀ z ∈ U, deriv f z ≠ 0
have hfx : ∀ z ∈ U, f z ≠ x
Tactic: have hfx : ∀ z ∈ U, f z ≠ x := fun z hz ↦ by simpa using hε₀.trans (hε 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 : ℂ → ℂ
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
⊢ ∃ (f : ℂ → ℂ), MapsTo f U (ball 0 1) ∧ InjOn f U ∧ ∀ z ∈ U, deriv f z ≠ 0
have 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
Tactic: use fun z ↦ ε / (f z - x)
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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
have refine : MapsTo (β := ℂ) (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) U (ball 0 1)
Tactic: refine ⟨?mapsTo, ?injOn, ?deriv⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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)
⊢ 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
have refine₁ : InjOn (β := ℂ) (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) U
Tactic: refine ⟨?mapsTo, ?injOn, ?deriv⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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
⊢ 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
have refine₂ : ∀ z ∈ U, Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z) 0
Tactic: refine ⟨?mapsTo, ?injOn, ?deriv⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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
⊢ Membership.mem (γ := Set ℂ) (ball 0 1) ((fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z)
have rw : ε < ‖f z - x‖
Tactic: rw [mem_ball_zero_iff, norm_div, norm_real, Real.norm_of_nonneg hε₀.le, div_lt_one₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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‖
⊢ Membership.mem (γ := Set ℂ) (ball 0 1) ((fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z)
have rw₁ : 0 < ‖f z - x‖
Tactic: rw [mem_ball_zero_iff, norm_div, norm_real, Real.norm_of_nonneg hε₀.le, div_lt_one₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (hypothesis)
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
⊢ Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z) 0
have hdz : DifferentiableAt ℂ f z
Tactic: have hdz : DifferentiableAt ℂ f z := differentiableAt_of_deriv_ne_zero (hdf 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 : ℂ → ℂ
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
⊢ Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z) 0
have rw : (0 * (f z - x) - (↑ε : ℂ) * deriv f z) / HPow.hPow (β := ℕ) (f z - x) 2 ≠ 0
Tactic: rw [(hasDerivAt_const _ _).fun_div (hdz.hasDerivAt.sub_const _) _ |>.deriv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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
⊢ Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z) 0
have rw₁ : f z - x ≠ 0
Tactic: rw [(hasDerivAt_const _ _).fun_div (hdz.hasDerivAt.sub_const _) _ |>.deriv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.RiemannMapping (goal)
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
⊢ ∀ z ∈ U, Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑ε : ℂ) / (f z - x)) z) 0
have case₂ : ∀ (z : ℂ) (hz : z ∈ U) (hdz : DifferentiableAt ℂ f z), 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
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₁
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
have hR₁ : 0 < R₁
Tactic: have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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₁
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
have 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)
Tactic: wlog hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧
    MapsTo f (closedBall c R₁) (closedBall (f c) R₂) generalizing R₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
have 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)
Tactic: wlog hd' : DifferentiableOn ℂ f (closedBall c R₁) ∧
    MapsTo f (closedBall c R₁) (closedBall (f c) R₂) generalizing R₁
Cleared hypotheses: R₁, hd, h_maps, hz, hR₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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)
have refine : Tendsto (fun (c_1 : ℝ) ↦ R₂ * (‖z - c‖ / c_1) ^ (n + 1)) (𝓝[<] R₁) (𝓝 (R₂ * (‖z - c‖ / R₁) ^ (n + 1)))
Tactic: refine ge_of_tendsto ?_ this