Theorem: Super.grow (Ray/Dynamics/Grow.lean)

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}
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

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 _)
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

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
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

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⟩
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

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⟩
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

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 _)
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

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⟩
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

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
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

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
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

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
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

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
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

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
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

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⟩
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

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
State after:
no goals

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
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

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⟩
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

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
State after:
no goals

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
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

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
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

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
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

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 _)
State after:
no goals

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⟩
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

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'⟩
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

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]
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

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
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

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
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

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
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

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
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

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
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

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
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

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))
State after:
no goals

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]
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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)
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

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]
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

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
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

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⟩
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

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
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

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))
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

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))
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

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⟩
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

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
State after:
no goals

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⟩
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

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
State after:
no goals