internlm/Lean-Github huggingface dataset:
Theorem: Super.ext_connected
Proof state before:
case h.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y✝ : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
y : ℂ × ℂ
n : y ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext}
⊢ y ∈ s.ext
Tactic:
simp only [mem_image, mem_setOf] at n
Proof state after:
case h.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y✝ : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
y : ℂ × ℂ
n : ∃ x, (c, x) ∈ s.ext ∧ (c, x) = y
⊢ y ∈ s.ext
Theorem: Super.ext_connected
Proof state before:
case h.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y✝ : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
y : ℂ × ℂ
n : ∃ x, (c, x) ∈ s.ext ∧ (c, x) = y
⊢ y ∈ s.ext
Tactic:
rcases n with ⟨x, m, e⟩
Proof state after:
case h.refine_1.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝¹ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y✝ : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x✝ : ℂ
m✝ : (c, x✝) ∈ s.ext
y : ℂ × ℂ
x : ℂ
m : (c, x) ∈ s.ext
e : (c, x) = y
⊢ y ∈ s.ext
Theorem: Super.ext_connected
Proof state before:
case h.refine_1.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝¹ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y✝ : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x✝ : ℂ
m✝ : (c, x✝) ∈ s.ext
y : ℂ × ℂ
x : ℂ
m : (c, x) ∈ s.ext
e : (c, x) = y
⊢ y ∈ s.ext
Tactic:
rw [e] at m
Proof state after:
case h.refine_1.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝¹ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y✝ : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x✝ : ℂ
m✝ : (c, x✝) ∈ s.ext
y : ℂ × ℂ
x : ℂ
m : y ∈ s.ext
e : (c, x) = y
⊢ y ∈ s.ext
Theorem: Super.ext_connected
Proof state before:
case h.refine_1.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝¹ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y✝ : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x✝ : ℂ
m✝ : (c, x✝) ∈ s.ext
y : ℂ × ℂ
x : ℂ
m : y ∈ s.ext
e : (c, x) = y
⊢ y ∈ s.ext
Tactic:
exact m
Proof state after:
no goals
Theorem: Super.ext_connected
Proof state before:
case h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ univ ×ˢ {0} ⊆ s.ext
Tactic:
intro ⟨c, x⟩ m
Proof state after:
case h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝¹ x✝¹ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c✝ x✝ : ℂ
m✝ : (c✝, x✝) ∈ s.ext
c x : ℂ
m : (c, x) ∈ univ ×ˢ {0}
⊢ (c, x) ∈ s.ext
Theorem: Super.ext_connected
Proof state before:
case h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝¹ x✝¹ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c✝ x✝ : ℂ
m✝ : (c✝, x✝) ∈ s.ext
c x : ℂ
m : (c, x) ∈ univ ×ˢ {0}
⊢ (c, x) ∈ s.ext
Tactic:
simp only [mem_prod_eq, mem_singleton_iff] at m
Proof state after:
case h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝¹ x✝¹ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c✝ x✝ : ℂ
m✝ : (c✝, x✝) ∈ s.ext
c x : ℂ
m : c ∈ univ ∧ x = 0
⊢ (c, x) ∈ s.ext
Theorem: Super.ext_connected
Proof state before:
case h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝¹ x✝¹ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c✝ x✝ : ℂ
m✝ : (c✝, x✝) ∈ s.ext
c x : ℂ
m : c ∈ univ ∧ x = 0
⊢ (c, x) ∈ s.ext
Tactic:
rw [m.2]
Proof state after:
case h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝¹ x✝¹ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c✝ x✝ : ℂ
m✝ : (c✝, x✝) ∈ s.ext
c x : ℂ
m : c ∈ univ ∧ x = 0
⊢ (c, 0) ∈ s.ext
Theorem: Super.ext_connected
Proof state before:
case h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝¹ x✝¹ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c✝ x✝ : ℂ
m✝ : (c✝, x✝) ∈ s.ext
c x : ℂ
m : c ∈ univ ∧ x = 0
⊢ (c, 0) ∈ s.ext
Tactic:
exact s.mem_ext c
Proof state after:
no goals
Theorem: Super.ext_connected
Proof state before:
case h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ (∃ x_1, (c, x_1) ∈ s.ext ∧ (c, x_1) = (c, x)) ∨ x = 0
Tactic:
left
Proof state after:
case h.refine_3.h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ ∃ x_1, (c, x_1) ∈ s.ext ∧ (c, x_1) = (c, x)
Theorem: Super.ext_connected
Proof state before:
case h.refine_3.h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ ∃ x_1, (c, x_1) ∈ s.ext ∧ (c, x_1) = (c, x)
Tactic:
exact ⟨x, m, rfl⟩
Proof state after:
no goals
Theorem: Super.ext_connected
Proof state before:
case h.refine_4
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0})
Tactic:
refine IsPreconnected.union (c, 0) ?_ ?_ ?_ ?_
Proof state after:
case h.refine_4.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ (c, 0) ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext}

case h.refine_4.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ (c, 0) ∈ univ ×ˢ {0}

case h.refine_4.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext})

case h.refine_4.refine_4
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ IsPreconnected (univ ×ˢ {0})
Theorem: Super.ext_connected
Proof state before:
case h.refine_4.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ (c, 0) ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext}
Tactic:
use 0, s.mem_ext c
Proof state after:
no goals
Theorem: Super.ext_connected
Proof state before:
case h.refine_4.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ (c, 0) ∈ univ ×ˢ {0}
Tactic:
exact mk_mem_prod (mem_univ _) rfl
Proof state after:
no goals
Theorem: Super.ext_connected
Proof state before:
case h.refine_4.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext})
Tactic:
exact IsPreconnected.image (s.ext_slice_connected c).isPreconnected _
  (Continuous.Prod.mk _).continuousOn
Proof state after:
no goals
Theorem: Super.ext_connected
Proof state before:
case h.refine_4.refine_4
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ IsPreconnected (univ ×ˢ {0})
Tactic:
exact isPreconnected_univ.prod isPreconnected_singleton
Proof state after:
no goals
Theorem: Super.ray_holomorphicOn
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ HolomorphicOn (I.prod I) I (uncurry s.ray) s.ext
Tactic:
intro ⟨c, x⟩ m
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ HolomorphicAt (I.prod I) I (uncurry s.ray) (c, x)
Theorem: Super.ray_holomorphicOn
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ HolomorphicAt (I.prod I) I (uncurry s.ray) (c, x)
Tactic:
exact s.ray_holomorphic m
Proof state after:
no goals
Theorem: Super.ray_post
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
⊢ (c, s.ray c x) ∈ s.post
Tactic:
simp only [Super.post, Postcritical, mem_setOf, s.ray_potential post]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
⊢ Complex.abs x < s.p c
Theorem: Super.ray_post
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
⊢ Complex.abs x < s.p c
Tactic:
exact post
Proof state after:
no goals
Theorem: Super.ray_noncritical_zero
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ mfderiv I I (s.ray c) 0 ≠ 0
Tactic:
have h : mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 ≠ 0 := by
  have e : s.bottcherNear c ∘ s.ray c =ᶠ[𝓝 0] id :=
    (continuousAt_const.prod continuousAt_id).eventually (s.ray_eqn_zero c)
  rw [e.mfderiv_eq]; exact id_mderiv_ne_zero
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 ≠ 0
⊢ mfderiv I I (s.ray c) 0 ≠ 0
Theorem: Super.ray_noncritical_zero
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 ≠ 0
⊢ mfderiv I I (s.ray c) 0 ≠ 0
Tactic:
contrapose h
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : ¬mfderiv I I (s.ray c) 0 ≠ 0
⊢ ¬mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 ≠ 0
Theorem: Super.ray_noncritical_zero
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : ¬mfderiv I I (s.ray c) 0 ≠ 0
⊢ ¬mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 ≠ 0
Tactic:
simp only [not_not] at h ⊢
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 = 0
Theorem: Super.ray_noncritical_zero
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 = 0
Tactic:
have hb : MDifferentiableAt I I (s.bottcherNear c) (s.ray c 0) := by
  rw [s.ray_zero]; exact (s.bottcherNear_holomorphic _ (s.mem_near c)).along_snd.mdifferentiableAt
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
hb : MDifferentiableAt I I (s.bottcherNear c) (s.ray c 0)
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 = 0
Theorem: Super.ray_noncritical_zero
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
hb : MDifferentiableAt I I (s.bottcherNear c) (s.ray c 0)
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 = 0
Tactic:
have hr : MDifferentiableAt I I (s.ray c) 0 :=
  (s.ray_holomorphic (s.mem_ext c)).along_snd.mdifferentiableAt
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
hb : MDifferentiableAt I I (s.bottcherNear c) (s.ray c 0)
hr : MDifferentiableAt I I (s.ray c) 0
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 = 0
Theorem: Super.ray_noncritical_zero
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
hb : MDifferentiableAt I I (s.bottcherNear c) (s.ray c 0)
hr : MDifferentiableAt I I (s.ray c) 0
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 = 0
Tactic:
rw [mfderiv_comp 0 hb hr, h, ContinuousLinearMap.comp_zero]
Proof state after:
no goals
Theorem: Super.ray_noncritical_zero
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 ≠ 0
Tactic:
have e : s.bottcherNear c ∘ s.ray c =ᶠ[𝓝 0] id :=
  (continuousAt_const.prod continuousAt_id).eventually (s.ray_eqn_zero c)
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
e : (𝓝 0).EventuallyEq (s.bottcherNear c ∘ s.ray c) id
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 ≠ 0
Theorem: Super.ray_noncritical_zero
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
e : (𝓝 0).EventuallyEq (s.bottcherNear c ∘ s.ray c) id
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 ≠ 0
Tactic:
rw [e.mfderiv_eq]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
e : (𝓝 0).EventuallyEq (s.bottcherNear c ∘ s.ray c) id
⊢ mfderiv I I id 0 ≠ 0
Theorem: Super.ray_noncritical_zero
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
e : (𝓝 0).EventuallyEq (s.bottcherNear c ∘ s.ray c) id
⊢ mfderiv I I id 0 ≠ 0
Tactic:
exact id_mderiv_ne_zero
Proof state after:
no goals
Theorem: Super.ray_noncritical_zero
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
⊢ MDifferentiableAt I I (s.bottcherNear c) (s.ray c 0)
Tactic:
rw [s.ray_zero]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
⊢ MDifferentiableAt I I (s.bottcherNear c) a
Theorem: Super.ray_noncritical_zero
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
⊢ MDifferentiableAt I I (s.bottcherNear c) a
Tactic:
exact (s.bottcherNear_holomorphic _ (s.mem_near c)).along_snd.mdifferentiableAt
Proof state after:
no goals
Theorem: Super.ray_noncritical
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
⊢ mfderiv I I (s.ray c) x ≠ 0
Tactic:
by_cases x0 : x = 0
Proof state after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0
Theorem: Super.ray_noncritical
Proof state before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0
Tactic:
rw [x0]
Proof state after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : x = 0
⊢ mfderiv I I (s.ray c) 0 ≠ 0

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0
Theorem: Super.ray_noncritical
Proof state before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : x = 0
⊢ mfderiv I I (s.ray c) 0 ≠ 0

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0
Tactic:
exact s.ray_noncritical_zero c
Proof state after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0