internlm/Lean-Github huggingface dataset:
Theorem: complex_inverse_fun'
Proof state before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
f' : ℂ → S → T := fun x z => f z
⊢ ∃ g, HolomorphicAt I I g (f z) ∧ (∀ᶠ (x : S) in 𝓝 z, g (f x) = x) ∧ ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
Tactic:
have fa' : HolomorphicAt II I (uncurry f') (0, z) := fa.comp_of_eq holomorphicAt_snd rfl
Proof state after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
f' : ℂ → S → T := fun x z => f z
fa' : HolomorphicAt (I.prod I) I (uncurry f') (0, z)
⊢ ∃ g, HolomorphicAt I I g (f z) ∧ (∀ᶠ (x : S) in 𝓝 z, g (f x) = x) ∧ ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
Theorem: complex_inverse_fun'
Proof state before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
f' : ℂ → S → T := fun x z => f z
fa' : HolomorphicAt (I.prod I) I (uncurry f') (0, z)
⊢ ∃ g, HolomorphicAt I I g (f z) ∧ (∀ᶠ (x : S) in 𝓝 z, g (f x) = x) ∧ ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
Tactic:
rcases complex_inverse_fun fa' nc with ⟨g, ga, gf, fg⟩
Proof state after:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
f' : ℂ → S → T := fun x z => f z
fa' : HolomorphicAt (I.prod I) I (uncurry f') (0, z)
g : ℂ → T → S
ga : HolomorphicAt (I.prod I) I (uncurry g) (0, f' 0 z)
gf : ∀ᶠ (x : ℂ × S) in 𝓝 (0, z), g x.1 (f' x.1 x.2) = x.2
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (0, f' 0 z), f' x.1 (g x.1 x.2) = x.2
⊢ ∃ g, HolomorphicAt I I g (f z) ∧ (∀ᶠ (x : S) in 𝓝 z, g (f x) = x) ∧ ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
Theorem: complex_inverse_fun'
Proof state before:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
f' : ℂ → S → T := fun x z => f z
fa' : HolomorphicAt (I.prod I) I (uncurry f') (0, z)
g : ℂ → T → S
ga : HolomorphicAt (I.prod I) I (uncurry g) (0, f' 0 z)
gf : ∀ᶠ (x : ℂ × S) in 𝓝 (0, z), g x.1 (f' x.1 x.2) = x.2
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (0, f' 0 z), f' x.1 (g x.1 x.2) = x.2
⊢ ∃ g, HolomorphicAt I I g (f z) ∧ (∀ᶠ (x : S) in 𝓝 z, g (f x) = x) ∧ ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
Tactic:
use g 0, ga.comp (holomorphicAt_const.prod holomorphicAt_id),
  (continuousAt_const.prod continuousAt_id).eventually gf,
  (continuousAt_const.prod continuousAt_id).eventually fg
Proof state after:
no goals
Theorem: mandelbrot_eq_multibrot
Proof state before:
⊢ mandelbrot = multibrot 2
Tactic:
ext c
Proof state after:
case h
c : ℂ
⊢ c ∈ mandelbrot ↔ c ∈ multibrot 2
Theorem: mandelbrot_eq_multibrot
Proof state before:
case h
c : ℂ
⊢ c ∈ mandelbrot ↔ c ∈ multibrot 2
Tactic:
simp only [mandelbrot, mem_setOf_eq, multibrot, f_f'_iter, tendsto_inf_iff_tendsto_atInf,
  tendsto_atInf_iff_norm_tendsto_atTop, Complex.norm_eq_abs]
Proof state after:
case h
c : ℂ
⊢ ¬Tendsto (fun n => Complex.abs ((fun z => z ^ 2 + c)^[n] c)) atTop atTop ↔
    ¬Tendsto (fun x => Complex.abs ((f' 2 c)^[x] c)) atTop atTop
Theorem: mandelbrot_eq_multibrot
Proof state before:
case h
c : ℂ
⊢ ¬Tendsto (fun n => Complex.abs ((fun z => z ^ 2 + c)^[n] c)) atTop atTop ↔
    ¬Tendsto (fun x => Complex.abs ((f' 2 c)^[x] c)) atTop atTop
Tactic:
rfl
Proof state after:
no goals
Theorem: isConnected_mandelbrot
Proof state before:
⊢ IsConnected mandelbrot
Tactic:
rw [mandelbrot_eq_multibrot]
Proof state after:
⊢ IsConnected (multibrot 2)
Theorem: isConnected_mandelbrot
Proof state before:
⊢ IsConnected (multibrot 2)
Tactic:
exact isConnected_multibrot 2
Proof state after:
no goals
Theorem: isConnected_compl_mandelbrot
Proof state before:
⊢ IsConnected mandelbrotᶜ
Tactic:
rw [mandelbrot_eq_multibrot]
Proof state after:
⊢ IsConnected (multibrot 2)ᶜ
Theorem: isConnected_compl_mandelbrot
Proof state before:
⊢ IsConnected (multibrot 2)ᶜ
Tactic:
exact isConnected_compl_multibrot 2
Proof state after:
no goals
Theorem: Super.ray_inv
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
⊢ ∃ b, HolomorphicOn (I.prod I) I (uncurry b) s.post ∧ ∀ y ∈ s.ext, b y.1 (s.ray y.1 y.2) = y.2
Tactic:
rw [← s.ray_bij.image_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
⊢ ∃ b,
    HolomorphicOn (I.prod I) I (uncurry b) ((fun y => (y.1, s.ray y.1 y.2)) '' s.ext) ∧
      ∀ y ∈ s.ext, b y.1 (s.ray y.1 y.2) = y.2
Theorem: Super.ray_inv
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
⊢ ∃ b,
    HolomorphicOn (I.prod I) I (uncurry b) ((fun y => (y.1, s.ray y.1 y.2)) '' s.ext) ∧
      ∀ y ∈ s.ext, b y.1 (s.ray y.1 y.2) = y.2
Tactic:
exact global_complex_inverse_fun_open s.ray_holomorphicOn (fun _ m ↦ s.ray_noncritical m)
    s.ray_bij.injOn s.isOpen_ext
Proof state after:
no goals
Theorem: Super.bottcher_eq_bottcherPost
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
m : (c, z) ∈ s.post
⊢ s.bottcher c z = s.bottcherPost c z
Tactic:
have h : ∃ n, (c, (f c)^[n] z) ∈ s.post := ⟨0, by simpa only [Function.iterate_zero_apply]⟩
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
m : (c, z) ∈ s.post
h : ∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ s.bottcher c z = s.bottcherPost c z
Theorem: Super.bottcher_eq_bottcherPost
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
m : (c, z) ∈ s.post
h : ∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ s.bottcher c z = s.bottcherPost c z
Tactic:
have h0 := (Nat.find_eq_zero h).mpr 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
m : (c, z) ∈ s.post
h : ∃ n, (c, (f c)^[n] z) ∈ s.post
h0 : Nat.find h = 0
⊢ s.bottcher c z = s.bottcherPost c z
Theorem: Super.bottcher_eq_bottcherPost
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
m : (c, z) ∈ s.post
h : ∃ n, (c, (f c)^[n] z) ∈ s.post
h0 : Nat.find h = 0
⊢ s.bottcher c z = s.bottcherPost c z
Tactic:
simp only [Super.bottcher, h, dif_pos, h0, Function.iterate_zero_apply, pow_zero, inv_one,
  Complex.cpow_one]
Proof state after:
no goals
Theorem: Super.bottcher_eq_bottcherPost
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
m : (c, z) ∈ s.post
⊢ (c, (f c)^[0] z) ∈ s.post
Tactic:
simpa only [Function.iterate_zero_apply]
Proof state after:
no goals
Theorem: Super.bottcher_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.bottcher) s.post
Tactic:
intro ⟨c, z⟩ 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 : ℂ
z : S
m : (c, z) ∈ s.post
⊢ HolomorphicAt (I.prod I) I (uncurry s.bottcher) (c, z)
Theorem: Super.bottcher_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 : ℂ
z : S
m : (c, z) ∈ s.post
⊢ HolomorphicAt (I.prod I) I (uncurry s.bottcher) (c, z)
Tactic:
apply ((choose_spec s.ray_inv).1 _ m).congr
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 : ℂ
z : S
m : (c, z) ∈ s.post
⊢ (𝓝 (c, z)).EventuallyEq (uncurry (choose ⋯)) (uncurry s.bottcher)
Theorem: Super.bottcher_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 : ℂ
z : S
m : (c, z) ∈ s.post
⊢ (𝓝 (c, z)).EventuallyEq (uncurry (choose ⋯)) (uncurry s.bottcher)
Tactic:
exact s.eqOn_bottcher_bottcherPost.symm.eventuallyEq_of_mem (s.isOpen_post.mem_nhds m)
Proof state after:
no goals
Theorem: Super.bottcher_ray
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
m : (c, x) ∈ s.ext
⊢ s.bottcher c (s.ray c x) = x
Tactic:
rw [s.bottcher_eq_bottcherPost (s.ray_post 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
m : (c, x) ∈ s.ext
⊢ s.bottcherPost c (s.ray c x) = x
Theorem: Super.bottcher_ray
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
m : (c, x) ∈ s.ext
⊢ s.bottcherPost c (s.ray c x) = x
Tactic:
exact (choose_spec s.ray_inv).2 _ m
Proof state after:
no goals
Theorem: Super.ray_bottcher
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
m : (c, z) ∈ s.post
⊢ s.ray c (s.bottcher c z) = z
Tactic:
rcases s.ray_surj m with ⟨x, m, e⟩
Proof state after:
case 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
m✝ : (c, z) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = z
⊢ s.ray c (s.bottcher c z) = z
Theorem: Super.ray_bottcher
Proof state before:
case 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
m✝ : (c, z) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = z
⊢ s.ray c (s.bottcher c z) = z
Tactic:
rw [← e, s.bottcher_ray m]
Proof state after:
no goals
Theorem: Super.bottcher_ext
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
m : (c, z) ∈ s.post
⊢ (c, s.bottcher c z) ∈ s.ext
Tactic:
rcases s.ray_surj m with ⟨x, m, e⟩
Proof state after:
case 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
m✝ : (c, z) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = z
⊢ (c, s.bottcher c z) ∈ s.ext
Theorem: Super.bottcher_ext
Proof state before:
case 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
m✝ : (c, z) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = z
⊢ (c, s.bottcher c z) ∈ s.ext
Tactic:
rw [← e, s.bottcher_ray m]
Proof state after:
case 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
m✝ : (c, z) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = z
⊢ (c, x) ∈ s.ext
Theorem: Super.bottcher_ext
Proof state before:
case 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
m✝ : (c, z) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = z
⊢ (c, x) ∈ s.ext
Tactic:
exact m
Proof state after:
no goals
Theorem: Super.bottcher_eq_bottcherNear
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 : ℂ
⊢ ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
Tactic:
have eq := (s.ray_nontrivial (s.mem_ext c)).nhds_eq_map_nhds
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 : ℂ
eq : 𝓝 (s.ray c 0) = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
Theorem: Super.bottcher_eq_bottcherNear
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 : ℂ
eq : 𝓝 (s.ray c 0) = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
Tactic:
simp only [s.ray_zero] at 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 : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
Theorem: Super.bottcher_eq_bottcherNear
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 : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
Tactic:
simp only [eq, Filter.eventually_map]
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 : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (a_1 : ℂ) in 𝓝 0, s.bottcher c (s.ray c a_1) = s.bottcherNear c (s.ray c a_1)
Theorem: Super.bottcher_eq_bottcherNear
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 : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (a_1 : ℂ) in 𝓝 0, s.bottcher c (s.ray c a_1) = s.bottcherNear c (s.ray c a_1)
Tactic:
apply ((continuousAt_const.prod continuousAt_id).eventually (s.ray_eqn_zero c)).mp
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 : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (x : ℂ) in 𝓝 0,
    s.bottcherNear (c, id x).1 (s.ray (c, id x).1 (c, id x).2) = (c, id x).2 →
      s.bottcher c (s.ray c x) = s.bottcherNear c (s.ray c x)
Theorem: Super.bottcher_eq_bottcherNear
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 : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (x : ℂ) in 𝓝 0,
    s.bottcherNear (c, id x).1 (s.ray (c, id x).1 (c, id x).2) = (c, id x).2 →
      s.bottcher c (s.ray c x) = s.bottcherNear c (s.ray c x)
Tactic:
refine ((s.isOpen_ext.snd_preimage c).eventually_mem (s.mem_ext c)).mp
  (eventually_of_forall fun z m e ↦ ?_)
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 : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
z : ℂ
m : z ∈ {b | (c, b) ∈ s.ext}
e : s.bottcherNear (c, id z).1 (s.ray (c, id z).1 (c, id z).2) = (c, id z).2
⊢ s.bottcher c (s.ray c z) = s.bottcherNear c (s.ray c z)
Theorem: Super.bottcher_eq_bottcherNear
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 : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
z : ℂ
m : z ∈ {b | (c, b) ∈ s.ext}
e : s.bottcherNear (c, id z).1 (s.ray (c, id z).1 (c, id z).2) = (c, id z).2
⊢ s.bottcher c (s.ray c z) = s.bottcherNear c (s.ray c z)
Tactic:
simp only [s.bottcher_ray 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 : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
z : ℂ
m : z ∈ {b | (c, b) ∈ s.ext}
e : s.bottcherNear (c, id z).1 (s.ray (c, id z).1 (c, id z).2) = (c, id z).2
⊢ z = s.bottcherNear c (s.ray c z)
Theorem: Super.bottcher_eq_bottcherNear
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 : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
z : ℂ
m : z ∈ {b | (c, b) ∈ s.ext}
e : s.bottcherNear (c, id z).1 (s.ray (c, id z).1 (c, id z).2) = (c, id z).2
⊢ z = s.bottcherNear c (s.ray c z)
Tactic:
exact e.symm
Proof state after:
no goals
Theorem: Super.post_connected
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
⊢ IsConnected s.post
Tactic:
have e : s.post = s.homeomorph '' s.ext := s.homeomorph.image_source_eq_target.symm
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
e : s.post = ↑s.homeomorph '' s.ext
⊢ IsConnected s.post
Theorem: Super.post_connected
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
e : s.post = ↑s.homeomorph '' s.ext
⊢ IsConnected s.post
Tactic:
rw [e]
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
e : s.post = ↑s.homeomorph '' s.ext
⊢ IsConnected (↑s.homeomorph '' s.ext)
Theorem: Super.post_connected
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
e : s.post = ↑s.homeomorph '' s.ext
⊢ IsConnected (↑s.homeomorph '' s.ext)
Tactic:
exact s.ext_connected.image _ s.homeomorph.continuousOn
Proof state after:
no goals
Theorem: Super.post_slice_connected
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 : ℂ
⊢ IsConnected {z | (c, z) ∈ s.post}
Tactic:
have e : {z | (c, z) ∈ s.post} = s.homeomorphSlice c '' {x | (c, x) ∈ s.ext} :=
  (s.homeomorphSlice c).image_source_eq_target.symm
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 : {z | (c, z) ∈ s.post} = ↑(s.homeomorphSlice c) '' {x | (c, x) ∈ s.ext}
⊢ IsConnected {z | (c, z) ∈ s.post}