Theorem: nontrivialHolomorphicAt_of_order (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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : orderAt f z ≠ 0
⊢ NontrivialHolomorphicAt f z
Tactic:
use fa.holomorphicAt I I
State after:
case nonconst
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : orderAt f z ≠ 0
⊢ ∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z

State before:
case nonconst
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : orderAt f z ≠ 0
⊢ ∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z
Tactic:
contrapose h
State after:
case nonconst
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ¬∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z
⊢ ¬orderAt f z ≠ 0

State before:
case nonconst
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ¬∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z
⊢ ¬orderAt f z ≠ 0
Tactic:
simp only [Filter.not_frequently, not_not] at h ⊢
State after:
case nonconst
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ orderAt f z = 0

State before:
case nonconst
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ orderAt f z = 0
Tactic:
have fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z :=
  hasFPowerSeriesAt_const.congr (Filter.EventuallyEq.symm h)
State after:
case nonconst
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
⊢ orderAt f z = 0

State before:
case nonconst
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
⊢ orderAt f z = 0
Tactic:
simp only [fp.orderAt_unique]
State after:
case nonconst
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
⊢ (constFormalMultilinearSeries ℂ ℂ (f z)).order = 0

State before:
case nonconst
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
⊢ (constFormalMultilinearSeries ℂ ℂ (f z)).order = 0
Tactic:
by_contra p0
State after:
case nonconst
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
p0 : ¬(constFormalMultilinearSeries ℂ ℂ (f z)).order = 0
⊢ False

State before:
case nonconst
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
p0 : ¬(constFormalMultilinearSeries ℂ ℂ (f z)).order = 0
⊢ False
Tactic:
have b := FormalMultilinearSeries.apply_order_ne_zero' p0
State after:
case nonconst
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
p0 : ¬(constFormalMultilinearSeries ℂ ℂ (f z)).order = 0
b : constFormalMultilinearSeries ℂ ℂ (f z) (constFormalMultilinearSeries ℂ ℂ (f z)).order ≠ 0
⊢ False

State before:
case nonconst
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
p0 : ¬(constFormalMultilinearSeries ℂ ℂ (f z)).order = 0
b : constFormalMultilinearSeries ℂ ℂ (f z) (constFormalMultilinearSeries ℂ ℂ (f z)).order ≠ 0
⊢ False
Tactic:
simp only [constFormalMultilinearSeries_apply p0, Ne, eq_self_iff_true, not_true] at b
State after:
no goals