Theorem: mfderiv_ne_zero_eventually (Ray/AnalyticManifold/OneDimension.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0
Tactic:
set c : ℂ := 0
State after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0
Tactic:
set g : ℂ → S → T := fun _ z ↦ f z
State after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0
Tactic:
have ga : HolomorphicAt II I (uncurry g) (c, z) := by
  have e : uncurry g = f ∘ fun p ↦ p.2 := rfl; rw [e]
  apply HolomorphicAt.comp_of_eq fa holomorphicAt_snd; simp only
State after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
ga : HolomorphicAt (I.prod I) I (uncurry g) (c, z)
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
ga : HolomorphicAt (I.prod I) I (uncurry g) (c, z)
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0
Tactic:
have pc : Tendsto (fun z ↦ (c, z)) (𝓝 z) (𝓝 (c, z)) := continuousAt_const.prod continuousAt_id
State after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
ga : HolomorphicAt (I.prod I) I (uncurry g) (c, z)
pc : Tendsto (fun z => (c, z)) (𝓝 z) (𝓝 (c, z))
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
ga : HolomorphicAt (I.prod I) I (uncurry g) (c, z)
pc : Tendsto (fun z => (c, z)) (𝓝 z) (𝓝 (c, z))
⊢ ∀ᶠ (w : S) in 𝓝 z, mfderiv I I f w ≠ 0
Tactic:
exact pc.eventually (mfderiv_ne_zero_eventually' ga f0)
State after:
no goals

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, z)
Tactic:
have e : uncurry g = f ∘ fun p ↦ p.2 := rfl
State after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
e : uncurry g = f ∘ fun p => p.2
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, z)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
e : uncurry g = f ∘ fun p => p.2
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, z)
Tactic:
rw [e]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
e : uncurry g = f ∘ fun p => p.2
⊢ HolomorphicAt (I.prod I) I (f ∘ fun p => p.2) (c, z)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
e : uncurry g = f ∘ fun p => p.2
⊢ HolomorphicAt (I.prod I) I (f ∘ fun p => p.2) (c, z)
Tactic:
apply HolomorphicAt.comp_of_eq fa holomorphicAt_snd
State after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
e : uncurry g = f ∘ fun p => p.2
⊢ (c, z).2 = z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → T
z : S
fa : HolomorphicAt I I f z
f0 : mfderiv I I f z ≠ 0
c : ℂ := 0
g : ℂ → S → T := fun x z => f z
e : uncurry g = f ∘ fun p => p.2
⊢ (c, z).2 = z
Tactic:
simp only
State after:
no goals