Theorem: Super.attracts (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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ Attracts (f c) z a
Tactic:
have m := s.mem_near_to_near' r
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
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
⊢ Attracts (f c) z 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
⊢ Attracts (f c) z a
Tactic:
have t := iterates_tendsto (s.superNearC.s (Set.mem_univ c)) 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
⊢ Attracts (f c) z 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
⊢ Attracts (f c) z a
Tactic:
generalize hg : (fun x : ℂ ↦ (extChartAt I a).symm (x + extChartAt I a a)) = g
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
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ Attracts (f c) z 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ Attracts (f c) z a
Tactic:
have gc : ContinuousAt g 0 := by
  rw [← hg]
  refine (continuousAt_extChartAt_symm'' I ?_).comp
    (continuous_id.add continuous_const).continuousAt
  simp only [zero_add]; exact mem_extChartAt_target I a
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
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
⊢ Attracts (f c) z 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
⊢ Attracts (f c) z a
Tactic:
have g0 : g 0 = a := by
  simp only [← hg]; simp only [zero_add]; exact PartialEquiv.left_inv _ (mem_extChartAt_source _ _)
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
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
g0 : g 0 = a
⊢ Attracts (f c) z 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
g0 : g 0 = a
⊢ Attracts (f c) z a
Tactic:
have h := gc.tendsto.comp t
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
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
g0 : g 0 = a
h : Tendsto (g ∘ fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 (g 0))
⊢ Attracts (f c) z 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
g0 : g 0 = a
h : Tendsto (g ∘ fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 (g 0))
⊢ Attracts (f c) z a
Tactic:
clear t gc 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
h : Tendsto (g ∘ fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 (g 0))
⊢ Attracts (f c) z 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
h : Tendsto (g ∘ fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 (g 0))
⊢ Attracts (f c) z a
Tactic:
simp only [Function.comp, g0] at h
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
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
h : Tendsto (fun x => g ((s.fl c)^[x] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a))) atTop (𝓝 a)
⊢ Attracts (f c) z 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
h : Tendsto (fun x => g ((s.fl c)^[x] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a))) atTop (𝓝 a)
⊢ Attracts (f c) z a
Tactic:
rw [← attracts_shift n]
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
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
h : Tendsto (fun x => g ((s.fl c)^[x] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a))) atTop (𝓝 a)
⊢ Attracts (f c) ((f c)^[n] z) 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
h : Tendsto (fun x => g ((s.fl c)^[x] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a))) atTop (𝓝 a)
⊢ Attracts (f c) ((f c)^[n] z) a
Tactic:
refine Filter.Tendsto.congr ?_ h
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
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
h : Tendsto (fun x => g ((s.fl c)^[x] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a))) atTop (𝓝 a)
⊢ ∀ (x : ℕ), g ((s.fl c)^[x] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a)) = (f c)^[x] ((f c)^[n] z)

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
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
h : Tendsto (fun x => g ((s.fl c)^[x] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a))) atTop (𝓝 a)
⊢ ∀ (x : ℕ), g ((s.fl c)^[x] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a)) = (f c)^[x] ((f c)^[n] z)
Tactic:
clear h
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
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
⊢ ∀ (x : ℕ), g ((s.fl c)^[x] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a)) = (f c)^[x] ((f c)^[n] z)

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
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
⊢ ∀ (x : ℕ), g ((s.fl c)^[x] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a)) = (f c)^[x] ((f c)^[n] z)
Tactic:
intro k
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
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
⊢ g ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a)) = (f c)^[k] ((f c)^[n] z)

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
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
⊢ g ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a)) = (f c)^[k] ((f c)^[n] z)
Tactic:
simp only [← hg]
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
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
⊢ ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)

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
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
⊢ ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
Tactic:
induction' k with k 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
⊢ ↑(extChartAt I a).symm ((s.fl c)^[0] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[0] ((f c)^[n] z)

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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
⊢ ↑(extChartAt I a).symm
      ((s.fl c)^[k + 1] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k + 1] ((f c)^[n] z)

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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
⊢ ↑(extChartAt I a).symm ((s.fl c)^[0] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[0] ((f c)^[n] z)

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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
⊢ ↑(extChartAt I a).symm
      ((s.fl c)^[k + 1] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k + 1] ((f c)^[n] z)
Tactic:
simp only [Function.iterate_zero_apply]
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
⊢ ↑(extChartAt I a).symm (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a + ↑(extChartAt I a) a) = (f c)^[n] z

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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
⊢ ↑(extChartAt I a).symm
      ((s.fl c)^[k + 1] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k + 1] ((f c)^[n] z)

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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
⊢ ↑(extChartAt I a).symm (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a + ↑(extChartAt I a) a) = (f c)^[n] z

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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
⊢ ↑(extChartAt I a).symm
      ((s.fl c)^[k + 1] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k + 1] ((f c)^[n] z)
Tactic:
rw [sub_add_cancel]
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
⊢ ↑(extChartAt I a).symm (↑(extChartAt I a) ((f c)^[n] z)) = (f c)^[n] z

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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
⊢ ↑(extChartAt I a).symm
      ((s.fl c)^[k + 1] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k + 1] ((f c)^[n] z)

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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
⊢ ↑(extChartAt I a).symm (↑(extChartAt I a) ((f c)^[n] z)) = (f c)^[n] z

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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
⊢ ↑(extChartAt I a).symm
      ((s.fl c)^[k + 1] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k + 1] ((f c)^[n] z)
Tactic:
exact PartialEquiv.left_inv _ (s.near_subset_chart r)
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
⊢ ↑(extChartAt I a).symm
      ((s.fl c)^[k + 1] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k + 1] ((f c)^[n] z)

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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
⊢ ↑(extChartAt I a).symm
      ((s.fl c)^[k + 1] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k + 1] ((f c)^[n] z)
Tactic:
simp only [Function.iterate_succ_apply']
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
⊢ ↑(extChartAt I a).symm
      (s.fl c ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a)) + ↑(extChartAt I a) a) =
    f c ((f c)^[k] ((f c)^[n] z))

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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
⊢ ↑(extChartAt I a).symm
      (s.fl c ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a)) + ↑(extChartAt I a) a) =
    f c ((f c)^[k] ((f c)^[n] z))
Tactic:
generalize hx : (s.fl c)^[k] (extChartAt I a ((f c)^[n] z) - extChartAt I a a) = x
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
x : ℂ
hx : (s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) = x
⊢ ↑(extChartAt I a).symm (s.fl c x + ↑(extChartAt I a) a) = f c ((f c)^[k] ((f c)^[n] z))

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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
h :
  ↑(extChartAt I a).symm ((s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) + ↑(extChartAt I a) a) =
    (f c)^[k] ((f c)^[n] z)
x : ℂ
hx : (s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) = x
⊢ ↑(extChartAt I a).symm (s.fl c x + ↑(extChartAt I a) a) = f c ((f c)^[k] ((f c)^[n] z))
Tactic:
rw [hx] at h
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
x : ℂ
h : ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a) = (f c)^[k] ((f c)^[n] z)
hx : (s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) = x
⊢ ↑(extChartAt I a).symm (s.fl c x + ↑(extChartAt I a) a) = f c ((f c)^[k] ((f c)^[n] z))

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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
x : ℂ
h : ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a) = (f c)^[k] ((f c)^[n] z)
hx : (s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) = x
⊢ ↑(extChartAt I a).symm (s.fl c x + ↑(extChartAt I a) a) = f c ((f c)^[k] ((f c)^[n] z))
Tactic:
simp only [Super.fl, _root_.fl, Function.comp, sub_add_cancel, h,
  ←Function.iterate_succ_apply' (f c)]
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
x : ℂ
h : ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a) = (f c)^[k] ((f c)^[n] z)
hx : (s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) = x
⊢ ↑(extChartAt I a).symm (↑(extChartAt I a) ((f c)^[k.succ] ((f c)^[n] z))) = (f c)^[k.succ] ((f c)^[n] z)

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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
g0 : g 0 = a
k : ℕ
x : ℂ
h : ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a) = (f c)^[k] ((f c)^[n] z)
hx : (s.fl c)^[k] (↑(extChartAt I a) ((f c)^[n] z) - ↑(extChartAt I a) a) = x
⊢ ↑(extChartAt I a).symm (↑(extChartAt I a) ((f c)^[k.succ] ((f c)^[n] z))) = (f c)^[k.succ] ((f c)^[n] z)
Tactic:
apply PartialEquiv.left_inv _ (s.near_subset_chart (s.iter_stays_near r _))
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ ContinuousAt g 0
Tactic:
rw [← hg]
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
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ ContinuousAt (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) 0

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
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ ContinuousAt (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) 0
Tactic:
refine (continuousAt_extChartAt_symm'' I ?_).comp
  (continuous_id.add continuous_const).continuousAt
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
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ 0 + ↑(extChartAt I a) a ∈ (extChartAt I a).target

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
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ 0 + ↑(extChartAt I a) a ∈ (extChartAt I a).target
Tactic:
simp only [zero_add]
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
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ ↑(extChartAt I a) a ∈ (extChartAt I a).target

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
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
⊢ ↑(extChartAt I a) a ∈ (extChartAt I a).target
Tactic:
exact mem_extChartAt_target I a
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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
⊢ g 0 = a
Tactic:
simp only [← hg]
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
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
⊢ ↑(extChartAt I a).symm (0 + ↑(extChartAt I a) 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
⊢ ↑(extChartAt I a).symm (0 + ↑(extChartAt I a) a) = a
Tactic:
simp only [zero_add]
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
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
⊢ ↑(extChartAt I a).symm (↑(extChartAt I a) 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
m : ((c, (f c)^[n] z).1, ↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a) ∈ s.near'
t : Tendsto (fun n_1 => (s.fl c)^[n_1] (↑(extChartAt I a) (c, (f c)^[n] z).2 - ↑(extChartAt I a) a)) atTop (𝓝 0)
g : ℂ → S
hg : (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = g
gc : ContinuousAt g 0
⊢ ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
Tactic:
exact PartialEquiv.left_inv _ (mem_extChartAt_source _ _)
State after:
no goals