internlm/Lean-Github huggingface dataset:
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
case intro.intro.intro.refine_3.intro.left.hy
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
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c) z ∈ (extChartAt I c).target
Tactic:
exact PartialEquiv.map_source _ m0
Proof state after:
no goals
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
case intro.intro.intro.refine_3.intro.right
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
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
Tactic:
simp only [← hg] at gh
Proof state after:
case intro.intro.intro.refine_3.intro.right
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
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh :
  ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z)))) =
    ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm (↑(extChartAt I c) z)))
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
case intro.intro.intro.refine_3.intro.right
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
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z)))) = ↑(extChartAt I (f c)) (f z)
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
Tactic:
rw [(PartialEquiv.injOn _).eq_iff m3 m2] at gh
Proof state after:
case intro.intro.intro.refine_3.intro.right
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
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
Theorem: not_local_inj_of_mfderiv_zero
Proof state before:
case intro.intro.intro.refine_3.intro.right
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
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
Tactic:
exact gh
Proof state after:
no goals
Theorem: Set.InjOn.mfderiv_ne_zero
Proof 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
Proof 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
Theorem: Set.InjOn.mfderiv_ne_zero
Proof 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 ⊢
Proof 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
Theorem: Set.InjOn.mfderiv_ne_zero
Proof 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⟩
Proof 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
Theorem: Set.InjOn.mfderiv_ne_zero
Proof 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]))
Proof 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
Theorem: Set.InjOn.mfderiv_ne_zero
Proof 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)
Proof 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
Theorem: Set.InjOn.mfderiv_ne_zero
Proof 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⟩
Proof 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
Theorem: Set.InjOn.mfderiv_ne_zero
Proof 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
Proof state after:
no goals
Theorem: Set.InjOn.mfderiv_ne_zero
Proof 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]
Proof state after:
no goals
Theorem: push_pop
Proof state before:
N : Finset ℕ
⊢ push (pop N) = insert 0 N
Tactic:
rw [push, pop]
Proof state after:
N : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) (Finset.image (fun n => n - 1) (N.erase 0))) = insert 0 N
Theorem: push_pop
Proof state before:
N : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) (Finset.image (fun n => n - 1) (N.erase 0))) = insert 0 N
Tactic:
apply Finset.ext
Proof state after:
case a
N : Finset ℕ
⊢ ∀ (a : ℕ), a ∈ insert 0 (Finset.image (fun n => n + 1) (Finset.image (fun n => n - 1) (N.erase 0))) ↔ a ∈ insert 0 N
Theorem: push_pop
Proof state before:
case a
N : Finset ℕ
⊢ ∀ (a : ℕ), a ∈ insert 0 (Finset.image (fun n => n + 1) (Finset.image (fun n => n - 1) (N.erase 0))) ↔ a ∈ insert 0 N
Tactic:
simp
Proof state after:
case a
N : Finset ℕ
⊢ ∀ (a : ℕ), (a = 0 ∨ ∃ a_1, (¬a_1 = 0 ∧ a_1 ∈ N) ∧ a_1 - 1 + 1 = a) ↔ a = 0 ∨ a ∈ N
Theorem: push_pop
Proof state before:
case a
N : Finset ℕ
⊢ ∀ (a : ℕ), (a = 0 ∨ ∃ a_1, (¬a_1 = 0 ∧ a_1 ∈ N) ∧ a_1 - 1 + 1 = a) ↔ a = 0 ∨ a ∈ N
Tactic:
intro n
Proof state after:
case a
N : Finset ℕ
n : ℕ
⊢ (n = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n = 0 ∨ n ∈ N
Theorem: push_pop
Proof state before:
case a
N : Finset ℕ
n : ℕ
⊢ (n = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n = 0 ∨ n ∈ N
Tactic:
by_cases n0 : n = 0
Proof state after:
case pos
N : Finset ℕ
n : ℕ
n0 : n = 0
⊢ (n = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n = 0 ∨ n ∈ N

case neg
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ (n = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n = 0 ∨ n ∈ N
Theorem: push_pop
Proof state before:
case neg
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ (n = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n = 0 ∨ n ∈ N
Tactic:
simp_rw [or_iff_right n0]
Proof state after:
case neg
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ (∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n ∈ N
Theorem: push_pop
Proof state before:
case neg
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ (∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n ∈ N
Tactic:
constructor
Proof state after:
case neg.mp
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ (∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) → n ∈ N

case neg.mpr
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ n ∈ N → ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n
Theorem: push_pop
Proof state before:
case pos
N : Finset ℕ
n : ℕ
n0 : n = 0
⊢ (n = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) ↔ n = 0 ∨ n ∈ N
Tactic:
rw [n0]
Proof state after:
case pos
N : Finset ℕ
n : ℕ
n0 : n = 0
⊢ (0 = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = 0) ↔ 0 = 0 ∨ 0 ∈ N
Theorem: push_pop
Proof state before:
case pos
N : Finset ℕ
n : ℕ
n0 : n = 0
⊢ (0 = 0 ∨ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = 0) ↔ 0 = 0 ∨ 0 ∈ N
Tactic:
simp
Proof state after:
no goals
Theorem: push_pop
Proof state before:
case neg.mp
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ (∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n) → n ∈ N
Tactic:
intro h
Proof state after:
case neg.mp
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n
⊢ n ∈ N
Theorem: push_pop
Proof state before:
case neg.mp
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n
⊢ n ∈ N
Tactic:
rcases h with ⟨x, ⟨x0, xN⟩, xn⟩
Proof state after:
case neg.mp.intro.intro.intro
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
x : ℕ
xn : x - 1 + 1 = n
x0 : ¬x = 0
xN : x ∈ N
⊢ n ∈ N
Theorem: push_pop
Proof state before:
case neg.mp.intro.intro.intro
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
x : ℕ
xn : x - 1 + 1 = n
x0 : ¬x = 0
xN : x ∈ N
⊢ n ∈ N
Tactic:
rw [Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr x0)] at xn
Proof state after:
case neg.mp.intro.intro.intro
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
x : ℕ
xn : x = n
x0 : ¬x = 0
xN : x ∈ N
⊢ n ∈ N
Theorem: push_pop
Proof state before:
case neg.mp.intro.intro.intro
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
x : ℕ
xn : x = n
x0 : ¬x = 0
xN : x ∈ N
⊢ n ∈ N
Tactic:
rwa [←xn]
Proof state after:
no goals
Theorem: push_pop
Proof state before:
case neg.mpr
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
⊢ n ∈ N → ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n
Tactic:
intro h
Proof state after:
case neg.mpr
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : n ∈ N
⊢ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n
Theorem: push_pop
Proof state before:
case neg.mpr
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : n ∈ N
⊢ ∃ a, (¬a = 0 ∧ a ∈ N) ∧ a - 1 + 1 = n
Tactic:
exists n
Proof state after:
case neg.mpr
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : n ∈ N
⊢ (¬n = 0 ∧ n ∈ N) ∧ n - 1 + 1 = n
Theorem: push_pop
Proof state before:
case neg.mpr
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : n ∈ N
⊢ (¬n = 0 ∧ n ∈ N) ∧ n - 1 + 1 = n
Tactic:
use ⟨n0,h⟩
Proof state after:
case right
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : n ∈ N
⊢ n - 1 + 1 = n
Theorem: push_pop
Proof state before:
case right
N : Finset ℕ
n : ℕ
n0 : ¬n = 0
h : n ∈ N
⊢ n - 1 + 1 = n
Tactic:
exact Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr n0)
Proof state after:
no goals
Theorem: push_le_push
Proof state before:
A B : Finset ℕ
⊢ push A ≤ push B ↔ A ≤ B
Tactic:
simp
Proof state after:
A B : Finset ℕ
⊢ push A ⊆ push B ↔ A ⊆ B
Theorem: push_le_push
Proof state before:
A B : Finset ℕ
⊢ push A ⊆ push B ↔ A ⊆ B
Tactic:
rw [push]
Proof state after:
A B : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ push B ↔ A ⊆ B
Theorem: push_le_push
Proof state before:
A B : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ push B ↔ A ⊆ B
Tactic:
rw [push]
Proof state after:
A B : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B) ↔ A ⊆ B
Theorem: push_le_push
Proof state before:
A B : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B) ↔ A ⊆ B
Tactic:
constructor
Proof state after:
case mp
A B : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B) → A ⊆ B

case mpr
A B : Finset ℕ
⊢ A ⊆ B → insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B)
Theorem: push_le_push
Proof state before:
case mp
A B : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B) → A ⊆ B
Tactic:
intro AB
Proof state after:
case mp
A B : Finset ℕ
AB : insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B)
⊢ A ⊆ B
Theorem: push_le_push
Proof state before:
case mp
A B : Finset ℕ
AB : insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B)
⊢ A ⊆ B
Tactic:
rw [Finset.subset_iff] at AB ⊢
Proof state after:
case mp
A B : Finset ℕ
AB : ∀ ⦃x : ℕ⦄, x ∈ insert 0 (Finset.image (fun n => n + 1) A) → x ∈ insert 0 (Finset.image (fun n => n + 1) B)
⊢ ∀ ⦃x : ℕ⦄, x ∈ A → x ∈ B
Theorem: push_le_push
Proof state before:
case mp
A B : Finset ℕ
AB : ∀ ⦃x : ℕ⦄, x ∈ insert 0 (Finset.image (fun n => n + 1) A) → x ∈ insert 0 (Finset.image (fun n => n + 1) B)
⊢ ∀ ⦃x : ℕ⦄, x ∈ A → x ∈ B
Tactic:
intro x xA
Proof state after:
case mp
A B : Finset ℕ
AB : ∀ ⦃x : ℕ⦄, x ∈ insert 0 (Finset.image (fun n => n + 1) A) → x ∈ insert 0 (Finset.image (fun n => n + 1) B)
x : ℕ
xA : x ∈ A
⊢ x ∈ B
Theorem: push_le_push
Proof state before:
case mp
A B : Finset ℕ
AB : ∀ ⦃x : ℕ⦄, x ∈ insert 0 (Finset.image (fun n => n + 1) A) → x ∈ insert 0 (Finset.image (fun n => n + 1) B)
x : ℕ
xA : x ∈ A
⊢ x ∈ B
Tactic:
have h : x + 1 ∈ insert 0 (Finset.image (fun n : ℕ ↦ n + 1) A) := by simpa
Proof state after:
case mp
A B : Finset ℕ
AB : ∀ ⦃x : ℕ⦄, x ∈ insert 0 (Finset.image (fun n => n + 1) A) → x ∈ insert 0 (Finset.image (fun n => n + 1) B)
x : ℕ
xA : x ∈ A
h : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) A)
⊢ x ∈ B