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✝ : T2Space T
f : S → T
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ ∀ w ∈ s, f w = a
Tactic:
generalize ht : {z | z ∈ s ∧ ∀ᶠ w in 𝓝 z, f w = a} = t
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ ∀ w ∈ s, f w = a

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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ ∀ w ∈ s, f w = a
Tactic:
suffices st : s ⊆ t by rw [← ht] at st; exact fun z m ↦ (st m).2.self_of_nhds
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ s ⊆ t

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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ s ⊆ t
Tactic:
refine p.subset_of_closure_inter_subset ?_ ?_ ?_
State after:
case refine_1
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ IsOpen t

case refine_2
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ (s ∩ t).Nonempty

case refine_3
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ closure t ∩ s ⊆ t

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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
st : s ⊆ t
⊢ ∀ w ∈ s, f w = a
Tactic:
rw [← ht] at st
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
st : s ⊆ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}
⊢ ∀ w ∈ s, f w = a

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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
st : s ⊆ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}
⊢ ∀ w ∈ s, f w = a
Tactic:
exact fun z m ↦ (st m).2.self_of_nhds
State after:
no goals

State before:
case refine_1
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ IsOpen t
Tactic:
rw [isOpen_iff_eventually]
State after:
case refine_1
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ ∀ x ∈ t, ∀ᶠ (y : S) in 𝓝 x, y ∈ t

State before:
case refine_1
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ ∀ x ∈ t, ∀ᶠ (y : S) in 𝓝 x, y ∈ t
Tactic:
intro z m
State after:
case refine_1
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : z ∈ t
⊢ ∀ᶠ (y : S) in 𝓝 z, y ∈ t

State before:
case refine_1
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : z ∈ t
⊢ ∀ᶠ (y : S) in 𝓝 z, y ∈ t
Tactic:
simp only [Set.mem_setOf_eq, ← ht] at m ⊢
State after:
case refine_1
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ ∀ᶠ (y : S) in 𝓝 z, y ∈ s ∧ ∀ᶠ (w : S) in 𝓝 y, f w = a

State before:
case refine_1
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ ∀ᶠ (y : S) in 𝓝 z, y ∈ s ∧ ∀ᶠ (w : S) in 𝓝 y, f w = a
Tactic:
exact ((o.eventually_mem m.1).and m.2.eventually_nhds).mp (eventually_of_forall fun y h ↦ h)
State after:
no goals

State before:
case refine_2
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ (s ∩ t).Nonempty
Tactic:
use z
State after:
case h
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ z ∈ s ∩ t

State before:
case h
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ z ∈ s ∩ t
Tactic:
simp only [Set.mem_inter_iff, ← ht]
State after:
case h
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ z ∈ s ∧ z ∈ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}

State before:
case h
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ z ∈ s ∧ z ∈ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}
Tactic:
exact ⟨zs, zs, c⟩
State after:
no goals

State before:
case refine_3
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z : S
a : T
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
⊢ closure t ∩ s ⊆ t
Tactic:
intro z m
State after:
case refine_3
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : z ∈ closure t ∩ s
⊢ z ∈ t

State before:
case refine_3
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : z ∈ closure t ∩ s
⊢ z ∈ t
Tactic:
simp only [Set.mem_inter_iff, mem_closure_iff_frequently] at m
State after:
case refine_3
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
⊢ z ∈ t

State before:
case refine_3
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
⊢ z ∈ t
Tactic:
have aa : HolomorphicAt I I (fun _ ↦ a) z := holomorphicAt_const
State after:
case refine_3
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
⊢ z ∈ t

State before:
case refine_3
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
⊢ z ∈ t
Tactic:
cases' (fa _ m.2).eventually_eq_or_eventually_ne aa with h h
State after:
case refine_3.inl
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ z ∈ t

case refine_3.inr
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ a
⊢ z ∈ t

State before:
case refine_3.inl
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ z ∈ t
Tactic:
rw [← ht]
State after:
case refine_3.inl
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ z ∈ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}

State before:
case refine_3.inl
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (w : S) in 𝓝 z, f w = a
⊢ z ∈ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}
Tactic:
use m.2, h
State after:
no goals

State before:
case refine_3.inr
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ a
⊢ z ∈ t
Tactic:
simp only [eventually_nhdsWithin_iff, Set.mem_compl_singleton_iff] at h
State after:
case refine_3.inr
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
⊢ z ∈ t

State before:
case refine_3.inr
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
⊢ z ∈ t
Tactic:
have m' := m.1
State after:
case refine_3.inr
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ∃ᶠ (x : S) in 𝓝 z, x ∈ t
⊢ z ∈ t

State before:
case refine_3.inr
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ∃ᶠ (x : S) in 𝓝 z, x ∈ t
⊢ z ∈ t
Tactic:
contrapose m'
State after:
case refine_3.inr
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
⊢ ¬∃ᶠ (x : S) in 𝓝 z, x ∈ t

State before:
case refine_3.inr
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
⊢ ¬∃ᶠ (x : S) in 𝓝 z, x ∈ t
Tactic:
simp only [Filter.not_frequently]
State after:
case refine_3.inr
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
⊢ ∀ᶠ (x : S) in 𝓝 z, x ∉ t

State before:
case refine_3.inr
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
⊢ ∀ᶠ (x : S) in 𝓝 z, x ∉ t
Tactic:
refine h.mp (eventually_of_forall ?_)
State after:
case refine_3.inr
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
⊢ ∀ (x : S), (x ≠ z → f x ≠ a) → x ∉ t

State before:
case refine_3.inr
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
⊢ ∀ (x : S), (x ≠ z → f x ≠ a) → x ∉ t
Tactic:
intro x i
State after:
case refine_3.inr
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
i : x ≠ z → f x ≠ a
⊢ x ∉ t

State before:
case refine_3.inr
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
i : x ≠ z → f x ≠ a
⊢ x ∉ t
Tactic:
by_cases xz : x = z
State after:
case pos
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
i : x ≠ z → f x ≠ a
xz : x = z
⊢ x ∉ t

case neg
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
i : x ≠ z → f x ≠ a
xz : ¬x = z
⊢ x ∉ t

State before:
case pos
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
i : x ≠ z → f x ≠ a
xz : x = z
⊢ x ∉ t

case neg
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
i : x ≠ z → f x ≠ a
xz : ¬x = z
⊢ x ∉ t
Tactic:
rwa [xz]
State after:
case neg
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
i : x ≠ z → f x ≠ a
xz : ¬x = z
⊢ x ∉ t

State before:
case neg
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
i : x ≠ z → f x ≠ a
xz : ¬x = z
⊢ x ∉ t
Tactic:
specialize i xz
State after:
case neg
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
xz : ¬x = z
i : f x ≠ a
⊢ x ∉ t

State before:
case neg
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
xz : ¬x = z
i : f x ≠ a
⊢ x ∉ t
Tactic:
contrapose i
State after:
case neg
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
xz : ¬x = z
i : ¬x ∉ t
⊢ ¬f x ≠ a

State before:
case neg
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
xz : ¬x = z
i : ¬x ∉ t
⊢ ¬f x ≠ a
Tactic:
simp only [not_not, ← ht] at i ⊢
State after:
case neg
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
xz : ¬x = z
i : x ∈ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}
⊢ f x = a

State before:
case neg
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
s : Set S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
z✝ : S
a : T
zs : z✝ ∈ s
o : IsOpen s
p : IsPreconnected s
c : ∀ᶠ (w : S) in 𝓝 z✝, f w = a
t : Set S
ht : {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a} = t
z : S
m : (∃ᶠ (x : S) in 𝓝 z, x ∈ t) ∧ z ∈ s
aa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => a) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ a
m' : ¬z ∈ t
x : S
xz : ¬x = z
i : x ∈ {z | z ∈ s ∧ ∀ᶠ (w : S) in 𝓝 z, f w = a}
⊢ f x = a
Tactic:
exact i.2.self_of_nhds
State after:
no goals