Theorem: Super.has_ray (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
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r
Tactic:
generalize hr : (fun {c p} (h : 0 ≤ p ∧ p < s.p c) ↦ choose (s.grow _ h.1 h.2)) = r
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r
Tactic:
have g : ∀ {c p} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h) := by
  intro c p h; rw [← hr]; exact choose_spec _
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r
Tactic:
clear hr
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r
Tactic:
generalize hray : (fun c x : ℂ ↦
  if h : abs x < s.p c then r ⟨Complex.abs.nonneg _, h⟩ c x else a) = ray
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
loc : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
⊢ ∃ r, ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) r
Tactic:
use ray
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
loc : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
⊢ ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) ray

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
loc : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
⊢ ∀ (c : ℂ) (p : ℝ), 0 ≤ p → p < s.p c → Grow s c p (s.np c p) ray
Tactic:
intro c p p0 h
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
loc : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
c : ℂ
p : ℝ
p0 : 0 ≤ p
h : p < s.p c
⊢ Grow s c p (s.np c p) ray

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
loc : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
c : ℂ
p : ℝ
p0 : 0 ≤ p
h : p < s.p c
⊢ Grow s c p (s.np c p) ray
Tactic:
exact (g ⟨p0, h⟩).congr (loc ⟨p0, h⟩).symm
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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
⊢ ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
Tactic:
intro c p h
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
⊢ Grow s c p (s.np c p) (r h)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
⊢ Grow s c p (s.np c p) (r h)
Tactic:
rw [← hr]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
⊢ Grow s c p (s.np c p) ((fun {c} {p} h => choose ⋯) h)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
⊢ Grow s c p (s.np c p) ((fun {c} {p} h => choose ⋯) h)
Tactic:
exact choose_spec _
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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
⊢ ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
Tactic:
intro c p h
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
Tactic:
rcases(g h).open with ⟨q', pq', gh⟩
State after:
case 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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q' : ℝ
pq' : p < q'
gh : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' q' (s.np c p) (r h)
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))

State before:
case 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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q' : ℝ
pq' : p < q'
gh : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' q' (s.np c p) (r h)
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
Tactic:
rcases exists_between (lt_min pq' h.2) with ⟨q, pq, qlo⟩
State after:
case 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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q' : ℝ
pq' : p < q'
gh : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' q' (s.np c p) (r h)
q : ℝ
pq : p < q
qlo : q < min q' (s.p c)
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))

State before:
case 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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q' : ℝ
pq' : p < q'
gh : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' q' (s.np c p) (r h)
q : ℝ
pq : p < q
qlo : q < min q' (s.p c)
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
Tactic:
rcases lt_min_iff.mp qlo with ⟨qq', qs⟩
State after:
case intro.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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q' : ℝ
pq' : p < q'
gh : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' q' (s.np c p) (r h)
q : ℝ
pq : p < q
qlo : q < min q' (s.p c)
qq' : q < q'
qs : q < s.p c
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))

State before:
case intro.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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q' : ℝ
pq' : p < q'
gh : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' q' (s.np c p) (r h)
q : ℝ
pq : p < q
qlo : q < min q' (s.p c)
qq' : q < q'
qs : q < s.p c
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
Tactic:
have q0 : 0 ≤ q := _root_.trans h.1 pq.le
State after:
case intro.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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q' : ℝ
pq' : p < q'
gh : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' q' (s.np c p) (r h)
q : ℝ
pq : p < q
qlo : q < min q' (s.p c)
qq' : q < q'
qs : q < s.p c
q0 : 0 ≤ q
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))

State before:
case intro.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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q' : ℝ
pq' : p < q'
gh : ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' q' (s.np c p) (r h)
q : ℝ
pq : p < q
qlo : q < min q' (s.p c)
qq' : q < q'
qs : q < s.p c
q0 : 0 ≤ q
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
Tactic:
replace gh := gh.mp (eventually_of_forall fun c' g ↦ g.anti q0 qq'.le)
State after:
case intro.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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q' : ℝ
pq' : p < q'
q : ℝ
pq : p < q
qlo : q < min q' (s.p c)
qq' : q < q'
qs : q < s.p c
q0 : 0 ≤ q
gh : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))

State before:
case intro.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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q' : ℝ
pq' : p < q'
q : ℝ
pq : p < q
qlo : q < min q' (s.p c)
qq' : q < q'
qs : q < s.p c
q0 : 0 ≤ q
gh : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
Tactic:
clear qlo qq' pq' q'
State after:
case intro.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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))

State before:
case intro.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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
Tactic:
rcases eventually_nhds_iff.mp gh with ⟨t0, gh, ot0, ct0⟩
State after:
case intro.intro.intro.intro.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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))

State before:
case intro.intro.intro.intro.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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
Tactic:
rcases eventually_nhds_iff.mp (s.lowerSemicontinuous_p _ _ qs) with ⟨t1, lo, ot1, ct1⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))

State before:
case intro.intro.intro.intro.intro.intro.intro.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
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
Tactic:
refine eventually_nhdsSet_iff_exists.mpr
    ⟨(t0 ∩ t1) ×ˢ ball 0 q, (ot0.inter ot1).prod isOpen_ball, ?_, ?_⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
⊢ {c} ×ˢ closedBall 0 p ⊆ (t0 ∩ t1) ×ˢ ball 0 q

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
⊢ ∀ x ∈ (t0 ∩ t1) ×ˢ ball 0 q, uncurry ray x = uncurry (r h) x

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
⊢ {c} ×ˢ closedBall 0 p ⊆ (t0 ∩ t1) ×ˢ ball 0 q
Tactic:
exact prod_mono (singleton_subset_iff.mpr ⟨ct0, ct1⟩) (Metric.closedBall_subset_ball pq)
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
⊢ ∀ x ∈ (t0 ∩ t1) ×ˢ ball 0 q, uncurry ray x = uncurry (r h) x
Tactic:
intro ⟨e, x⟩ ⟨⟨et0, et1⟩, xq⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : (e, x).1 ∈ t0
et1 : (e, x).1 ∈ t1
xq : (e, x).2 ∈ ball 0 q
⊢ uncurry ray (e, x) = uncurry (r h) (e, x)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : (e, x).1 ∈ t0
et1 : (e, x).1 ∈ t1
xq : (e, x).2 ∈ ball 0 q
⊢ uncurry ray (e, x) = uncurry (r h) (e, x)
Tactic:
simp only [uncurry] at et0 et1 xq ⊢
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : x ∈ ball 0 q
⊢ ray e x = r h e x

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : x ∈ ball 0 q
⊢ ray e x = r h e x
Tactic:
simp only [mem_ball, Complex.dist_eq, sub_zero] at xq
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
⊢ ray e x = r h e x

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
⊢ ray e x = r h e x
Tactic:
have hx : 0 ≤ abs x ∧ abs x < s.p e := ⟨Complex.abs.nonneg _, _root_.trans xq (lo _ et1)⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
hx : 0 ≤ Complex.abs x ∧ Complex.abs x < s.p e
⊢ ray e x = r h e x

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
hx : 0 ≤ Complex.abs x ∧ Complex.abs x < s.p e
⊢ ray e x = r h e x
Tactic:
simp only [← hray, dif_pos hx.2]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
hx : 0 ≤ Complex.abs x ∧ Complex.abs x < s.p e
⊢ r ⋯ e x = r h e x

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
hx : 0 ≤ Complex.abs x ∧ Complex.abs x < s.p e
⊢ r ⋯ e x = r h e x
Tactic:
refine ((g hx).unique (gh _ et0) xq.le).self_of_nhdsSet (x := ⟨e, x⟩) ⟨rfl, ?_⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
hx : 0 ≤ Complex.abs x ∧ Complex.abs x < s.p e
⊢ (e, x).2 ∈ closedBall 0 (Complex.abs x)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
hx : 0 ≤ Complex.abs x ∧ Complex.abs x < s.p e
⊢ (e, x).2 ∈ closedBall 0 (Complex.abs x)
Tactic:
simp only [mem_closedBall, Complex.dist_eq, sub_zero, le_refl]
State after:
no goals