Theorem: HolomorphicOn.const_of_locally_const' (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✝¹ : LocallyConnectedSpace S
inst✝ : T2Space T
f : S → T
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ ∀ w ∈ s, f w = a
Tactic:
rcases local_preconnected_nhdsSet p (isOpen_holomorphicAt.mem_nhdsSet.mpr fa)
  with ⟨u, uo, su, ua, uc⟩
State after:
case 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✝¹ : LocallyConnectedSpace S
inst✝ : T2Space T
f : S → T
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
u : Set S
uo : IsOpen u
su : s ⊆ u
ua : u ⊆ {x | HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x}
uc : IsPreconnected u
⊢ ∀ w ∈ s, f w = a

State before:
case 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✝¹ : LocallyConnectedSpace S
inst✝ : T2Space T
f : S → T
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
u : Set S
uo : IsOpen u
su : s ⊆ u
ua : u ⊆ {x | HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x}
uc : IsPreconnected u
⊢ ∀ w ∈ s, f w = a
Tactic:
exact fun w ws ↦ HolomorphicOn.const_of_locally_const (fun _ m ↦ ua m) (su zs) uo uc c w (su ws)
State after:
no goals