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