Theorem: Super.iter_holomorphic' (Ray/Dynamics/Potential.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
n : ℕ
⊢ Holomorphic (I.prod I) I fun p => (f p.1)^[n] p.2
Tactic:
intro p
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 : ℕ
p : ℂ × S
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) 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
n : ℕ
p : ℂ × S
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) 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
p : ℂ × S
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[0] p.2) 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
p : ℂ × S
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n + 1] p.2) 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
p : ℂ × S
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[0] p.2) 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
p : ℂ × S
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n + 1] p.2) p
Tactic:
simp [Function.iterate_zero, holomorphicAt_snd]
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 : HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n + 1] p.2) 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
p : ℂ × S
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n + 1] p.2) p
Tactic:
simp only [Function.iterate_succ', Function.comp]
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 : HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) p
⊢ HolomorphicAt (I.prod I) I (fun p => f p.1 ((f p.1)^[n] p.2)) 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
p : ℂ × S
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) p
⊢ HolomorphicAt (I.prod I) I (fun p => f p.1 ((f p.1)^[n] p.2)) p
Tactic:
exact (s.fa _).comp₂ holomorphicAt_fst h
State after:
no goals