mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case convert_2
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
⊢ ProperSpace 𝕜

pp: case convert_5
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
x' : 𝕜
h : x' ∈ {0}ᶜ
⊢ x' ∈ ((fun x ↦ eval x (X ^ n)) '' {k | eval k (derivative (X ^ n)) = 0})ᶜ

Tactic:
·

Goal state after:
case convert_2
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
⊢ ProperSpace 𝕜
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case convert_5
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
x' : 𝕜
h : x' ∈ {0}ᶜ
⊢ x' ∈ ((fun x ↦ eval x (X ^ n)) '' {k | eval k (derivative (X ^ n)) = 0})ᶜ

Tactic:
·

Goal state after:
case convert_5
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
x' : 𝕜
h : x' ∈ {0}ᶜ
⊢ x' ∈ ((fun x ↦ eval x (X ^ n)) '' {k | eval k (derivative (X ^ n)) = 0})ᶜ
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑↑n ≠ 0
⊢ IsCoveringMap fun x ↦ ⟨↑x ^ ↑n, ⋯⟩

pp: case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
⊢ IsCoveringMap fun x ↦ ⟨↑x ^ (-↑n), ⋯⟩

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑↑n ≠ 0
⊢ IsCoveringMap fun x ↦ ⟨↑x ^ ↑n, ⋯⟩
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
⊢ IsCoveringMap fun x ↦ ⟨↑x ^ (-↑n), ⋯⟩

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
⊢ IsCoveringMap fun x ↦ ⟨↑x ^ (-↑n), ⋯⟩
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
⊢ IsCoveringMap fun x ↦ ⟨↑x ^ (-↑n), ⋯⟩

Tactic:
convert! (isCoveringMap_npow n _).comp_homeomorph (.inv₀ 𝕜)

Goal state after:
case e'_3
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
x✝ : { x // x ≠ 0 }
⊢ ↑x✝ ^ (-↑n) = ↑(((fun x ↦ ⟨↑x ^ n, ⋯⟩) ∘ ⇑(Homeomorph.inv₀ 𝕜)) x✝)

case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
⊢ ↑n ≠ 0
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case e'_3
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
x✝ : { x // x ≠ 0 }
⊢ ↑x✝ ^ (-↑n) = ↑(((fun x ↦ ⟨↑x ^ n, ⋯⟩) ∘ ⇑(Homeomorph.inv₀ 𝕜)) x✝)

pp: case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
⊢ ↑n ≠ 0

Tactic:
·

Goal state after:
case e'_3
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
x✝ : { x // x ≠ 0 }
⊢ ↑x✝ ^ (-↑n) = ↑(((fun x ↦ ⟨↑x ^ n, ⋯⟩) ∘ ⇑(Homeomorph.inv₀ 𝕜)) x✝)
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
⊢ ↑n ≠ 0

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
⊢ ↑n ≠ 0
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((fun x ↦ x ^ n) ⁻¹' {0}ᶜ)

pp: case refine_2
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ IsCoveringMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((fun x ↦ x ^ n) ⁻¹' {0}ᶜ)
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ IsCoveringMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
this : ∀ (x : 𝕜), x ^ n = 0 ↔ x = 0
⊢ IsCoveringMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr.refine_1
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
⊢ ∀ z ∈ frontier (ball c R₁), ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)

pp: case inr.refine_2
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
⊢ z ∈ closure (ball c R₁)

Tactic:
·

Goal state after:
case inr.refine_1
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
⊢ ∀ z ∈ frontier (ball c R₁), ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g // g ≠ 0 } := unitsHomeomorphNeZero
x✝ : 𝕜ˣ
⊢ x✝ ^ n = ((⇑e.symm ∘ {0}ᶜ.restrictPreimage fun x ↦ x ^ n) ∘ ⇑(e.trans (Homeomorph.ofEqSubtypes ?m.141))) x✝

pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g // g ≠ 0 } := unitsHomeomorphNeZero
⊢ (fun g ↦ g ≠ 0) = fun x ↦ x ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ

Tactic:
·

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g // g ≠ 0 } := unitsHomeomorphNeZero
x✝ : 𝕜ˣ
⊢ x✝ ^ n = ((⇑e.symm ∘ {0}ᶜ.restrictPreimage fun x ↦ x ^ n) ∘ ⇑(e.trans (Homeomorph.ofEqSubtypes ?m.141))) x✝
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g // g ≠ 0 } := unitsHomeomorphNeZero
⊢ (fun g ↦ g ≠ 0) = fun x ↦ x ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ

Tactic:
·

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
e : 𝕜ˣ ≃ₜ { g // g ≠ 0 } := unitsHomeomorphNeZero
⊢ (fun g ↦ g ≠ 0) = fun x ↦ x ∈ (fun x ↦ x ^ n) ⁻¹' {0}ᶜ
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝¹ : NeZero n
this✝ : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
this : IsQuotientMap fun x ↦ x ^ n
⊢ IsQuotientCoveringMap (fun x ↦ x ^ n) ↥(rootsOfUnity n 𝕜)

Tactic:
refine this.isQuotientCoveringMap_of_subgroup _
    (Set.Finite.isDiscrete <| inferInstanceAs (Finite (rootsOfUnity ..))) ?_

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝¹ : NeZero n
this✝ : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
this : IsQuotientMap fun x ↦ x ^ n
⊢ ∀ {e₁ e₂ : 𝕜ˣ}, e₁ ^ n = e₂ ^ n ↔ e₂ * e₁⁻¹ ∈ rootsOfUnity n 𝕜
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ ↑n
⊢ IsQuotientCoveringMap (fun x ↦ x ^ ↑n) ↥(zpowGroupHom ↑n).ker

pp: case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
⊢ IsQuotientCoveringMap (fun x ↦ x ^ (-↑n)) ↥(zpowGroupHom (-↑n)).ker

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ ↑n
⊢ IsQuotientCoveringMap (fun x ↦ x ^ ↑n) ↥(zpowGroupHom ↑n).ker
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr.refine_2
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
⊢ z ∈ closure (ball c R₁)

Tactic:
·

Goal state after:
case inr.refine_2
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
⊢ z ∈ closure (ball c R₁)
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
x✝ : 𝕜ˣ
⊢ x✝ ^ (-↑n) = (⇑(Homeomorph.inv 𝕜ˣ) ∘ fun x ↦ x ^ n) x✝

pp: case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
⊢ Function.Surjective fun x ↦ x ^ n

Tactic:
·

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑(-↑n) ≠ 0
surj : Function.Surjective fun x ↦ x ^ (-↑n)
x✝ : 𝕜ˣ
⊢ x✝ ^ (-↑n) = (⇑(Homeomorph.inv 𝕜ˣ) ∘ fun x ↦ x ^ n) x✝
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inl
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
heq : f z = f c
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)

pp: case inr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)

Tactic:
·

Goal state after:
case inl
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
heq : f z = f c
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
Module: Mathlib.Analysis.Complex.BranchLogRoot

Goal state before:
pp: case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
⊢ ContinuousOn (U.piecewise (fun x ↦ cexp (f x / ↑n)) fun x ↦ g x ^ (1 / ↑n)) U

pp: case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
z : X
⊢ U.piecewise (fun x ↦ cexp (f x / ↑n)) (fun x ↦ g x ^ (1 / ↑n)) z ^ n = g z

Tactic:
·

Goal state after:
case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
⊢ ContinuousOn (U.piecewise (fun x ↦ cexp (f x / ↑n)) fun x ↦ g x ^ (1 / ↑n)) U
Module: Mathlib.Analysis.Complex.BranchLogRoot

Goal state before:
pp: case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
z : X
⊢ U.piecewise (fun x ↦ cexp (f x / ↑n)) (fun x ↦ g x ^ (1 / ↑n)) z ^ n = g z

Tactic:
·

Goal state after:
case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
z : X
⊢ U.piecewise (fun x ↦ cexp (f x / ↑n)) (fun x ↦ g x ^ (1 / ↑n)) z ^ n = g z
Module: Mathlib.Analysis.Complex.BranchLogRoot

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
z : X
hz : z ∈ U
⊢ U.piecewise (fun x ↦ cexp (f x / ↑n)) (fun x ↦ g x ^ (1 / ↑n)) z ^ n = g z

pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
z : X
hz : z ∉ U
⊢ U.piecewise (fun x ↦ cexp (f x / ↑n)) (fun x ↦ g x ^ (1 / ↑n)) z ^ n = g z

Tactic:
·

Goal state after:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
z : X
hz : z ∈ U
⊢ U.piecewise (fun x ↦ cexp (f x / ↑n)) (fun x ↦ g x ^ (1 / ↑n)) z ^ n = g z
Module: Mathlib.Analysis.Complex.BranchLogRoot

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
z : X
hz : z ∉ U
⊢ U.piecewise (fun x ↦ cexp (f x / ↑n)) (fun x ↦ g x ^ (1 / ↑n)) z ^ n = g z

Tactic:
·

Goal state after:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
z : X
hz : z ∉ U
⊢ U.piecewise (fun x ↦ cexp (f x / ↑n)) (fun x ↦ g x ^ (1 / ↑n)) z ^ n = g z
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f ((lineMap c z) 0)) =o[𝓝 ((lineMap c z) 0)] fun w ↦ ‖w - (lineMap c z) 0‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : g (f z - f c) = ↑‖f z - f c‖
h : ℂ → ℂ := ⇑g ∘ f ∘ ⇑(lineMap c z)
hmaps_line : MapsTo (⇑(lineMap c z)) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ Tendsto (⇑(lineMap c z)) (𝓝 0) (𝓝 ((lineMap c z) 0))

pp: case refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f ((lineMap c z) 0)) =o[𝓝 ((lineMap c z) 0)] fun w ↦ ‖w - (lineMap c z) 0‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : g (f z - f c) = ↑‖f z - f c‖
h : ℂ → ℂ := ⇑g ∘ f ∘ ⇑(lineMap c z)
hmaps_line : MapsTo (⇑(lineMap c z)) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ ((fun w ↦ ‖w - (lineMap c z) 0‖ ^ n) ∘ ⇑(lineMap c z)) =O[𝓝 0] fun w ↦ w ^ n

Tactic:
·

Goal state after:
case refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f ((lineMap c z) 0)) =o[𝓝 ((lineMap c z) 0)] fun w ↦ ‖w - (lineMap c z) 0‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : g (f z - f c) = ↑‖f z - f c‖
h : ℂ → ℂ := ⇑g ∘ f ∘ ⇑(lineMap c z)
hmaps_line : MapsTo (⇑(lineMap c z)) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ Tendsto (⇑(lineMap c z)) (𝓝 0) (𝓝 ((lineMap c z) 0))
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f ((lineMap c z) 0)) =o[𝓝 ((lineMap c z) 0)] fun w ↦ ‖w - (lineMap c z) 0‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : g (f z - f c) = ↑‖f z - f c‖
h : ℂ → ℂ := ⇑g ∘ f ∘ ⇑(lineMap c z)
hmaps_line : MapsTo (⇑(lineMap c z)) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ ((fun w ↦ ‖w - (lineMap c z) 0‖ ^ n) ∘ ⇑(lineMap c z)) =O[𝓝 0] fun w ↦ w ^ n

Tactic:
·

Goal state after:
case refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f ((lineMap c z) 0)) =o[𝓝 ((lineMap c z) 0)] fun w ↦ ‖w - (lineMap c z) 0‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : g (f z - f c) = ↑‖f z - f c‖
h : ℂ → ℂ := ⇑g ∘ f ∘ ⇑(lineMap c z)
hmaps_line : MapsTo (⇑(lineMap c z)) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ ((fun w ↦ ‖w - (lineMap c z) 0‖ ^ n) ∘ ⇑(lineMap c z)) =O[𝓝 0] fun w ↦ w ^ n
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
⊢ Tendsto (fun n ↦ z ^ n) atTop (𝓝 0)

Tactic:
simp only [isEmbedding_coe.tendsto_nhds_iff, comp_def, coe_pow]

Goal state after:
z : 𝔻
⊢ Tendsto (fun x ↦ ↑z ^ ↑x) atTop (𝓝 ↑0)
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
R₁ R₂ : ℝ
f : E → F
c z : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
⊢ (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ ‖w - c‖ ^ 0

pp: case refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
R₁ R₂ : ℝ
f : E → F
c z : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
⊢ R₂ * (dist z c / R₁) ^ (0 + 1) = R₂ / R₁ * dist z c

Tactic:
·

Goal state after:
case refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
R₁ R₂ : ℝ
f : E → F
c z : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
⊢ (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ ‖w - c‖ ^ 0
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
R₁ R₂ : ℝ
f : E → F
c z : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
⊢ R₂ * (dist z c / R₁) ^ (0 + 1) = R₂ / R₁ * dist z c

Tactic:
·

Goal state after:
case refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
R₁ R₂ : ℝ
f : E → F
c z : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
⊢ R₂ * (dist z c / R₁) ^ (0 + 1) = R₂ / R₁ * dist z c
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f (ball z R₁)
h_maps : MapsTo f (ball z R₁) (closedBall (f z) R₂)
hz : z ∈ ball z R₁
⊢ ‖dslope f z z‖ ≤ R₂ / R₁

pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
·

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f (ball z R₁)
h_maps : MapsTo f (ball z R₁) (closedBall (f z) R₂)
hz : z ∈ ball z R₁
⊢ ‖dslope f z z‖ ≤ R₂ / R₁
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
·

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ ‖dslope f c z‖ ≤ R₂ / R₁