Theorem: Super.f_nontrivial (Ray/Dynamics/BottcherNearM.lean)

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ NontrivialHolomorphicAt (f c) a
Tactic:
refine ⟨(s.fa _).along_snd, ?_⟩
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ ∃ᶠ (w : S) in 𝓝 a, f c w ≠ f c a

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ ∃ᶠ (w : S) in 𝓝 a, f c w ≠ f c a
Tactic:
simp only [s.f0]
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ ∃ᶠ (w : S) in 𝓝 a, f c w ≠ a

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
⊢ ∃ᶠ (w : S) in 𝓝 a, f c w ≠ a
Tactic:
contrapose n
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ¬∃ᶠ (w : S) in 𝓝 a, f c w ≠ a
⊢ ¬∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ¬∃ᶠ (w : S) in 𝓝 a, f c w ≠ a
⊢ ¬∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
Tactic:
simp only [Filter.not_frequently, not_not, Super.fl, fl, Function.comp, sub_eq_zero] at n ⊢
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, _root_.fl f a c x = 0

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, _root_.fl f a c x = 0
Tactic:
have gc : ContinuousAt (fun x ↦ (extChartAt I a).symm (x + extChartAt I a a)) 0 := by
  refine (continuousAt_extChartAt_symm I a).comp_of_eq ?_ (by simp only [zero_add])
  exact continuousAt_id.add continuousAt_const
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : ContinuousAt (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, _root_.fl f a c x = 0

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : ContinuousAt (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, _root_.fl f a c x = 0
Tactic:
simp only [ContinuousAt, zero_add, PartialEquiv.left_inv _ (mem_extChartAt_source _ _)] at gc
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : Tendsto (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) (𝓝 0) (𝓝 a)
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, _root_.fl f a c x = 0

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : Tendsto (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) (𝓝 0) (𝓝 a)
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, _root_.fl f a c x = 0
Tactic:
refine (gc.eventually n).mp (eventually_of_forall ?_)
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : Tendsto (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) (𝓝 0) (𝓝 a)
⊢ ∀ (x : ℂ), f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = a → _root_.fl f a c x = 0

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : Tendsto (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) (𝓝 0) (𝓝 a)
⊢ ∀ (x : ℂ), f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = a → _root_.fl f a c x = 0
Tactic:
intro x h
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : Tendsto (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) (𝓝 0) (𝓝 a)
x : ℂ
h : f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = a
⊢ _root_.fl f a c x = 0

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
gc : Tendsto (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) (𝓝 0) (𝓝 a)
x : ℂ
h : f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) = a
⊢ _root_.fl f a c x = 0
Tactic:
simp only [_root_.fl, Function.comp, h, sub_self]
State after:
no goals

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
Tactic:
have e := (nontrivialHolomorphicAt_of_order (s.fla c).along_snd ?_).nonconst
State after:
case refine_2
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
e : ∃ᶠ (w : ℂ) in 𝓝 (c, 0).2, uncurry s.fl ((c, 0).1, w) ≠ uncurry s.fl ((c, 0).1, (c, 0).2)
⊢ ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0

case refine_1
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ orderAt (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2 ≠ 0

State before:
case refine_2
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
e : ∃ᶠ (w : ℂ) in 𝓝 (c, 0).2, uncurry s.fl ((c, 0).1, w) ≠ uncurry s.fl ((c, 0).1, (c, 0).2)
⊢ ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
Tactic:
simp only [s.fl0, uncurry] at e
State after:
case refine_2
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
e : ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
⊢ ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0

State before:
case refine_2
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
e : ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
⊢ ∃ᶠ (w : ℂ) in 𝓝 0, s.fl c w ≠ 0
Tactic:
exact e
State after:
no goals

State before:
case refine_1
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ orderAt (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2 ≠ 0
Tactic:
simp only [Super.fl, s.fd, uncurry]
State after:
case refine_1
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ d ≠ 0

State before:
case refine_1
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ d ≠ 0
Tactic:
exact s.d0
State after:
no goals

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
⊢ ContinuousAt (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) 0
Tactic:
refine (continuousAt_extChartAt_symm I a).comp_of_eq ?_ (by simp only [zero_add])
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
⊢ ContinuousAt (fun x => x + ↑(extChartAt I a) a) 0

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
⊢ ContinuousAt (fun x => x + ↑(extChartAt I a) a) 0
Tactic:
exact continuousAt_id.add continuousAt_const
State after:
no goals

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
c : ℂ
n : ∀ᶠ (x : S) in 𝓝 a, f c x = a
⊢ 0 + ↑(extChartAt I a) a = ↑(extChartAt I a) a
Tactic:
simp only [zero_add]
State after:
no goals