Theorem: Super.bottcherNear_holomorphic (Ray/Dynamics/BottcherNearM.lean)

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
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

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
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

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]
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

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
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

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
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

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
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

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 ?_
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)

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]
State after:
no goals

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
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

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
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

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
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

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
State after:
no goals