internlm/Lean-Github huggingface dataset:
Theorem: join_r
Proof 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]
Proof 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
Theorem: join_r
Proof 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
Proof 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
Theorem: join_r
Proof 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 ⊢
Proof 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
Theorem: join_r
Proof 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
Proof state after:
no goals
Theorem: join_r
Proof 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 ?_)
Proof 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)
Theorem: join_r
Proof 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]
Proof state after:
no goals
Theorem: joined_growOpen
Proof 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⟩
Proof 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
Theorem: joined_growOpen
Proof 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
Proof 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
Theorem: joined_growOpen
Proof 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
Proof 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
Theorem: joined_growOpen
Proof 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]
Proof state after:
no goals
Theorem: joined_growOpen
Proof 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]
Proof state after:
no goals
Theorem: joined_growOpen
Proof 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⟩
Proof 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
Theorem: joined_growOpen
Proof 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
Proof 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
Theorem: joined_growOpen
Proof 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
Proof 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
Theorem: joined_growOpen
Proof 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
Proof 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
Theorem: joined_growOpen
Proof 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
Proof 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
Theorem: joined_growOpen
Proof 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 ⊢
Proof 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