Theorem: NontrivialHolomorphicAt.eventually_ne (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, w ≠ z → f w ≠ f z
Tactic:
have ca : _root_.HolomorphicAt I I (fun _ ↦ f z) z := holomorphicAt_const
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
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z

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
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Tactic:
cases' n.holomorphicAt.eventually_eq_or_eventually_ne ca with h h
State after:
case 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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (w : S) in 𝓝 z, f w = f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z

case 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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z

State before:
case 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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (w : S) in 𝓝 z, f w = f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Tactic:
have b := h.and_frequently n.nonconst
State after:
case 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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (w : S) in 𝓝 z, f w = f z
b : ∃ᶠ (x : S) in 𝓝 z, f x = f z ∧ f x ≠ f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z

State before:
case 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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (w : S) in 𝓝 z, f w = f z
b : ∃ᶠ (x : S) in 𝓝 z, f x = f z ∧ f x ≠ f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Tactic:
simp only [and_not_self_iff, Filter.frequently_false] at b
State after:
no goals

State before:
case 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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Tactic:
simp only [eventually_nhdsWithin_iff, mem_compl_singleton_iff] at h
State after:
case 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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z

State before:
case 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
z : S
n : NontrivialHolomorphicAt f z
ca : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun x => f z) z
h : ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ f z
⊢ ∀ᶠ (w : S) in 𝓝 z, w ≠ z → f w ≠ f z
Tactic:
convert h
State after:
no goals