internlm/Lean-Github huggingface dataset:
Theorem: join_r
Proof 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⟩
Proof 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))
Theorem: join_r
Proof 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]
Proof 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))
Theorem: join_r
Proof 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
Proof 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
Theorem: join_r
Proof 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⟩
Proof 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)
Theorem: join_r
Proof 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
Proof 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)
Theorem: join_r
Proof 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
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
⊢ ∀ (k : ℕ), ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
Tactic:
intro k
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
k : ℕ
⊢ ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
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
k : ℕ
⊢ ∀ᶠ (e : ℂ) in 𝓝 c, ∀ (x : ℂ), Complex.abs x < p k → rs e x = r k e x
Tactic:
induction' k with k h
Proof 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
Theorem: join_r
Proof 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
Proof 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
Theorem: join_r
Proof 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
Proof 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
Theorem: join_r
Proof 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⟩
Proof 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
Theorem: join_r
Proof 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]
Proof state after:
no goals
Theorem: join_r
Proof 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)
Proof 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
Theorem: join_r
Proof 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
Proof 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
Theorem: join_r
Proof 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
Proof 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
Theorem: join_r
Proof 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⟩
Proof 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