Theorem: joined_growOpen (Ray/Dynamics/Grow.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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
⊢ rs c 0 = a
Tactic:
rcases tend.exists_lt pos with ⟨k, pos⟩
State after:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
⊢ rs c 0 = a

State before:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
⊢ rs c 0 = a
Tactic:
have e := (loc k 0 (by simp only [Complex.abs.map_zero, pos])).self_of_nhds
State after:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
e : uncurry rs (c, 0) = uncurry (r k) (c, 0)
⊢ rs c 0 = a

State before:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
e : uncurry rs (c, 0) = uncurry (r k) (c, 0)
⊢ rs c 0 = a
Tactic:
simp only [uncurry] at e
State after:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
e : rs c 0 = r k c 0
⊢ rs c 0 = a

State before:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
e : rs c 0 = r k c 0
⊢ rs c 0 = a
Tactic:
simp only [e, (g k).zero]
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
⊢ Complex.abs 0 < p k
Tactic:
simp only [Complex.abs.map_zero, pos]
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (rs x.1 x.2) = x.2
Tactic:
rcases tend.exists_lt pos with ⟨k, pos⟩
State after:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (rs x.1 x.2) = x.2

State before:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (rs x.1 x.2) = x.2
Tactic:
apply (g k).start.mp
State after:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r k x.1 x.2) = x.2 → s.bottcherNear x.1 (rs x.1 x.2) = x.2

State before:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r k x.1 x.2) = x.2 → s.bottcherNear x.1 (rs x.1 x.2) = x.2
Tactic:
apply (loc k 0 (by simp only [Complex.abs.map_zero, pos])).mp
State after:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0),
    uncurry rs x = uncurry (r k) x → s.bottcherNear x.1 (r k x.1 x.2) = x.2 → s.bottcherNear x.1 (rs x.1 x.2) = x.2

State before:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0),
    uncurry rs x = uncurry (r k) x → s.bottcherNear x.1 (r k x.1 x.2) = x.2 → s.bottcherNear x.1 (rs x.1 x.2) = x.2
Tactic:
apply eventually_of_forall
State after:
case intro.hp
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
⊢ ∀ (x : ℂ × ℂ),
    uncurry rs x = uncurry (r k) x → s.bottcherNear x.1 (r k x.1 x.2) = x.2 → s.bottcherNear x.1 (rs x.1 x.2) = x.2

State before:
case intro.hp
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
⊢ ∀ (x : ℂ × ℂ),
    uncurry rs x = uncurry (r k) x → s.bottcherNear x.1 (r k x.1 x.2) = x.2 → s.bottcherNear x.1 (rs x.1 x.2) = x.2
Tactic:
intro ⟨e, x⟩ loc start
State after:
case intro.hp
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc✝ : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
e x : ℂ
loc : uncurry rs (e, x) = uncurry (r k) (e, x)
start : s.bottcherNear (e, x).1 (r k (e, x).1 (e, x).2) = (e, x).2
⊢ s.bottcherNear (e, x).1 (rs (e, x).1 (e, x).2) = (e, x).2

State before:
case intro.hp
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc✝ : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
e x : ℂ
loc : uncurry rs (e, x) = uncurry (r k) (e, x)
start : s.bottcherNear (e, x).1 (r k (e, x).1 (e, x).2) = (e, x).2
⊢ s.bottcherNear (e, x).1 (rs (e, x).1 (e, x).2) = (e, x).2
Tactic:
simp only [uncurry] at loc start ⊢
State after:
case intro.hp
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc✝ : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
e x : ℂ
loc : rs e x = r k e x
start : s.bottcherNear e (r k e x) = x
⊢ s.bottcherNear e (rs e x) = x

State before:
case intro.hp
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos✝ : 0 < ps
loc✝ : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
k : ℕ
pos : 0 < p k
e x : ℂ
loc : rs e x = r k e x
start : s.bottcherNear e (r k e x) = x
⊢ s.bottcherNear e (rs e x) = x
Tactic:
simp only [start, loc]
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ ball 0 ps), Eqn s (s.np c ps) rs x
Tactic:
apply mem_nhdsSet_iff_forall.mpr
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
⊢ ∀ x ∈ {c} ×ˢ ball 0 ps, {x | (fun x => Eqn s (s.np c ps) rs x) x} ∈ 𝓝 x

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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
⊢ ∀ x ∈ {c} ×ˢ ball 0 ps, {x | (fun x => Eqn s (s.np c ps) rs x) x} ∈ 𝓝 x
Tactic:
intro ⟨c', x⟩ lt
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
c' x : ℂ
lt : (c', x) ∈ {c} ×ˢ ball 0 ps
⊢ {x | (fun x => Eqn s (s.np c ps) rs x) x} ∈ 𝓝 (c', x)

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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
c' x : ℂ
lt : (c', x) ∈ {c} ×ˢ ball 0 ps
⊢ {x | (fun x => Eqn s (s.np c ps) rs x) x} ∈ 𝓝 (c', x)
Tactic:
simp only [mem_prod_eq, mem_singleton_iff, mem_ball, Complex.dist_eq, sub_zero] at lt
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
c' x : ℂ
lt : c' = c ∧ Complex.abs x < ps
⊢ {x | (fun x => Eqn s (s.np c ps) rs x) x} ∈ 𝓝 (c', x)

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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
c' x : ℂ
lt : c' = c ∧ Complex.abs x < ps
⊢ {x | (fun x => Eqn s (s.np c ps) rs x) x} ∈ 𝓝 (c', x)
Tactic:
simp only [lt.1, eq_self_iff_true, true_and_iff, ← Filter.eventually_iff] at lt ⊢
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
c' x : ℂ
lt : Complex.abs x < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x

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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
c' x : ℂ
lt : Complex.abs x < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
Tactic:
clear c'
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x

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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
Tactic:
rcases tend.exists_lt lt with ⟨k, ltp⟩
State after:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x

State before:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
Tactic:
have m : (c, x) ∈ {c} ×ˢ closedBall (0 : ℂ) (p k) := by
  simp only [mem_prod_eq, mem_singleton_iff, Metric.mem_closedBall, eq_self_iff_true,
    true_and_iff, Complex.dist_eq, sub_zero, ltp.le]
State after:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x

State before:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
Tactic:
have lt' : ∀ᶠ y : ℂ × ℂ in 𝓝 (c, x), abs y.2 < ps :=
  (Complex.continuous_abs.continuousAt.comp continuousAt_snd).eventually_lt
    continuousAt_const lt
State after:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x

State before:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
Tactic:
apply ((g k).eqn.filter_mono (nhds_le_nhdsSet m)).mp
State after:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x

State before:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x
Tactic:
apply (loc _ _ ltp).eventually_nhds.mp
State after:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    (∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry rs x = uncurry (r k) x) → Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x

State before:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    (∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry rs x = uncurry (r k) x) → Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x
Tactic:
apply lt'.mp
State after:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    Complex.abs x.2 < ps →
      (∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry rs x = uncurry (r k) x) → Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x

State before:
case intro
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    Complex.abs x.2 < ps →
      (∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry rs x = uncurry (r k) x) → Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x
Tactic:
apply eventually_of_forall
State after:
case intro.hp
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ (x : ℂ × ℂ),
    Complex.abs x.2 < ps →
      (∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry rs x = uncurry (r k) x) → Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x

State before:
case intro.hp
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ (x : ℂ × ℂ),
    Complex.abs x.2 < ps →
      (∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry rs x = uncurry (r k) x) → Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x
Tactic:
intro ⟨e, y⟩ _ loc eq
State after:
case intro.hp
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc✝ : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
e y : ℂ
a✝ : Complex.abs (e, y).2 < ps
loc : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (e, y), uncurry rs x = uncurry (r k) x
eq : Eqn s (s.np c ps) (r k) (e, y)
⊢ Eqn s (s.np c ps) rs (e, y)

State before:
case intro.hp
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc✝ : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
e y : ℂ
a✝ : Complex.abs (e, y).2 < ps
loc : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (e, y), uncurry rs x = uncurry (r k) x
eq : Eqn s (s.np c ps) (r k) (e, y)
⊢ Eqn s (s.np c ps) rs (e, y)
Tactic:
exact eq.congr (Filter.EventuallyEq.symm loc)
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 : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
⊢ (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
Tactic:
simp only [mem_prod_eq, mem_singleton_iff, Metric.mem_closedBall, eq_self_iff_true,
  true_and_iff, Complex.dist_eq, sub_zero, ltp.le]
State after:
no goals