Theorem: Set.InjOn.mfderiv_ne_zero (Ray/Dynamics/Multiple.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
s : Set S
inj : InjOn f s
so : IsOpen s
c : S
m : c ∈ s
fa : HolomorphicAt I I f c
⊢ mfderiv I I f c ≠ 0
Tactic:
contrapose inj
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
s : Set S
so : IsOpen s
c : S
m : c ∈ s
fa : HolomorphicAt I I f c
inj : ¬mfderiv I I f c ≠ 0
⊢ ¬InjOn f s

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
s : Set S
so : IsOpen s
c : S
m : c ∈ s
fa : HolomorphicAt I I f c
inj : ¬mfderiv I I f c ≠ 0
⊢ ¬InjOn f s
Tactic:
simp only [not_not, InjOn, not_forall] at inj ⊢
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
s : Set S
so : IsOpen s
c : S
m : c ∈ s
fa : HolomorphicAt I I f c
inj : mfderiv I I f c = 0
⊢ ∃ x, ∃ (_ : x ∈ s), ∃ x_1, ∃ (_ : x_1 ∈ s) (_ : f x = f x_1), ¬x = x_1

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
s : Set S
so : IsOpen s
c : S
m : c ∈ s
fa : HolomorphicAt I I f c
inj : mfderiv I I f c = 0
⊢ ∃ x, ∃ (_ : x ∈ s), ∃ x_1, ∃ (_ : x_1 ∈ s) (_ : f x = f x_1), ¬x = x_1
Tactic:
rcases not_local_inj_of_mfderiv_zero fa inj with ⟨g, ga, gc, fg⟩
State after:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
s : Set S
so : IsOpen s
c : S
m : c ∈ s
fa : HolomorphicAt I I f c
inj : mfderiv I I f c = 0
g : S → S
ga : HolomorphicAt I I g c
gc : g c = c
fg : ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
⊢ ∃ x, ∃ (_ : x ∈ s), ∃ x_1, ∃ (_ : x_1 ∈ s) (_ : f x = f x_1), ¬x = x_1

State before:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
s : Set S
so : IsOpen s
c : S
m : c ∈ s
fa : HolomorphicAt I I f c
inj : mfderiv I I f c = 0
g : S → S
ga : HolomorphicAt I I g c
gc : g c = c
fg : ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
⊢ ∃ x, ∃ (_ : x ∈ s), ∃ x_1, ∃ (_ : x_1 ∈ s) (_ : f x = f x_1), ¬x = x_1
Tactic:
have gm : ∀ᶠ z in 𝓝 c, g z ∈ s :=
  ga.continuousAt.eventually_mem (so.mem_nhds (by simp only [gc, m]))
State after:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
s : Set S
so : IsOpen s
c : S
m : c ∈ s
fa : HolomorphicAt I I f c
inj : mfderiv I I f c = 0
g : S → S
ga : HolomorphicAt I I g c
gc : g c = c
fg : ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
gm : ∀ᶠ (z : S) in 𝓝 c, g z ∈ s
⊢ ∃ x, ∃ (_ : x ∈ s), ∃ x_1, ∃ (_ : x_1 ∈ s) (_ : f x = f x_1), ¬x = x_1

State before:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
s : Set S
so : IsOpen s
c : S
m : c ∈ s
fa : HolomorphicAt I I f c
inj : mfderiv I I f c = 0
g : S → S
ga : HolomorphicAt I I g c
gc : g c = c
fg : ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
gm : ∀ᶠ (z : S) in 𝓝 c, g z ∈ s
⊢ ∃ x, ∃ (_ : x ∈ s), ∃ x_1, ∃ (_ : x_1 ∈ s) (_ : f x = f x_1), ¬x = x_1
Tactic:
replace fg := fg.and (((so.eventually_mem m).and gm).filter_mono nhdsWithin_le_nhds)
State after:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
s : Set S
so : IsOpen s
c : S
m : c ∈ s
fa : HolomorphicAt I I f c
inj : mfderiv I I f c = 0
g : S → S
ga : HolomorphicAt I I g c
gc : g c = c
gm : ∀ᶠ (z : S) in 𝓝 c, g z ∈ s
fg : ∀ᶠ (x : S) in 𝓝[≠] c, (g x ≠ x ∧ f (g x) = f x) ∧ x ∈ s ∧ g x ∈ s
⊢ ∃ x, ∃ (_ : x ∈ s), ∃ x_1, ∃ (_ : x_1 ∈ s) (_ : f x = f x_1), ¬x = x_1

State before:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
s : Set S
so : IsOpen s
c : S
m : c ∈ s
fa : HolomorphicAt I I f c
inj : mfderiv I I f c = 0
g : S → S
ga : HolomorphicAt I I g c
gc : g c = c
gm : ∀ᶠ (z : S) in 𝓝 c, g z ∈ s
fg : ∀ᶠ (x : S) in 𝓝[≠] c, (g x ≠ x ∧ f (g x) = f x) ∧ x ∈ s ∧ g x ∈ s
⊢ ∃ x, ∃ (_ : x ∈ s), ∃ x_1, ∃ (_ : x_1 ∈ s) (_ : f x = f x_1), ¬x = x_1
Tactic:
rcases @Filter.Eventually.exists _ _ _ (AnalyticManifold.punctured_nhds_neBot I c) fg
  with ⟨z, ⟨gz, fg⟩, zs, gs⟩
State after:
case intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
s : Set S
so : IsOpen s
c : S
m : c ∈ s
fa : HolomorphicAt I I f c
inj : mfderiv I I f c = 0
g : S → S
ga : HolomorphicAt I I g c
gc : g c = c
gm : ∀ᶠ (z : S) in 𝓝 c, g z ∈ s
fg✝ : ∀ᶠ (x : S) in 𝓝[≠] c, (g x ≠ x ∧ f (g x) = f x) ∧ x ∈ s ∧ g x ∈ s
z : S
gz : g z ≠ z
fg : f (g z) = f z
zs : z ∈ s
gs : g z ∈ s
⊢ ∃ x, ∃ (_ : x ∈ s), ∃ x_1, ∃ (_ : x_1 ∈ s) (_ : f x = f x_1), ¬x = x_1

State before:
case intro.intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
s : Set S
so : IsOpen s
c : S
m : c ∈ s
fa : HolomorphicAt I I f c
inj : mfderiv I I f c = 0
g : S → S
ga : HolomorphicAt I I g c
gc : g c = c
gm : ∀ᶠ (z : S) in 𝓝 c, g z ∈ s
fg✝ : ∀ᶠ (x : S) in 𝓝[≠] c, (g x ≠ x ∧ f (g x) = f x) ∧ x ∈ s ∧ g x ∈ s
z : S
gz : g z ≠ z
fg : f (g z) = f z
zs : z ∈ s
gs : g z ∈ s
⊢ ∃ x, ∃ (_ : x ∈ s), ∃ x_1, ∃ (_ : x_1 ∈ s) (_ : f x = f x_1), ¬x = x_1
Tactic:
use g z, gs, z, zs, fg, gz
State after:
no goals

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
s : Set S
so : IsOpen s
c : S
m : c ∈ s
fa : HolomorphicAt I I f c
inj : mfderiv I I f c = 0
g : S → S
ga : HolomorphicAt I I g c
gc : g c = c
fg : ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
⊢ g c ∈ s
Tactic:
simp only [gc, m]
State after:
no goals