internlm/Lean-Github huggingface dataset:
Theorem: global_complex_inverse_fun_compact
Proof state before:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
⊢ ∃ g,
    HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧
      ∀ᶠ (p : ℂ × S) in 𝓝ˢ s, g p.1 (f p.1 p.2) = p.2
Tactic:
have tu : u ⊆ t := inter_subset_left t _
Proof state after:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
⊢ ∃ g,
    HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧
      ∀ᶠ (p : ℂ × S) in 𝓝ˢ s, g p.1 (f p.1 p.2) = p.2
Theorem: global_complex_inverse_fun_compact
Proof state before:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
⊢ ∃ g,
    HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧
      ∀ᶠ (p : ℂ × S) in 𝓝ˢ s, g p.1 (f p.1 p.2) = p.2
Tactic:
have su : s ⊆ u := subset_inter st (subset_inter fa nc)
Proof state after:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
⊢ ∃ g,
    HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧
      ∀ᶠ (p : ℂ × S) in 𝓝ˢ s, g p.1 (f p.1 p.2) = p.2
Theorem: global_complex_inverse_fun_compact
Proof state before:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
⊢ ∃ g,
    HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧
      ∀ᶠ (p : ℂ × S) in 𝓝ˢ s, g p.1 (f p.1 p.2) = p.2
Tactic:
have uo : IsOpen u := by
  apply ot.inter; rw [isOpen_iff_eventually]; intro ⟨c, z⟩ ⟨fa, nc⟩
  refine fa.eventually.mp ((mfderiv_ne_zero_eventually' fa nc).mp (eventually_of_forall ?_))
  intro ⟨c, z⟩ nc fa; use fa, nc
Proof state after:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
⊢ ∃ g,
    HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧
      ∀ᶠ (p : ℂ × S) in 𝓝ˢ s, g p.1 (f p.1 p.2) = p.2
Theorem: global_complex_inverse_fun_compact
Proof state before:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
⊢ ∃ g,
    HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧
      ∀ᶠ (p : ℂ × S) in 𝓝ˢ s, g p.1 (f p.1 p.2) = p.2
Tactic:
have fa' : HolomorphicOn II I (uncurry f) u := fun _ m ↦ (inter_subset_right _ _ m).1
Proof state after:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
fa' : HolomorphicOn (I.prod I) I (uncurry f) u
⊢ ∃ g,
    HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧
      ∀ᶠ (p : ℂ × S) in 𝓝ˢ s, g p.1 (f p.1 p.2) = p.2
Theorem: global_complex_inverse_fun_compact
Proof state before:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
fa' : HolomorphicOn (I.prod I) I (uncurry f) u
⊢ ∃ g,
    HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧
      ∀ᶠ (p : ℂ × S) in 𝓝ˢ s, g p.1 (f p.1 p.2) = p.2
Tactic:
have d0 : ∀ (p : ℂ × S), p ∈ u → mfderiv I I (f p.fst) p.snd ≠ 0 :=
  fun _ m ↦ (inter_subset_right _ _ m).2
Proof state after:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
fa' : HolomorphicOn (I.prod I) I (uncurry f) u
d0 : ∀ p ∈ u, mfderiv I I (f p.1) p.2 ≠ 0
⊢ ∃ g,
    HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧
      ∀ᶠ (p : ℂ × S) in 𝓝ˢ s, g p.1 (f p.1 p.2) = p.2
Theorem: global_complex_inverse_fun_compact
Proof state before:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
fa' : HolomorphicOn (I.prod I) I (uncurry f) u
d0 : ∀ p ∈ u, mfderiv I I (f p.1) p.2 ≠ 0
⊢ ∃ g,
    HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧
      ∀ᶠ (p : ℂ × S) in 𝓝ˢ s, g p.1 (f p.1 p.2) = p.2
Tactic:
rcases global_complex_inverse_fun_open fa' d0 (ti.mono tu) uo with ⟨g, ga, gf⟩
Proof state after:
case intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
fa' : HolomorphicOn (I.prod I) I (uncurry f) u
d0 : ∀ p ∈ u, mfderiv I I (f p.1) p.2 ≠ 0
g : ℂ → T → S
ga : HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' u)
gf : ∀ p ∈ u, g p.1 (f p.1 p.2) = p.2
⊢ ∃ g,
    HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧
      ∀ᶠ (p : ℂ × S) in 𝓝ˢ s, g p.1 (f p.1 p.2) = p.2
Theorem: global_complex_inverse_fun_compact
Proof state before:
case intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
fa' : HolomorphicOn (I.prod I) I (uncurry f) u
d0 : ∀ p ∈ u, mfderiv I I (f p.1) p.2 ≠ 0
g : ℂ → T → S
ga : HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' u)
gf : ∀ p ∈ u, g p.1 (f p.1 p.2) = p.2
⊢ ∃ g,
    HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧
      ∀ᶠ (p : ℂ × S) in 𝓝ˢ s, g p.1 (f p.1 p.2) = p.2
Tactic:
use g, ga.mono (image_subset _ su), Filter.eventually_of_mem (uo.mem_nhdsSet.mpr su) gf
Proof state after:
no goals
Theorem: global_complex_inverse_fun_compact
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
⊢ ∃ t, IsOpen t ∧ s ⊆ t ∧ InjOn (fun p => (p.1, f p.1 p.2)) t
Tactic:
apply inj.exists_isOpen_superset sc (fun _ m ↦ continuousAt_fst.prod (fa _ m).continuousAt)
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
⊢ ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn (fun p => (p.1, f p.1 p.2)) u
Theorem: global_complex_inverse_fun_compact
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
⊢ ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn (fun p => (p.1, f p.1 p.2)) u
Tactic:
intro ⟨c, z⟩ m
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m : (c, z) ∈ s
⊢ ∃ u ∈ 𝓝 (c, z), InjOn (fun p => (p.1, f p.1 p.2)) u
Theorem: global_complex_inverse_fun_compact
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m : (c, z) ∈ s
⊢ ∃ u ∈ 𝓝 (c, z), InjOn (fun p => (p.1, f p.1 p.2)) u
Tactic:
rcases complex_inverse_fun (fa _ m) (nc _ m) with ⟨g, _, gf, _⟩
Proof state after:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
⊢ ∃ u ∈ 𝓝 (c, z), InjOn (fun p => (p.1, f p.1 p.2)) u
Theorem: global_complex_inverse_fun_compact
Proof state before:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
⊢ ∃ u ∈ 𝓝 (c, z), InjOn (fun p => (p.1, f p.1 p.2)) u
Tactic:
rcases eventually_nhds_iff.mp gf with ⟨t, gf, o, m⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
⊢ ∃ u ∈ 𝓝 (c, z), InjOn (fun p => (p.1, f p.1 p.2)) u
Theorem: global_complex_inverse_fun_compact
Proof state before:
case intro.intro.intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
⊢ ∃ u ∈ 𝓝 (c, z), InjOn (fun p => (p.1, f p.1 p.2)) u
Tactic:
use t, o.mem_nhds m
Proof state after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
⊢ InjOn (fun p => (p.1, f p.1 p.2)) t
Theorem: global_complex_inverse_fun_compact
Proof state before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
⊢ InjOn (fun p => (p.1, f p.1 p.2)) t
Tactic:
intro ⟨c0, z0⟩ m0 ⟨c1, z1⟩ m1 e
Proof state after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : (fun p => (p.1, f p.1 p.2)) (c0, z0) = (fun p => (p.1, f p.1 p.2)) (c1, z1)
⊢ (c0, z0) = (c1, z1)
Theorem: global_complex_inverse_fun_compact
Proof state before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : (fun p => (p.1, f p.1 p.2)) (c0, z0) = (fun p => (p.1, f p.1 p.2)) (c1, z1)
⊢ (c0, z0) = (c1, z1)
Tactic:
simp only [uncurry, Prod.ext_iff] at e ⊢
Proof state after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : c0 = c1 ∧ f c0 z0 = f c1 z1
⊢ c0 = c1 ∧ z0 = z1
Theorem: global_complex_inverse_fun_compact
Proof state before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : c0 = c1 ∧ f c0 z0 = f c1 z1
⊢ c0 = c1 ∧ z0 = z1
Tactic:
use e.1
Proof state after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : c0 = c1 ∧ f c0 z0 = f c1 z1
⊢ z0 = z1