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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
p : 𝕜[X]
x : 𝕜
hx : x ∈ ((fun x ↦ eval x p) '' {k | eval k (derivative p) = 0})ᶜ
ne : p ≠ C x
⊢ ((fun x ↦ eval x p) ⁻¹' {x}).Finite

Tactic:
simpa using

Goal state after:
case inr
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
p : 𝕜[X]
x : 𝕜
hx : x ∈ ((fun x ↦ eval x p) '' {k | eval k (derivative p) = 0})ᶜ
ne : p ≠ C x
⊢ ((p - C x).rootSet 𝕜).Finite
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:
simpa using

Goal state after:
case convert_5
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
x' : 𝕜
h : x' ∈ {0}ᶜ
⊢ ¬n - 1 = 0 → ¬0 = 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:
simpa using

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

Goal state before:
pp: 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₁)
this : ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
⊢ ‖z - c‖ ≠ 0

Tactic:
simpa using

Goal state after:
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₁)
this : ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
⊢ ¬z = c
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: 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₁)
this : ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
hz' : ‖z - c‖ ≠ 0
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
simpa using

Goal state after:
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₁)
this : ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
hz' : ‖z - c‖ ≠ 0
⊢ ‖f z - f c‖ * R₁ ^ (n + 1) ≤ R₂ * ‖z - c‖ ^ (n + 1)
Module: Mathlib.Analysis.Normed.Module.Ball.Action

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜' E
r : ℝ
c : ↑(closedBall 0 1)
x : ↑(ball 0 r)
⊢ ‖↑c • ↑x‖ < r

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜' E
r : ℝ
c : ↑(closedBall 0 1)
x : ↑(ball 0 r)
⊢ ‖↑c‖ * ‖↑x‖ < r
Module: Mathlib.Analysis.Normed.Module.Ball.Action

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜' E
r : ℝ
c : ↑(closedBall 0 1)
x : ↑(closedBall 0 r)
⊢ ‖↑c • ↑x‖ ≤ r

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜' E
r : ℝ
c : ↑(closedBall 0 1)
x : ↑(closedBall 0 r)
⊢ ‖↑c‖ * ‖↑x‖ ≤ r
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: 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₁)
w : ℂ
hw : w ∈ sphere c R₁
hwc : w ≠ c
⊢ ‖f w - f c‖ ≤ R₂

Tactic:
simpa using

Goal state after:
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₁)
w : ℂ
hw : w ∈ sphere c R₁
hwc : w ≠ c
⊢ ‖f w - f 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
⊢ Function.Surjective fun x ↦ x ^ n

Tactic:
simpa using

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

Goal state before:
pp: 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
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)
w : ℂ
hw : w ∈ ball 0 (R₁ / dist z c)
⊢ (lineMap c z) w ∈ ball c R₁

Tactic:
simpa using

Goal state after:
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
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)
w : ℂ
hw : w ∈ ball 0 (R₁ / dist z c)
⊢ ‖w‖ * dist z c < R₁
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: 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
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₁)
⊢ MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)

Tactic:
refine MapsTo.comp ?_ (h_maps.comp hmaps_line)

Goal state after:
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
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₁)
⊢ MapsTo (⇑g) (closedBall (f c) R₂) (closedBall (h 0) R₂)
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: 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
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₁)
⊢ MapsTo (⇑g) (closedBall (f c) R₂) (closedBall (h 0) R₂)

Tactic:
simpa using

Goal state after:
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
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₁)
⊢ MapsTo (⇑g) (closedBall (f c) R₂) (closedBall (g (f c)) R₂)
Module: Mathlib.Analysis.Complex.BranchLogRoot

Goal state before:
pp: 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
this✝ : SimplyConnectedSpace ↑U
this : LocallyPathConnectedSpace ↑U
x₀ : { x // x ∈ U }
hx₀ : g✝ ↑x₀ ≠ 0
f : C(↑U, ℂ)
hf : cexp ∘ ⇑f = ⇑{ toFun := U.domRestrict g✝, continuous_toFun := ⋯ }
g : X → ℂ
hg : ∀ (z : ↑U), g ↑z = f z
x : { x // x ∈ U }
⊢ (cexp ∘ g) ↑x = g✝ ↑x

Tactic:
simpa using

Goal state after:
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
this✝ : SimplyConnectedSpace ↑U
this : LocallyPathConnectedSpace ↑U
x₀ : { x // x ∈ U }
hx₀ : g✝ ↑x₀ ≠ 0
f : C(↑U, ℂ)
hf : cexp ∘ ⇑f = ⇑{ toFun := U.domRestrict g✝, continuous_toFun := ⋯ }
g : X → ℂ
hg : ∀ (z : ↑U), g ↑z = f z
x : { x // x ∈ U }
⊢ cexp (f x) = g✝ ↑x
Module: Mathlib.Analysis.Complex.BranchLogRoot

Goal state before:
pp: 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 : ℕ+
⊢ 0 ∉ UnitDisc.coe ∘ g '' U

Tactic:
simpa using

Goal state after:
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 : ℕ+
⊢ ∀ x ∈ U, ¬g x = 0
Module: Mathlib.Analysis.Complex.BranchLogRoot

Goal state before:
pp: 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 : ℕ+
f : X → 𝔻
hfc : ContinuousOn (fun i ↦ ↑(f i)) U
hf : ∀ (x : X), (fun i ↦ ↑(f i)) x ^ ↑n = (UnitDisc.coe ∘ g) x
x : X
⊢ f x ^ n = g x

Tactic:
simpa using

Goal state after:
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 : ℕ+
f : X → 𝔻
hfc : ContinuousOn (fun i ↦ ↑(f i)) U
hf : ∀ (x : X), (fun i ↦ ↑(f i)) x ^ ↑n = (UnitDisc.coe ∘ g) x
x : X
⊢ f x ^ n = g x
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:
simpa using

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 x ↦ dist c z ^ n * ‖x‖ ^ n) =O[𝓝 0] fun w ↦ w ^ n
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
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
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : g (f z) - g (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))
hn : (fun x ↦ h x - h 0) =o[𝓝 0] fun w ↦ (w - 0) ^ n
hmem : 1 ∈ ball 0 (R₁ / dist z c)
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)

Tactic:
simpa using

Goal state after:
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
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : g (f z) - g (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))
hn : (fun x ↦ h x - h 0) =o[𝓝 0] fun w ↦ (w - 0) ^ n
hmem : 1 ∈ ball 0 (R₁ / dist z c)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
⊢ ‖↑z‖ ≠ ‖-1‖

Tactic:
simpa using

Goal state after:
z : 𝔻
⊢ ¬‖↑z‖ = 1
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

Tactic:
simpa using

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₁
⊢ Tendsto (fun x ↦ f x - f c) (𝓝 c) (𝓝 0)
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: 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 : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
this : 0 ≤ R₂
z : E
hz : z ∈ ball c R₁
⊢ ‖f z - f c‖ ≤ R₂ / R₁ * ‖z - c‖

Tactic:
simpa using

Goal state after:
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 : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
this : 0 ≤ R₂
z : E
hz : z ∈ ball c R₁
⊢ ‖f z - f c‖ ≤ R₂ / R₁ * ‖z - c‖
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
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
⊢ dist (f z) (f c) ≤ dist z c

Tactic:
simpa using

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
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
⊢ dist (f z) (f c) ≤ dist z c
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
R : ℝ
f : E → F
c : E
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (closedBall (f c) R)
hR : 0 < R
⊢ ‖fderiv ℂ f c‖ ≤ 1

Tactic:
simpa using

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
R : ℝ
f : E → F
c : E
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (closedBall (f c) R)
hR : 0 < R
⊢ ‖fderiv ℂ f c‖ ≤ 1
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
R : ℝ
f : E → F
z : E
hd : DifferentiableOn ℂ f (ball 0 R)
h_maps : MapsTo f (ball 0 R) (closedBall 0 R)
h₀ : f 0 = 0
hz : ‖z‖ < R
⊢ ‖f z‖ ≤ ‖z‖

Tactic:
simpa using

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
R : ℝ
f : E → F
z : E
hd : DifferentiableOn ℂ f (ball 0 R)
h_maps : MapsTo f (ball 0 R) (closedBall 0 R)
h₀ : f 0 = 0
hz : ‖z‖ < R
⊢ ‖f z‖ ≤ ‖z‖
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₁

Tactic:
simpa using

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₁
⊢ ‖deriv f z‖ ≤ R₂ / R₁
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: 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₁
⊢ 0 < R₁

Tactic:
simpa using

Goal state after:
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₁
⊢ 0 < R₁
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope (⇑e ∘ f) c
z✝ : ℂ
hz✝ : z✝ ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = ⇑e ∘ dslope f c
z : ℂ
hz : z ∈ ball c R₁
w : ℂ
hw : w ∈ ball c R₁
⊢ (⇑e ∘ f) w ∈ closedBall ((⇑e ∘ f) c) R₂

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope (⇑e ∘ f) c
z✝ : ℂ
hz✝ : z✝ ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = ⇑e ∘ dslope f c
z : ℂ
hz : z ∈ ball c R₁
w : ℂ
hw : w ∈ ball c R₁
⊢ dist (f w) (f c) ≤ R₂
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope (⇑e ∘ f) c
z✝ : ℂ
hz✝ : z✝ ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = ⇑e ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
⊢ (norm ∘ g) z ≤ (norm ∘ g) z₀

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope (⇑e ∘ f) c
z✝ : ℂ
hz✝ : z✝ ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = ⇑e ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope (⇑e ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = ⇑e ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
⊢ ‖dslope f c z‖ = ‖dslope f c z₀‖

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope (⇑e ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = ⇑e ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
⊢ ‖dslope f c z‖ = ‖dslope f c z₀‖