Theorem: eqn_near (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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
Tactic:
have m : ∀ᶠ y : ℂ × ℂ in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near := by
  refine ContinuousAt.eventually_mem ?_ (s.isOpen_near.mem_nhds mem)
  exact continuousAt_fst.prod (s.continuousAt_iter continuousAt_fst holo.continuousAt)
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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y

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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
Tactic:
apply holo.eventually.mp
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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x

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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x
Tactic:
apply loc.mp
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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    s.bottcherNear x.1 ((f x.1)^[n] (r x.1 x.2)) = x.2 ^ d ^ n → HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x

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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    s.bottcherNear x.1 ((f x.1)^[n] (r x.1 x.2)) = x.2 ^ d ^ n → HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x
Tactic:
apply m.mp
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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    (x.1, (f x.1)^[n] (r x.1 x.2)) ∈ s.near →
      s.bottcherNear x.1 ((f x.1)^[n] (r x.1 x.2)) = x.2 ^ d ^ n →
        HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x

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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    (x.1, (f x.1)^[n] (r x.1 x.2)) ∈ s.near →
      s.bottcherNear x.1 ((f x.1)^[n] (r x.1 x.2)) = x.2 ^ d ^ n →
        HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x
Tactic:
apply eventually_of_forall
State after:
case hp
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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ (x : ℂ × ℂ),
    (x.1, (f x.1)^[n] (r x.1 x.2)) ∈ s.near →
      s.bottcherNear x.1 ((f x.1)^[n] (r x.1 x.2)) = x.2 ^ d ^ n →
        HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x

State before:
case hp
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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ (x : ℂ × ℂ),
    (x.1, (f x.1)^[n] (r x.1 x.2)) ∈ s.near →
      s.bottcherNear x.1 ((f x.1)^[n] (r x.1 x.2)) = x.2 ^ d ^ n →
        HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x
Tactic:
intro _ m l h
State after:
case hp
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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
x✝ : ℂ × ℂ
m : (x✝.1, (f x✝.1)^[n] (r x✝.1 x✝.2)) ∈ s.near
l : s.bottcherNear x✝.1 ((f x✝.1)^[n] (r x✝.1 x✝.2)) = x✝.2 ^ d ^ n
h : HolomorphicAt (I.prod I) I (uncurry r) x✝
⊢ Eqn s n r x✝

State before:
case hp
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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
x✝ : ℂ × ℂ
m : (x✝.1, (f x✝.1)^[n] (r x✝.1 x✝.2)) ∈ s.near
l : s.bottcherNear x✝.1 ((f x✝.1)^[n] (r x✝.1 x✝.2)) = x✝.2 ^ d ^ n
h : HolomorphicAt (I.prod I) I (uncurry r) x✝
⊢ Eqn s n r x✝
Tactic:
exact ⟨h, m, l⟩
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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
Tactic:
refine ContinuousAt.eventually_mem ?_ (s.isOpen_near.mem_nhds mem)
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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
⊢ ContinuousAt (fun y => (y.1, (f y.1)^[n] (r y.1 y.2))) (c, x)

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
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
⊢ ContinuousAt (fun y => (y.1, (f y.1)^[n] (r y.1 y.2))) (c, x)
Tactic:
exact continuousAt_fst.prod (s.continuousAt_iter continuousAt_fst holo.continuousAt)
State after:
no goals