Theorem: NontrivialHolomorphicAt.eventually (Ray/AnalyticManifold/Nontrivial.lean)

State before:
X : Type
inst✝⁷ : TopologicalSpace X
S : Type
inst✝⁶ : TopologicalSpace S
inst✝⁵ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝⁴ : TopologicalSpace T
inst✝³ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝² : TopologicalSpace U
inst✝¹ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
⊢ ∀ᶠ (w : S) in 𝓝 z, NontrivialHolomorphicAt f w
Tactic:
have lc : LocallyConnectedSpace S := ChartedSpace.locallyConnectedSpace ℂ _
State after:
X : Type
inst✝⁷ : TopologicalSpace X
S : Type
inst✝⁶ : TopologicalSpace S
inst✝⁵ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝⁴ : TopologicalSpace T
inst✝³ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝² : TopologicalSpace U
inst✝¹ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
⊢ ∀ᶠ (w : S) in 𝓝 z, NontrivialHolomorphicAt f w

State before:
X : Type
inst✝⁷ : TopologicalSpace X
S : Type
inst✝⁶ : TopologicalSpace S
inst✝⁵ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝⁴ : TopologicalSpace T
inst✝³ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝² : TopologicalSpace U
inst✝¹ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
⊢ ∀ᶠ (w : S) in 𝓝 z, NontrivialHolomorphicAt f w
Tactic:
rcases eventually_nhds_iff.mp n.holomorphicAt.eventually with ⟨s, fa, os, zs⟩
State after:
case intro.intro.intro
X : Type
inst✝⁷ : TopologicalSpace X
S : Type
inst✝⁶ : TopologicalSpace S
inst✝⁵ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝⁴ : TopologicalSpace T
inst✝³ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝² : TopologicalSpace U
inst✝¹ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
⊢ ∀ᶠ (w : S) in 𝓝 z, NontrivialHolomorphicAt f w

State before:
case intro.intro.intro
X : Type
inst✝⁷ : TopologicalSpace X
S : Type
inst✝⁶ : TopologicalSpace S
inst✝⁵ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝⁴ : TopologicalSpace T
inst✝³ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝² : TopologicalSpace U
inst✝¹ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
⊢ ∀ᶠ (w : S) in 𝓝 z, NontrivialHolomorphicAt f w
Tactic:
rcases locallyConnectedSpace_iff_open_connected_subsets.mp lc z s (os.mem_nhds zs) with
  ⟨t, ts, ot, zt, ct⟩
State after:
case intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁷ : TopologicalSpace X
S : Type
inst✝⁶ : TopologicalSpace S
inst✝⁵ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝⁴ : TopologicalSpace T
inst✝³ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝² : TopologicalSpace U
inst✝¹ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
ct : IsConnected t
⊢ ∀ᶠ (w : S) in 𝓝 z, NontrivialHolomorphicAt f w

State before:
case intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁷ : TopologicalSpace X
S : Type
inst✝⁶ : TopologicalSpace S
inst✝⁵ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝⁴ : TopologicalSpace T
inst✝³ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝² : TopologicalSpace U
inst✝¹ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
ct : IsConnected t
⊢ ∀ᶠ (w : S) in 𝓝 z, NontrivialHolomorphicAt f w
Tactic:
rw [eventually_nhds_iff]
State after:
case intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁷ : TopologicalSpace X
S : Type
inst✝⁶ : TopologicalSpace S
inst✝⁵ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝⁴ : TopologicalSpace T
inst✝³ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝² : TopologicalSpace U
inst✝¹ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
ct : IsConnected t
⊢ ∃ t, (∀ x ∈ t, NontrivialHolomorphicAt f x) ∧ IsOpen t ∧ z ∈ t

State before:
case intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁷ : TopologicalSpace X
S : Type
inst✝⁶ : TopologicalSpace S
inst✝⁵ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝⁴ : TopologicalSpace T
inst✝³ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝² : TopologicalSpace U
inst✝¹ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
ct : IsConnected t
⊢ ∃ t, (∀ x ∈ t, NontrivialHolomorphicAt f x) ∧ IsOpen t ∧ z ∈ t
Tactic:
refine ⟨t, ?_, ot, zt⟩
State after:
case intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁷ : TopologicalSpace X
S : Type
inst✝⁶ : TopologicalSpace S
inst✝⁵ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝⁴ : TopologicalSpace T
inst✝³ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝² : TopologicalSpace U
inst✝¹ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
ct : IsConnected t
⊢ ∀ x ∈ t, NontrivialHolomorphicAt f x

State before:
case intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁷ : TopologicalSpace X
S : Type
inst✝⁶ : TopologicalSpace S
inst✝⁵ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝⁴ : TopologicalSpace T
inst✝³ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝² : TopologicalSpace U
inst✝¹ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s✝ : Set ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
ct : IsConnected t
⊢ ∀ x ∈ t, NontrivialHolomorphicAt f x
Tactic:
exact n.on_preconnected (HolomorphicOn.mono fa ts) zt ot ct.isPreconnected
State after:
no goals