internlm/Lean-Github huggingface dataset:
Theorem: Super.fp2
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 : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
p : ℂ × S
⊢ (s.fp^[n] p).2 = (f p.1)^[n] p.2
Tactic:
induction' n with n h
Proof state after:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
⊢ (s.fp^[0] p).2 = (f p.1)^[0] p.2

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
p : ℂ × S
n : ℕ
h : (s.fp^[n] p).2 = (f p.1)^[n] p.2
⊢ (s.fp^[n + 1] p).2 = (f p.1)^[n + 1] p.2
Theorem: Super.fp2
Proof state before:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
⊢ (s.fp^[0] p).2 = (f p.1)^[0] p.2
Tactic:
simp only [Function.iterate_zero_apply]
Proof state after:
no goals
Theorem: Super.fp2
Proof state before:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
p : ℂ × S
n : ℕ
h : (s.fp^[n] p).2 = (f p.1)^[n] p.2
⊢ (s.fp^[n + 1] p).2 = (f p.1)^[n + 1] p.2
Tactic:
have c := s.fp1 n p
Proof state after:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
p : ℂ × S
n : ℕ
h : (s.fp^[n] p).2 = (f p.1)^[n] p.2
c : (s.fp^[n] p).1 = p.1
⊢ (s.fp^[n + 1] p).2 = (f p.1)^[n + 1] p.2
Theorem: Super.fp2
Proof state before:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
p : ℂ × S
n : ℕ
h : (s.fp^[n] p).2 = (f p.1)^[n] p.2
c : (s.fp^[n] p).1 = p.1
⊢ (s.fp^[n + 1] p).2 = (f p.1)^[n + 1] p.2
Tactic:
simp only [Function.iterate_succ_apply', c, h, fp]
Proof state after:
no goals
Theorem: Super.bottcherNear_holomorphic
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ HolomorphicOn (I.prod I) I (uncurry s.bottcherNear) s.near
Tactic:
intro p 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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
⊢ HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) p
Theorem: Super.bottcherNear_holomorphic
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
⊢ HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) p
Tactic:
have e : uncurry s.bottcherNear =
    (fun p : ℂ × ℂ ↦ _root_.bottcherNear (s.fl p.1) d p.2) ∘ fun p : ℂ × S ↦
      (p.1, extChartAt I a p.2 - extChartAt I a a) :=
  rfl
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
e :
  uncurry s.bottcherNear =
    (fun p => _root_.bottcherNear (s.fl p.1) d p.2) ∘ fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) p
Theorem: Super.bottcherNear_holomorphic
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
e :
  uncurry s.bottcherNear =
    (fun p => _root_.bottcherNear (s.fl p.1) d p.2) ∘ fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) p
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
e :
  uncurry s.bottcherNear =
    (fun p => _root_.bottcherNear (s.fl p.1) d p.2) ∘ fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) I
    ((fun p => _root_.bottcherNear (s.fl p.1) d p.2) ∘ fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p
Theorem: Super.bottcherNear_holomorphic
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
e :
  uncurry s.bottcherNear =
    (fun p => _root_.bottcherNear (s.fl p.1) d p.2) ∘ fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) I
    ((fun p => _root_.bottcherNear (s.fl p.1) d p.2) ∘ fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p
Tactic:
clear 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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
⊢ HolomorphicAt (I.prod I) I
    ((fun p => _root_.bottcherNear (s.fl p.1) d p.2) ∘ fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p
Theorem: Super.bottcherNear_holomorphic
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
⊢ HolomorphicAt (I.prod I) I
    ((fun p => _root_.bottcherNear (s.fl p.1) d p.2) ∘ fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p
Tactic:
have h1 := (bottcherNear_analytic s.superNearC _ (s.mem_near_to_near' m)).holomorphicAt II I
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) I
    ((fun p => _root_.bottcherNear (s.fl p.1) d p.2) ∘ fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p
Theorem: Super.bottcherNear_holomorphic
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) I
    ((fun p => _root_.bottcherNear (s.fl p.1) d p.2) ∘ fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p
Tactic:
have h2 : HolomorphicAt II II (fun p : ℂ × S ↦
    (p.1, extChartAt I a p.2 - extChartAt I a a)) p := by
  apply holomorphicAt_fst.prod; apply HolomorphicAt.sub
  exact (HolomorphicAt.extChartAt (s.near_subset_chart m)).comp holomorphicAt_snd
  exact holomorphicAt_const
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
h2 : HolomorphicAt (I.prod I) (I.prod I) (fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p
⊢ HolomorphicAt (I.prod I) I
    ((fun p => _root_.bottcherNear (s.fl p.1) d p.2) ∘ fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p
Theorem: Super.bottcherNear_holomorphic
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
h2 : HolomorphicAt (I.prod I) (I.prod I) (fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p
⊢ HolomorphicAt (I.prod I) I
    ((fun p => _root_.bottcherNear (s.fl p.1) d p.2) ∘ fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p
Tactic:
refine h1.comp_of_eq h2 ?_
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
h2 : HolomorphicAt (I.prod I) (I.prod I) (fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p
⊢ (fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p = (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
Theorem: Super.bottcherNear_holomorphic
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
h2 : HolomorphicAt (I.prod I) (I.prod I) (fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p
⊢ (fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p = (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
Tactic:
simp only [sub_self]
Proof state after:
no goals
Theorem: Super.bottcherNear_holomorphic
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) (I.prod I) (fun p => (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)) p
Tactic:
apply holomorphicAt_fst.prod
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a) p
Theorem: Super.bottcherNear_holomorphic
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(extChartAt I a) x.2 - ↑(extChartAt I a) a) p
Tactic:
apply HolomorphicAt.sub
Proof state after:
case fa
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(extChartAt I a) x.2) p

case ga
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(extChartAt I a) a) p
Theorem: Super.bottcherNear_holomorphic
Proof state before:
case fa
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(extChartAt I a) x.2) p

case ga
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(extChartAt I a) a) p
Tactic:
exact (HolomorphicAt.extChartAt (s.near_subset_chart m)).comp holomorphicAt_snd
Proof state after:
case ga
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(extChartAt I a) a) p
Theorem: Super.bottcherNear_holomorphic
Proof state before:
case ga
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
h1 :
  HolomorphicAt (I.prod I) I (fun p => _root_.bottcherNear (s.fl p.1) d p.2)
    (p.1, ↑(extChartAt I a) p.2 - ↑(extChartAt I a) a)
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(extChartAt I a) a) p
Tactic:
exact holomorphicAt_const
Proof state after:
no goals
Theorem: Super.bottcherNearIter_holomorphic
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 : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
Tactic:
refine (s.bottcherNear_holomorphic _ ?_).comp₂ holomorphicAt_fst (s.holomorphic_iter _)
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 : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ ((c, z).1, (f (c, z).1)^[n] (c, z).2) ∈ s.near
Theorem: Super.bottcherNearIter_holomorphic
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 : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ ((c, z).1, (f (c, z).1)^[n] (c, z).2) ∈ s.near
Tactic:
exact r
Proof state after:
no goals
Theorem: Super.bottcherNear_eqn
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ s.bottcherNear c (f c z) = s.bottcherNear c z ^ d
Tactic:
simp only [Super.bottcherNear]
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) =
    _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) ^ d
Theorem: Super.bottcherNear_eqn
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) =
    _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) ^ d
Tactic:
have e : extChartAt I a (f c z) - extChartAt I a a =
    s.fl c (extChartAt I a z - extChartAt I a a) := by
  simp only [Function.comp, Super.fl, _root_.fl, sub_add_cancel,
    PartialEquiv.left_inv _ (s.near_subset_chart 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 : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
e : ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a = s.fl c (↑(extChartAt I a) z - ↑(extChartAt I a) a)
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) =
    _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) ^ d
Theorem: Super.bottcherNear_eqn
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
e : ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a = s.fl c (↑(extChartAt I a) z - ↑(extChartAt I a) a)
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) =
    _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) ^ d
Tactic:
rw [e, _root_.bottcherNear_eqn (s.superNearC.s (Set.mem_univ c)) (s.mem_near_to_near' m)]
Proof state after:
no goals
Theorem: Super.bottcherNear_eqn
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a = s.fl c (↑(extChartAt I a) z - ↑(extChartAt I a) a)
Tactic:
simp only [Function.comp, Super.fl, _root_.fl, sub_add_cancel,
  PartialEquiv.left_inv _ (s.near_subset_chart m)]
Proof state after:
no goals
Theorem: Super.bottcherNear_eqn_iter
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 : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
m : (c, z) ∈ s.near
n : ℕ
⊢ s.bottcherNear c ((f c)^[n] z) = s.bottcherNear c z ^ d ^ n
Tactic:
induction' n with n h
Proof state after:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ s.bottcherNear c ((f c)^[0] z) = s.bottcherNear c z ^ d ^ 0

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
m : (c, z) ∈ s.near
n : ℕ
h : s.bottcherNear c ((f c)^[n] z) = s.bottcherNear c z ^ d ^ n
⊢ s.bottcherNear c ((f c)^[n + 1] z) = s.bottcherNear c z ^ d ^ (n + 1)
Theorem: Super.bottcherNear_eqn_iter
Proof state before:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ s.bottcherNear c ((f c)^[0] z) = s.bottcherNear c z ^ d ^ 0

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
m : (c, z) ∈ s.near
n : ℕ
h : s.bottcherNear c ((f c)^[n] z) = s.bottcherNear c z ^ d ^ n
⊢ s.bottcherNear c ((f c)^[n + 1] z) = s.bottcherNear c z ^ d ^ (n + 1)
Tactic:
simp only [Function.iterate_zero_apply, pow_zero, pow_one]
Proof state after:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
m : (c, z) ∈ s.near
n : ℕ
h : s.bottcherNear c ((f c)^[n] z) = s.bottcherNear c z ^ d ^ n
⊢ s.bottcherNear c ((f c)^[n + 1] z) = s.bottcherNear c z ^ d ^ (n + 1)
Theorem: Super.bottcherNear_eqn_iter
Proof state before:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
m : (c, z) ∈ s.near
n : ℕ
h : s.bottcherNear c ((f c)^[n] z) = s.bottcherNear c z ^ d ^ n
⊢ s.bottcherNear c ((f c)^[n + 1] z) = s.bottcherNear c z ^ d ^ (n + 1)
Tactic:
simp only [Function.iterate_succ_apply', s.bottcherNear_eqn (s.iter_stays_near m n), h, ←
  pow_mul, ← pow_succ]
Proof state after:
no goals
Theorem: Super.bottcherNearp_eqn
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ℂ × S
m : p ∈ s.near
⊢ s.bottcherNearp (s.fp p) = s.bottcherNearp p ^ d
Tactic:
rcases p with ⟨c, z⟩
Proof state after:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ s.bottcherNearp (s.fp (c, z)) = s.bottcherNearp (c, z) ^ d
Theorem: Super.bottcherNearp_eqn
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ s.bottcherNearp (s.fp (c, z)) = s.bottcherNearp (c, z) ^ d
Tactic:
exact s.bottcherNear_eqn m
Proof state after:
no goals
Theorem: Super.bottcherNear_lt_one
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c z) < 1
Tactic:
simp only [Super.bottcherNear, mem_setOf]
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ Complex.abs (_root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a)) < 1
Theorem: Super.bottcherNear_lt_one
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ Complex.abs (_root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a)) < 1
Tactic:
exact _root_.bottcherNear_lt_one (s.superNearC.s (Set.mem_univ c)) (s.mem_near_to_near' m)
Proof state after:
no goals