internlm/Lean-Github huggingface dataset:
Theorem: Super.grow
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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
q : ℝ
q0 : 0 ≤ q
le : q ≤ sSup t
lt : ¬q < sSup t
⊢ ∃ r, Grow s c q (s.np c q) r
Tactic:
have eq := le_antisymm le (not_lt.mp lt)
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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
q : ℝ
q0 : 0 ≤ q
le : q ≤ sSup t
lt : ¬q < sSup t
eq : q = sSup t
⊢ ∃ r, Grow s c q (s.np c q) r
Theorem: Super.grow
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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
q : ℝ
q0 : 0 ≤ q
le : q ≤ sSup t
lt : ¬q < sSup t
eq : q = sSup t
⊢ ∃ r, Grow s c q (s.np c q) r
Tactic:
rw [eq]
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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
q : ℝ
q0 : 0 ≤ q
le : q ≤ sSup t
lt : ¬q < sSup t
eq : q = sSup t
⊢ ∃ r, Grow s c (sSup t) (s.np c (sSup t)) r
Theorem: Super.grow
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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
q : ℝ
q0 : 0 ≤ q
le : q ≤ sSup t
lt : ¬q < sSup t
eq : q = sSup t
⊢ ∃ r, Grow s c (sSup t) (s.np c (sSup t)) r
Tactic:
clear eq lt le q0 q
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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
⊢ ∃ r, Grow s c (sSup t) (s.np c (sSup t)) r
Theorem: Super.grow
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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
⊢ ∃ r, Grow s c (sSup t) (s.np c (sSup t)) r
Tactic:
rcases exists_seq_tendsto_sSup ne above with ⟨p, mono, tend, sub⟩
Proof state after:
case neg.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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
p : ℕ → ℝ
mono : Monotone p
tend : Tendsto p atTop (𝓝 (sSup t))
sub : ∀ (n : ℕ), p n ∈ t
⊢ ∃ r, Grow s c (sSup t) (s.np c (sSup t)) r
Theorem: Super.grow
Proof state before:
case neg.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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
p : ℕ → ℝ
mono : Monotone p
tend : Tendsto p atTop (𝓝 (sSup t))
sub : ∀ (n : ℕ), p n ∈ t
⊢ ∃ r, Grow s c (sSup t) (s.np c (sSup t)) r
Tactic:
simp only [Set.range_subset_iff, mem_setOf, t] at sub
Proof state after:
case neg.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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
p : ℕ → ℝ
mono : Monotone p
tend : Tendsto p atTop (𝓝 (sSup t))
sub : ∀ (n : ℕ), 0 ≤ p n ∧ ∀ (q : ℝ), 0 ≤ q → q ≤ p n → ∃ r, Grow s c q (s.np c q) r
⊢ ∃ r, Grow s c (sSup t) (s.np c (sSup t)) r
Theorem: Super.grow
Proof state before:
case neg.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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
p : ℕ → ℝ
mono : Monotone p
tend : Tendsto p atTop (𝓝 (sSup t))
sub : ∀ (n : ℕ), 0 ≤ p n ∧ ∀ (q : ℝ), 0 ≤ q → q ≤ p n → ∃ r, Grow s c q (s.np c q) r
⊢ ∃ r, Grow s c (sSup t) (s.np c (sSup t)) r
Tactic:
set pr := fun k ↦ choose (self (sub k))
Proof state after:
case neg.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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
p : ℕ → ℝ
mono : Monotone p
tend : Tendsto p atTop (𝓝 (sSup t))
sub : ∀ (n : ℕ), 0 ≤ p n ∧ ∀ (q : ℝ), 0 ≤ q → q ≤ p n → ∃ r, Grow s c q (s.np c q) r
pr : ℕ → ℂ → ℂ → S := fun k => choose ⋯
⊢ ∃ r, Grow s c (sSup t) (s.np c (sSup t)) r
Theorem: Super.grow
Proof state before:
case neg.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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
p : ℕ → ℝ
mono : Monotone p
tend : Tendsto p atTop (𝓝 (sSup t))
sub : ∀ (n : ℕ), 0 ≤ p n ∧ ∀ (q : ℝ), 0 ≤ q → q ≤ p n → ∃ r, Grow s c q (s.np c q) r
pr : ℕ → ℂ → ℂ → S := fun k => choose ⋯
⊢ ∃ r, Grow s c (sSup t) (s.np c (sSup t)) r
Tactic:
have pg : ∀ k, Grow s c (p k) (s.np c (sSup t)) (pr k) := fun k ↦
  (choose_spec (self (sub k))).mono
    (s.np_mono c (le_csSup above (sub k)) (lt_of_lt_of_le post s.p_le_one))
Proof state after:
case neg.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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
p : ℕ → ℝ
mono : Monotone p
tend : Tendsto p atTop (𝓝 (sSup t))
sub : ∀ (n : ℕ), 0 ≤ p n ∧ ∀ (q : ℝ), 0 ≤ q → q ≤ p n → ∃ r, Grow s c q (s.np c q) r
pr : ℕ → ℂ → ℂ → S := fun k => choose ⋯
pg : ∀ (k : ℕ), Grow s c (p k) (s.np c (sSup t)) (pr k)
⊢ ∃ r, Grow s c (sSup t) (s.np c (sSup t)) r
Theorem: Super.grow
Proof state before:
case neg.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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
p : ℕ → ℝ
mono : Monotone p
tend : Tendsto p atTop (𝓝 (sSup t))
sub : ∀ (n : ℕ), 0 ≤ p n ∧ ∀ (q : ℝ), 0 ≤ q → q ≤ p n → ∃ r, Grow s c q (s.np c q) r
pr : ℕ → ℂ → ℂ → S := fun k => choose ⋯
pg : ∀ (k : ℕ), Grow s c (p k) (s.np c (sSup t)) (pr k)
⊢ ∃ r, Grow s c (sSup t) (s.np c (sSup t)) r
Tactic:
rcases join_r s pg mono tend with ⟨r, loc⟩
Proof state after:
case neg.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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
p : ℕ → ℝ
mono : Monotone p
tend : Tendsto p atTop (𝓝 (sSup t))
sub : ∀ (n : ℕ), 0 ≤ p n ∧ ∀ (q : ℝ), 0 ≤ q → q ≤ p n → ∃ r, Grow s c q (s.np c q) r
pr : ℕ → ℂ → ℂ → S := fun k => choose ⋯
pg : ∀ (k : ℕ), Grow s c (p k) (s.np c (sSup t)) (pr k)
r : ℂ → ℂ → S
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry r) (uncurry (pr k))
⊢ ∃ r, Grow s c (sSup t) (s.np c (sSup t)) r
Theorem: Super.grow
Proof state before:
case neg.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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
p : ℕ → ℝ
mono : Monotone p
tend : Tendsto p atTop (𝓝 (sSup t))
sub : ∀ (n : ℕ), 0 ≤ p n ∧ ∀ (q : ℝ), 0 ≤ q → q ≤ p n → ∃ r, Grow s c q (s.np c q) r
pr : ℕ → ℂ → ℂ → S := fun k => choose ⋯
pg : ∀ (k : ℕ), Grow s c (p k) (s.np c (sSup t)) (pr k)
r : ℂ → ℂ → S
loc : ∀ (k : ℕ) (x : ℂ), Complex.abs x < p k → (𝓝 (c, x)).EventuallyEq (uncurry r) (uncurry (pr k))
⊢ ∃ r, Grow s c (sSup t) (s.np c (sSup t)) r
Tactic:
exact (joined_growOpen s pg tend post pos loc).grow
Proof state after:
no goals
Theorem: Super.grow
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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
q : ℝ
q0 : 0 ≤ q
le : q ≤ sSup t
lt : q < sSup t
⊢ ∃ r, Grow s c q (s.np c q) r
Tactic:
rcases exists_lt_of_lt_csSup ne lt with ⟨q', ⟨_, m⟩, qq⟩
Proof state after:
case pos.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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
q : ℝ
q0 : 0 ≤ q
le : q ≤ sSup t
lt : q < sSup t
q' : ℝ
qq : q < q'
left✝ : 0 ≤ q'
m : ∀ (q : ℝ), 0 ≤ q → q ≤ q' → ∃ r, Grow s c q (s.np c q) r
⊢ ∃ r, Grow s c q (s.np c q) r
Theorem: Super.grow
Proof state before:
case pos.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
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
above : BddAbove t
p0 : ℝ
r0 : ℂ → ℂ → S
pos0 : 0 < p0
g0 : Grow s c p0 0 r0
start : p0 ∈ t
ne : t.Nonempty
pos : 0 < sSup t
missing : sSup t ∉ t
post : sSup t < s.p c
q : ℝ
q0 : 0 ≤ q
le : q ≤ sSup t
lt : q < sSup t
q' : ℝ
qq : q < q'
left✝ : 0 ≤ q'
m : ∀ (q : ℝ), 0 ≤ q → q ≤ q' → ∃ r, Grow s c q (s.np c q) r
⊢ ∃ r, Grow s c q (s.np c q) r
Tactic:
exact m _ q0 qq.le
Proof state after:
no goals
Theorem: Super.has_ray
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
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r
Tactic:
generalize hr : (fun {c p} (h : 0 ≤ p ∧ p < s.p c) ↦ choose (s.grow _ h.1 h.2)) = 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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r
Theorem: Super.has_ray
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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r
Tactic:
have g : ∀ {c p} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h) := by
  intro c p h; rw [← hr]; exact choose_spec _
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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r
Theorem: Super.has_ray
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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r
Tactic:
clear hr
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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r
Theorem: Super.has_ray
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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r
Tactic:
generalize hray : (fun c x : ℂ ↦
  if h : abs x < s.p c then r ⟨Complex.abs.nonneg _, h⟩ c x else a) = ray
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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r
Theorem: Super.has_ray
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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
loc : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r
Tactic:
use ray
Proof state after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
loc : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
⊢ ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) ray
Theorem: Super.has_ray
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
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
loc : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
⊢ ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) ray
Tactic:
intro c p p0 h
Proof state after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
loc : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
c : ℂ
p : ℝ
p0 : 0 ≤ p
h : p < s.p c
⊢ Grow s c p (s.np c p) ray
Theorem: Super.has_ray
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
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
loc : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
c : ℂ
p : ℝ
p0 : 0 ≤ p
h : p < s.p c
⊢ Grow s c p (s.np c p) ray
Tactic:
exact (g ⟨p0, h⟩).congr (loc ⟨p0, h⟩).symm
Proof state after:
no goals