internlm/Lean-Github huggingface dataset:
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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
have above : BddAbove t := bddAbove_def.mpr ⟨1, fun p m ↦ (t1 p m).le⟩
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
above : BddAbove t
⊢ ∀ (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
t1 : ∀ p ∈ t, p < 1
above : BddAbove t
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
rcases s.grow_start c with ⟨p0, r0, pos0, g0⟩
Proof state after:
case 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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Theorem: Super.grow
Proof state before:
case 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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
have start : p0 ∈ t := by
  use g0.nonneg; intro q q0 qp; use r0; exact (g0.anti q0 qp).mono (Nat.zero_le _)
Proof state after:
case 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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Theorem: Super.grow
Proof state before:
case 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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
have ne : t.Nonempty := ⟨p0, start⟩
Proof state after:
case 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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Theorem: Super.grow
Proof state before:
case 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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
have pos : 0 < sSup t := lt_csSup_of_lt above start pos0
Proof state after:
case 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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Theorem: Super.grow
Proof state before:
case 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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
by_cases missing : sSup t ∈ 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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) 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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) 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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
by_cases post : sSup t < s.p c
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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) 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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) 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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
simp only [not_lt] at post
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 : s.p c ≤ sSup t
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) 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 : s.p c ≤ sSup t
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
intro p p0 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 : s.p c ≤ sSup t
p : ℝ
p0 : 0 ≤ p
lt : p < s.p c
⊢ ∃ r, Grow s c p (s.np c p) 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 : s.p c ≤ sSup t
p : ℝ
p0 : 0 ≤ p
lt : p < s.p c
⊢ ∃ r, Grow s c p (s.np c p) r
Tactic:
rcases exists_lt_of_lt_csSup ne (lt_of_lt_of_le lt post) with ⟨q, m, pq⟩
Proof state after:
case neg.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 : s.p c ≤ sSup t
p : ℝ
p0 : 0 ≤ p
lt : p < s.p c
q : ℝ
m : q ∈ t
pq : p < q
⊢ ∃ r, Grow s c p (s.np c p) r
Theorem: Super.grow
Proof state before:
case neg.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 : s.p c ≤ sSup t
p : ℝ
p0 : 0 ≤ p
lt : p < s.p c
q : ℝ
m : q ∈ t
pq : p < q
⊢ ∃ r, Grow s c p (s.np c p) r
Tactic:
exact m.2 _ p0 pq.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
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 ∈ t, p < 1
Tactic:
intro p m
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 : ℝ
m : p ∈ t
⊢ p < 1
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 : ℝ
m : p ∈ t
⊢ p < 1
Tactic:
rcases self m with ⟨r, g⟩
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
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 : ℝ
m : p ∈ t
r : ℂ → ℂ → S
g : Grow s c p (s.np c p) r
⊢ p < 1
Theorem: Super.grow
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
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 : ℝ
m : p ∈ t
r : ℂ → ℂ → S
g : Grow s c p (s.np c p) r
⊢ p < 1
Tactic:
exact g.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
⊢ p0 ∈ t
Tactic:
use g0.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
⊢ ∀ (q : ℝ), 0 ≤ q → q ≤ p0 → ∃ 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
⊢ ∀ (q : ℝ), 0 ≤ q → q ≤ p0 → ∃ 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
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p0
⊢ ∃ 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
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p0
⊢ ∃ r, Grow s c q (s.np c q) r
Tactic:
use r0
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
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p0
⊢ Grow s c q (s.np c q) r0
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
q : ℝ
q0 : 0 ≤ q
qp : q ≤ p0
⊢ Grow s c q (s.np c q) r0
Tactic:
exact (g0.anti q0 qp).mono (Nat.zero_le _)
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
⊢ ∀ (p : ℝ), 0 ≤ p → p < s.p c → ∃ r, Grow s c p (s.np c p) r
Tactic:
rcases self missing with ⟨r, g⟩
Proof state after:
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