Theorem: Super.holomorphicAt_iter (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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h : ℂ × T → S
p : ℂ × T
n : ℕ
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h p)) p
Tactic:
induction' n with n h
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[0] (h p)) p

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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n + 1] (h✝ p)) p

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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[0] (h p)) p

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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n + 1] (h✝ p)) p
Tactic:
simp only [Function.iterate_zero, id]
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h p
⊢ HolomorphicAt (I.prod I) I (fun p => h p) p

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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n + 1] (h✝ p)) p

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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h p
⊢ HolomorphicAt (I.prod I) I (fun p => h p) p

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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n + 1] (h✝ p)) p
Tactic:
exact ha
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n + 1] (h✝ p)) p

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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n + 1] (h✝ p)) p
Tactic:
simp_rw [Function.iterate_succ']
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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p) ∘ (f (g p))^[n]) (h✝ p)) p

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
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
g : ℂ × T → ℂ
h✝ : ℂ × T → S
p : ℂ × T
ga : HolomorphicAt (I.prod I) I g p
ha : HolomorphicAt (I.prod I) I h✝ p
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f (g p))^[n] (h✝ p)) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f (g p) ∘ (f (g p))^[n]) (h✝ p)) p
Tactic:
exact (s.fa _).comp₂ ga h
State after:
no goals