internlm/Lean-Github huggingface dataset:
Theorem: Super.has_ray
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
⊢ ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
Tactic:
intro c p h
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
⊢ Grow s c p (s.np c p) (r h)
Theorem: Super.has_ray
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
⊢ Grow s c p (s.np c p) (r h)
Tactic:
rw [← hr]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
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)
Theorem: Super.has_ray
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
hr : (fun {c} {p} h => choose ⋯) = r
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 _
Proof state after:
no goals
Theorem: Super.has_ray
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → 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
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
⊢ (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry ray) (uncurry (r h))
Theorem: Super.has_ray
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
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⟩
Proof 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))
Theorem: Super.has_ray
Proof 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⟩
Proof 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))
Theorem: Super.has_ray
Proof 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⟩
Proof 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))
Theorem: Super.has_ray
Proof 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
Proof 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))
Theorem: Super.has_ray
Proof 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)
Proof 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))
Theorem: Super.has_ray
Proof 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'
Proof 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))
Theorem: Super.has_ray
Proof 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⟩
Proof 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))
Theorem: Super.has_ray
Proof 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⟩
Proof 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))
Theorem: Super.has_ray
Proof 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, ?_, ?_⟩
Proof 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
Theorem: Super.has_ray
Proof 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)
Proof state after:
no goals
Theorem: Super.has_ray
Proof 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⟩
Proof 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)
Theorem: Super.has_ray
Proof 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 ⊢
Proof 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