internlm/Lean-Github huggingface dataset:
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 : rs e x = r k e x
start : s.bottcherNear e (r k e x) = x
⊢ s.bottcherNear e (rs e x) = x
Tactic:
simp only [start, loc]
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} ×ˢ ball 0 ps), Eqn s (s.np c ps) rs x
Tactic:
apply mem_nhdsSet_iff_forall.mpr
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 : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
⊢ ∀ x ∈ {c} ×ˢ ball 0 ps, {x | (fun x => Eqn s (s.np c ps) rs x) x} ∈ 𝓝 x
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 ∈ {c} ×ˢ ball 0 ps, {x | (fun x => Eqn s (s.np c ps) rs x) x} ∈ 𝓝 x
Tactic:
intro ⟨c', x⟩ lt
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 : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
c' x : ℂ
lt : (c', x) ∈ {c} ×ˢ ball 0 ps
⊢ {x | (fun x => Eqn s (s.np c ps) rs x) x} ∈ 𝓝 (c', x)
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))
c' x : ℂ
lt : (c', x) ∈ {c} ×ˢ ball 0 ps
⊢ {x | (fun x => Eqn s (s.np c ps) rs x) x} ∈ 𝓝 (c', x)
Tactic:
simp only [mem_prod_eq, mem_singleton_iff, mem_ball, Complex.dist_eq, sub_zero] at lt
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 : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
c' x : ℂ
lt : c' = c ∧ Complex.abs x < ps
⊢ {x | (fun x => Eqn s (s.np c ps) rs x) x} ∈ 𝓝 (c', x)
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))
c' x : ℂ
lt : c' = c ∧ Complex.abs x < ps
⊢ {x | (fun x => Eqn s (s.np c ps) rs x) x} ∈ 𝓝 (c', x)
Tactic:
simp only [lt.1, eq_self_iff_true, true_and_iff, ← Filter.eventually_iff] at lt ⊢
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 : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
c' x : ℂ
lt : Complex.abs x < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
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))
c' x : ℂ
lt : Complex.abs x < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
Tactic:
clear c'
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 : ℕ → ℝ
ps : ℝ
r : ℕ → ℂ → ℂ → S
rs : ℂ → ℂ → S
g : ∀ (k : ℕ), Grow s c (p k) (s.np c ps) (r k)
tend : Tendsto p atTop (𝓝 ps)
post : ps < s.p c
pos : 0 < ps
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry rs) (uncurry (r k))
x : ℂ
lt : Complex.abs x < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
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 : ℂ
lt : Complex.abs x < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
Tactic:
rcases tend.exists_lt lt with ⟨k, ltp⟩
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
Tactic:
have m : (c, x) ∈ {c} ×ˢ closedBall (0 : ℂ) (p k) := by
  simp only [mem_prod_eq, mem_singleton_iff, Metric.mem_closedBall, eq_self_iff_true,
    true_and_iff, Complex.dist_eq, sub_zero, ltp.le]
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
Tactic:
have lt' : ∀ᶠ y : ℂ × ℂ in 𝓝 (c, x), abs y.2 < ps :=
  (Complex.continuous_abs.continuousAt.comp continuousAt_snd).eventually_lt
    continuousAt_const lt
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) rs x
Tactic:
apply ((g k).eqn.filter_mono (nhds_le_nhdsSet m)).mp
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x
Tactic:
apply (loc _ _ ltp).eventually_nhds.mp
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    (∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry rs x = uncurry (r k) x) → Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    (∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry rs x = uncurry (r k) x) → Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x
Tactic:
apply lt'.mp
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    Complex.abs x.2 < ps →
      (∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry rs x = uncurry (r k) x) → Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    Complex.abs x.2 < ps →
      (∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry rs x = uncurry (r k) x) → Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x
Tactic:
apply eventually_of_forall
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ (x : ℂ × ℂ),
    Complex.abs x.2 < ps →
      (∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry rs x = uncurry (r k) x) → Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
⊢ ∀ (x : ℂ × ℂ),
    Complex.abs x.2 < ps →
      (∀ᶠ (x : ℂ × ℂ) in 𝓝 x, uncurry rs x = uncurry (r k) x) → Eqn s (s.np c ps) (r k) x → Eqn s (s.np c ps) rs x
Tactic:
intro ⟨e, y⟩ _ loc eq
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
e y : ℂ
a✝ : Complex.abs (e, y).2 < ps
loc : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (e, y), uncurry rs x = uncurry (r k) x
eq : Eqn s (s.np c ps) (r k) (e, y)
⊢ Eqn s (s.np c ps) rs (e, y)
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))
x : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
m : (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
lt' : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Complex.abs y.2 < ps
e y : ℂ
a✝ : Complex.abs (e, y).2 < ps
loc : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (e, y), uncurry rs x = uncurry (r k) x
eq : Eqn s (s.np c ps) (r k) (e, y)
⊢ Eqn s (s.np c ps) rs (e, y)
Tactic:
exact eq.congr (Filter.EventuallyEq.symm loc)
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 : ℂ
lt : Complex.abs x < ps
k : ℕ
ltp : Complex.abs x < p k
⊢ (c, x) ∈ {c} ×ˢ closedBall 0 (p k)
Tactic:
simp only [mem_prod_eq, mem_singleton_iff, Metric.mem_closedBall, eq_self_iff_true,
  true_and_iff, Complex.dist_eq, sub_zero, ltp.le]
Proof state after:
no goals
Theorem: Super.grow
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
inst✝ : OnePreimage s
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
set t : Set ℝ := {p | 0 ≤ p ∧ ∀ q, 0 ≤ q → q ≤ p → ∃ r, Grow s c q (s.np c q) r}
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
inst✝ : OnePreimage s
t : Set ℝ := {p | 0 ≤ p ∧ ∀ (q : ℝ), 0 ≤ q → q ≤ p → ∃ r, Grow s c q (s.np c q) r}
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Theorem: Super.grow
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
inst✝ : OnePreimage s
t : Set ℝ := {p | 0 ≤ p ∧ ∀ (q : ℝ), 0 ≤ q → q ≤ p → ∃ r, Grow s c q (s.np c q) r}
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
have self : ∀ {p}, p ∈ t → ∃ r, Grow s c p (s.np c p) r := fun {p} m ↦ m.2 _ m.1 (le_refl _)
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
inst✝ : OnePreimage s
t : Set ℝ := {p | 0 ≤ p ∧ ∀ (q : ℝ), 0 ≤ q → q ≤ p → ∃ r, Grow s c q (s.np c q) r}
self : ∀ {p : ℝ}, p ∈ t → ∃ r, Grow s c p (s.np c p) r
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Theorem: Super.grow
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
inst✝ : OnePreimage s
t : Set ℝ := {p | 0 ≤ p ∧ ∀ (q : ℝ), 0 ≤ q → q ≤ p → ∃ r, Grow s c q (s.np c q) r}
self : ∀ {p : ℝ}, p ∈ t → ∃ r, Grow s c p (s.np c p) r
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
have t1 : ∀ p : ℝ, p ∈ t → p < 1 := by intro p m; rcases self m with ⟨r, g⟩; exact g.p1
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
inst✝ : OnePreimage s
t : Set ℝ := {p | 0 ≤ p ∧ ∀ (q : ℝ), 0 ≤ q → q ≤ p → ∃ r, Grow s c q (s.np c q) r}
self : ∀ {p : ℝ}, p ∈ t → ∃ r, Grow s c p (s.np c p) r
t1 : ∀ p ∈ t, p < 1
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r