Theorem: join_r (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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
⊢ ∃ rs, ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
Tactic:
have above : ∀ k, p k ≤ ps := fun k ↦ mono.ge_of_tendsto tend 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✝ : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
⊢ ∃ rs, ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))

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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
⊢ ∃ rs, ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
Tactic:
generalize hrs : (fun e x : ℂ ↦
  if h : abs x < ps then r (Nat.find (tend.exists_lt h)) e x else a) = rs
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
⊢ ∃ rs, ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))

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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
⊢ ∃ rs, ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
Tactic:
use rs
State after:
case h
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
⊢ ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))

State before:
case h
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
⊢ ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
Tactic:
intro k x xk
State after:
case h
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
⊢ (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))

State before:
case h
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
⊢ (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
Tactic:
rcases eventually_nhds_iff.mp (loc k) with ⟨u, eq, uo, uc⟩
State after:
case h.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
u : Set ℂ
eq : ∀ x ∈ u, ∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1
uo : IsOpen u
uc : c ∈ u
⊢ (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))

State before:
case h.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
u : Set ℂ
eq : ∀ x ∈ u, ∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1
uo : IsOpen u
uc : c ∈ u
⊢ (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
Tactic:
have m : u ×ˢ ball (0 : ℂ) (p k) ∈ 𝓝 (c, x) := by
  refine prod_mem_nhds (uo.mem_nhds uc) (isOpen_ball.mem_nhds ?_)
  simp only [mem_ball, Complex.dist_eq, sub_zero, xk]
State after:
case h.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
u : Set ℂ
eq : ∀ x ∈ u, ∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1
uo : IsOpen u
uc : c ∈ u
m : u ×ˢ ball 0 (p k) ∈ 𝓝 (c, x)
⊢ (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))

State before:
case h.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
u : Set ℂ
eq : ∀ x ∈ u, ∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1
uo : IsOpen u
uc : c ∈ u
m : u ×ˢ ball 0 (p k) ∈ 𝓝 (c, x)
⊢ (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
Tactic:
apply Filter.eventually_of_mem m
State after:
case h.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
u : Set ℂ
eq : ∀ x ∈ u, ∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1
uo : IsOpen u
uc : c ∈ u
m : u ×ˢ ball 0 (p k) ∈ 𝓝 (c, x)
⊢ ∀ x ∈ u ×ˢ ball 0 (p k), uncurry rs x = uncurry (r k) x

State before:
case h.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
u : Set ℂ
eq : ∀ x ∈ u, ∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1
uo : IsOpen u
uc : c ∈ u
m : u ×ˢ ball 0 (p k) ∈ 𝓝 (c, x)
⊢ ∀ x ∈ u ×ˢ ball 0 (p k), uncurry rs x = uncurry (r k) x
Tactic:
intro ⟨e, y⟩ ⟨m0, m1⟩
State after:
case h.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
u : Set ℂ
eq : ∀ x ∈ u, ∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1
uo : IsOpen u
uc : c ∈ u
m : u ×ˢ ball 0 (p k) ∈ 𝓝 (c, x)
e y : ℂ
m0 : (e, y).1 ∈ u
m1 : (e, y).2 ∈ ball 0 (p k)
⊢ uncurry rs (e, y) = uncurry (r k) (e, y)

State before:
case h.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
u : Set ℂ
eq : ∀ x ∈ u, ∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1
uo : IsOpen u
uc : c ∈ u
m : u ×ˢ ball 0 (p k) ∈ 𝓝 (c, x)
e y : ℂ
m0 : (e, y).1 ∈ u
m1 : (e, y).2 ∈ ball 0 (p k)
⊢ uncurry rs (e, y) = uncurry (r k) (e, y)
Tactic:
simp only [mem_ball, Complex.dist_eq, sub_zero] at m1
State after:
case h.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
u : Set ℂ
eq : ∀ x ∈ u, ∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1
uo : IsOpen u
uc : c ∈ u
m : u ×ˢ ball 0 (p k) ∈ 𝓝 (c, x)
e y : ℂ
m0 : (e, y).1 ∈ u
m1 : Complex.abs y < p k
⊢ uncurry rs (e, y) = uncurry (r k) (e, y)

State before:
case h.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
u : Set ℂ
eq : ∀ x ∈ u, ∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1
uo : IsOpen u
uc : c ∈ u
m : u ×ˢ ball 0 (p k) ∈ 𝓝 (c, x)
e y : ℂ
m0 : (e, y).1 ∈ u
m1 : Complex.abs y < p k
⊢ uncurry rs (e, y) = uncurry (r k) (e, y)
Tactic:
exact eq _ m0 _ m1
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
⊢ ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
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✝ : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
⊢ ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e 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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
⊢ ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
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✝ : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
⊢ ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p 0 → rs e x = r 0 e x

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✝ : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
⊢ ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p (k + 1) → rs e x = r (k + 1) e x

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✝ : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
⊢ ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p 0 → rs e x = r 0 e x
Tactic:
apply eventually_of_forall
State after:
case zero.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
⊢ ∀ (x x_1 : ℂ), Complex.abs x_1 < p 0 → rs x x_1 = r 0 x x_1

State before:
case zero.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
⊢ ∀ (x x_1 : ℂ), Complex.abs x_1 < p 0 → rs x x_1 = r 0 x x_1
Tactic:
intro e x x0
State after:
case zero.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
e x : ℂ
x0 : Complex.abs x < p 0
⊢ rs e x = r 0 e x

State before:
case zero.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
e x : ℂ
x0 : Complex.abs x < p 0
⊢ rs e x = r 0 e x
Tactic:
have xe : ∃ k, abs x < p k := ⟨0, x0⟩
State after:
case zero.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
e x : ℂ
x0 : Complex.abs x < p 0
xe : ∃ k, Complex.abs x < p k
⊢ rs e x = r 0 e x

State before:
case zero.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
e x : ℂ
x0 : Complex.abs x < p 0
xe : ∃ k, Complex.abs x < p k
⊢ rs e x = r 0 e x
Tactic:
simp only [← hrs, lt_of_lt_of_le x0 (above _), dif_pos, (Nat.find_eq_zero xe).mpr x0]
State after:
no goals

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✝ : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
⊢ ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p (k + 1) → rs e x = r (k + 1) e x
Tactic:
have eq := (g k).unique (g (k + 1)) (mono (Nat.lt_succ_self _).le)
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✝ : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq : (𝓝ˢ ({c} ×ˢ closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
⊢ ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p (k + 1) → rs e x = r (k + 1) e x

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✝ : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq : (𝓝ˢ ({c} ×ˢ closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
⊢ ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p (k + 1) → rs e x = r (k + 1) e x
Tactic:
simp only [isCompact_singleton.nhdsSet_prod_eq (isCompact_closedBall _ _)] at eq
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✝ : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
⊢ ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p (k + 1) → rs e x = r (k + 1) e x

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✝ : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
⊢ ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p (k + 1) → rs e x = r (k + 1) e x
Tactic:
apply h.mp
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✝ : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
⊢ ∀ᶠ (x : ℂ) in 𝓝 c,
    (∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1) →
      ∀ (x_1 : ℂ), Complex.abs x_1 < p (k + 1) → rs x x_1 = r (k + 1) x x_1

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✝ : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
p : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
⊢ ∀ᶠ (x : ℂ) in 𝓝 c,
    (∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1) →
      ∀ (x_1 : ℂ), Complex.abs x_1 < p (k + 1) → rs x x_1 = r (k + 1) x x_1
Tactic:
rcases Filter.mem_prod_iff.mp eq with ⟨u0, n0, u1, n1, eq⟩
State after:
case succ.intro.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 : Set ℂ
n0 : u0 ∈ 𝓝ˢ {c}
u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
⊢ ∀ᶠ (x : ℂ) in 𝓝 c,
    (∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1) →
      ∀ (x_1 : ℂ), Complex.abs x_1 < p (k + 1) → rs x x_1 = r (k + 1) x x_1

State before:
case succ.intro.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 : Set ℂ
n0 : u0 ∈ 𝓝ˢ {c}
u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
⊢ ∀ᶠ (x : ℂ) in 𝓝 c,
    (∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1) →
      ∀ (x_1 : ℂ), Complex.abs x_1 < p (k + 1) → rs x x_1 = r (k + 1) x x_1
Tactic:
simp only [nhdsSet_singleton] at n0
State after:
case succ.intro.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
⊢ ∀ᶠ (x : ℂ) in 𝓝 c,
    (∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1) →
      ∀ (x_1 : ℂ), Complex.abs x_1 < p (k + 1) → rs x x_1 = r (k + 1) x x_1

State before:
case succ.intro.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
⊢ ∀ᶠ (x : ℂ) in 𝓝 c,
    (∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1) →
      ∀ (x_1 : ℂ), Complex.abs x_1 < p (k + 1) → rs x x_1 = r (k + 1) x x_1
Tactic:
refine Filter.eventually_of_mem n0 fun e eu h x xk1 ↦ ?_
State after:
case succ.intro.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
⊢ rs e x = r (k + 1) e x

State before:
case succ.intro.intro.intro.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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
⊢ rs e x = r (k + 1) e x
Tactic:
by_cases xk0 : abs x < p k
State after:
case pos
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : Complex.abs x < p k
⊢ rs e x = r (k + 1) e x

case neg
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : ¬Complex.abs x < p k
⊢ rs e x = r (k + 1) e x

State before:
case pos
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : Complex.abs x < p k
⊢ rs e x = r (k + 1) e x
Tactic:
have m : (e, x) ∈ u0 ×ˢ u1 := by
  refine mk_mem_prod eu (subset_of_mem_nhdsSet n1 ?_)
  simp only [mem_closedBall, Complex.dist_eq, sub_zero, xk0.le]
State after:
case pos
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : Complex.abs x < p k
m : (e, x) ∈ u0 ×ˢ u1
⊢ rs e x = r (k + 1) e x

State before:
case pos
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : Complex.abs x < p k
m : (e, x) ∈ u0 ×ˢ u1
⊢ rs e x = r (k + 1) e x
Tactic:
specialize eq m
State after:
case pos
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : Complex.abs x < p k
m : (e, x) ∈ u0 ×ˢ u1
eq : (e, x) ∈ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
⊢ rs e x = r (k + 1) e x

State before:
case pos
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : Complex.abs x < p k
m : (e, x) ∈ u0 ×ˢ u1
eq : (e, x) ∈ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
⊢ rs e x = r (k + 1) e x
Tactic:
simp only [mem_setOf, uncurry] at eq
State after:
case pos
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : Complex.abs x < p k
m : (e, x) ∈ u0 ×ˢ u1
eq : r k e x = r (k + 1) e x
⊢ rs e x = r (k + 1) e x

State before:
case pos
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : Complex.abs x < p k
m : (e, x) ∈ u0 ×ˢ u1
eq : r k e x = r (k + 1) e x
⊢ rs e x = r (k + 1) e x
Tactic:
rw [h _ xk0, eq]
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : Complex.abs x < p k
⊢ (e, x) ∈ u0 ×ˢ u1
Tactic:
refine mk_mem_prod eu (subset_of_mem_nhdsSet n1 ?_)
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : Complex.abs x < p k
⊢ x ∈ closedBall 0 (p k)

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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : Complex.abs x < p k
⊢ x ∈ closedBall 0 (p k)
Tactic:
simp only [mem_closedBall, Complex.dist_eq, sub_zero, xk0.le]
State after:
no goals

State before:
case neg
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : ¬Complex.abs x < p k
⊢ rs e x = r (k + 1) e x
Tactic:
have xe : ∃ k, abs x < p k := ⟨k + 1, xk1⟩
State after:
case neg
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : ¬Complex.abs x < p k
xe : ∃ k, Complex.abs x < p k
⊢ rs e x = r (k + 1) e x

State before:
case neg
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : ¬Complex.abs x < p k
xe : ∃ k, Complex.abs x < p k
⊢ rs e x = r (k + 1) e x
Tactic:
have n := (Nat.find_eq_iff xe).mpr ⟨xk1, ?_⟩
State after:
case neg.refine_2
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 : ℕ → ℝ
n✝ : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n✝ k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : ¬Complex.abs x < p k
xe : ∃ k, Complex.abs x < p k
n : Nat.find xe = k + 1
⊢ rs e x = r (k + 1) e x

case neg.refine_1
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : ¬Complex.abs x < p k
xe : ∃ k, Complex.abs x < p k
⊢ ∀ n < k + 1, ¬Complex.abs x < p n

State before:
case neg.refine_2
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 : ℕ → ℝ
n✝ : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n✝ k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : ¬Complex.abs x < p k
xe : ∃ k, Complex.abs x < p k
n : Nat.find xe = k + 1
⊢ rs e x = r (k + 1) e x

case neg.refine_1
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : ¬Complex.abs x < p k
xe : ∃ k, Complex.abs x < p k
⊢ ∀ n < k + 1, ¬Complex.abs x < p n
Tactic:
simp only [← hrs, lt_of_lt_of_le xk1 (above _), dif_pos, n]
State after:
case neg.refine_1
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : ¬Complex.abs x < p k
xe : ∃ k, Complex.abs x < p k
⊢ ∀ n < k + 1, ¬Complex.abs x < p n

State before:
case neg.refine_1
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : ¬Complex.abs x < p k
xe : ∃ k, Complex.abs x < p k
⊢ ∀ n < k + 1, ¬Complex.abs x < p n
Tactic:
intro j jk
State after:
case neg.refine_1
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : ¬Complex.abs x < p k
xe : ∃ k, Complex.abs x < p k
j : ℕ
jk : j < k + 1
⊢ ¬Complex.abs x < p j

State before:
case neg.refine_1
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xk0 : ¬Complex.abs x < p k
xe : ∃ k, Complex.abs x < p k
j : ℕ
jk : j < k + 1
⊢ ¬Complex.abs x < p j
Tactic:
simp only [not_lt, Nat.lt_succ_iff] at jk xk0 ⊢
State after:
case neg.refine_1
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xe : ∃ k, Complex.abs x < p k
j : ℕ
jk : j ≤ k
xk0 : p k ≤ Complex.abs x
⊢ p j ≤ Complex.abs x

State before:
case neg.refine_1
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
k : ℕ
h✝ : ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
eq✝ : (𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 (p k))).EventuallyEq (uncurry (r k)) (uncurry (r (k + 1)))
u0 u1 : Set ℂ
n1 : u1 ∈ 𝓝ˢ (closedBall 0 (p k))
eq : u0 ×ˢ u1 ⊆ {x | (fun x => uncurry (r k) x = uncurry (r (k + 1)) x) x}
n0 : u0 ∈ 𝓝 c
e : ℂ
eu : e ∈ u0
h : ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
x : ℂ
xk1 : Complex.abs x < p (k + 1)
xe : ∃ k, Complex.abs x < p k
j : ℕ
jk : j ≤ k
xk0 : p k ≤ Complex.abs x
⊢ p j ≤ Complex.abs x
Tactic:
exact _root_.trans (mono jk) xk0
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
u : Set ℂ
eq : ∀ x ∈ u, ∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1
uo : IsOpen u
uc : c ∈ u
⊢ u ×ˢ ball 0 (p k) ∈ 𝓝 (c, x)
Tactic:
refine prod_mem_nhds (uo.mem_nhds uc) (isOpen_ball.mem_nhds ?_)
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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
u : Set ℂ
eq : ∀ x ∈ u, ∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1
uo : IsOpen u
uc : c ∈ u
⊢ x ∈ ball 0 (p k)

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 : ℕ → ℝ
n : ℕ → ℕ
ps : ℝ
r : ℕ → ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (n k) (r k)
mono : Monotone p
tend : Tendsto p atTop (𝓝 ps)
above : ∀ (k : ℕ), p k ≤ ps
rs : ℂ → ℂ → S
hrs : (fun e x => if h : Complex.abs x < ps then r (Nat.find ⋯) e x else a) = rs
loc : ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
k : ℕ
x : ℂ
xk : Complex.abs x < p k
u : Set ℂ
eq : ∀ x ∈ u, ∀ (x_1 : ℂ), Complex.abs x_1 < p k → rs x x_1 = r k x x_1
uo : IsOpen u
uc : c ∈ u
⊢ x ∈ ball 0 (p k)
Tactic:
simp only [mem_ball, Complex.dist_eq, sub_zero, xk]
State after:
no goals