internlm/Lean-Github huggingface dataset:
Theorem: Super.grow
Proof state before:
case pos.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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
rcases g.open with ⟨p, sp, g'⟩
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) 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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
suffices m : p ∈ t by linarith [le_csSup above m]
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
⊢ p ∈ t
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
⊢ p ∈ t
Tactic:
use g'.self_of_nhds.nonneg
Proof state after:
case right
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
⊢ ∀ (q : ℝ), 0 ≤ q → q ≤ p → ∃ r, Grow s c q (s.np c q) r
Theorem: Super.grow
Proof state before:
case right
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
⊢ ∀ (q : ℝ), 0 ≤ q → q ≤ p → ∃ r, Grow s c q (s.np c q) r
Tactic:
intro q q0 qp
Proof state after:
case right
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p
⊢ ∃ r, Grow s c q (s.np c q) r
Theorem: Super.grow
Proof state before:
case right
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p
⊢ ∃ r, Grow s c q (s.np c q) r
Tactic:
by_cases le : q ≤ sSup t
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
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p
le : q ≤ sSup t
⊢ ∃ r, Grow s c q (s.np c q) r

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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p
le : ¬q ≤ sSup t
⊢ ∃ r, Grow s c q (s.np c q) r
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p
le : q ≤ sSup t
⊢ ∃ r, Grow s c q (s.np c q) r

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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p
le : ¬q ≤ sSup t
⊢ ∃ r, Grow s c q (s.np c q) r
Tactic:
exact missing.2 _ q0 le
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p
le : ¬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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p
le : ¬q ≤ sSup t
⊢ ∃ r, Grow s c q (s.np c q) r
Tactic:
use r
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
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p
le : ¬q ≤ sSup t
⊢ Grow s c q (s.np c q) r
Theorem: Super.grow
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
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p
le : ¬q ≤ sSup t
⊢ Grow s c q (s.np c q) r
Tactic:
simp only [not_le] at le
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
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p
le : sSup t < q
⊢ Grow s c q (s.np c q) r
Theorem: Super.grow
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
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p
le : sSup t < q
⊢ Grow s c q (s.np c q) r
Tactic:
exact (g'.self_of_nhds.anti q0 qp).mono (s.np_mono c le.le (lt_of_le_of_lt qp g'.self_of_nhds.p1))
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
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
r : ℂ → ℂ → S
g : Grow s c (sSup t) (s.np c (sSup t)) r
p : ℝ
sp : sSup t < p
g' : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p (s.np c (sSup t)) r
m : p ∈ t
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
linarith [le_csSup above m]
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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
exfalso
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
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
⊢ False
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
⊢ False
Tactic:
apply missing
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
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
⊢ sSup t ∈ t
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
⊢ sSup t ∈ t
Tactic:
use pos.le
Proof state after:
case right
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 : ℝ), 0 ≤ q → q ≤ sSup t → ∃ r, Grow s c q (s.np c q) r
Theorem: Super.grow
Proof state before:
case right
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 : ℝ), 0 ≤ q → q ≤ sSup t → ∃ r, Grow s c q (s.np c q) r
Tactic:
intro q q0 le
Proof state after:
case right
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
⊢ ∃ r, Grow s c q (s.np c q) r
Theorem: Super.grow
Proof state before:
case right
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
⊢ ∃ r, Grow s c q (s.np c q) r
Tactic:
by_cases lt : q < sSup t
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
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

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