internlm/Lean-Github huggingface dataset:
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
⊢ z0 = z1
Tactic:
have e0 := gf _ m0
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
e0 : g (c0, z0).1 (f (c0, z0).1 (c0, z0).2) = (c0, z0).2
⊢ 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
e0 : g (c0, z0).1 (f (c0, z0).1 (c0, z0).2) = (c0, z0).2
⊢ z0 = z1
Tactic:
have e1 := gf _ m1
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
e0 : g (c0, z0).1 (f (c0, z0).1 (c0, z0).2) = (c0, z0).2
e1 : g (c1, z1).1 (f (c1, z1).1 (c1, z1).2) = (c1, z1).2
⊢ 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
e0 : g (c0, z0).1 (f (c0, z0).1 (c0, z0).2) = (c0, z0).2
e1 : g (c1, z1).1 (f (c1, z1).1 (c1, z1).2) = (c1, z1).2
⊢ z0 = z1
Tactic:
simp only at e0 e1
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
e0 : g c0 (f c0 z0) = z0
e1 : g c1 (f c1 z1) = z1
⊢ 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
e0 : g c0 (f c0 z0) = z0
e1 : g c1 (f c1 z1) = z1
⊢ z0 = z1
Tactic:
rw [← e0, ← e1, e.2, ← e.1]
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 : 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
⊢ IsOpen u
Tactic:
apply ot.inter
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
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
⊢ IsOpen {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
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 : 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
⊢ IsOpen {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
Tactic:
rw [isOpen_iff_eventually]
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
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
⊢ ∀ x ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0},
    ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
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 : 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
⊢ ∀ x ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0},
    ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
Tactic:
intro ⟨c, z⟩ ⟨fa, nc⟩
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
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f (c, z).1) (c, z).2 ≠ 0
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
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 : 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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f (c, z).1) (c, z).2 ≠ 0
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
Tactic:
refine fa.eventually.mp ((mfderiv_ne_zero_eventually' fa nc).mp (eventually_of_forall ?_))
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
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f (c, z).1) (c, z).2 ≠ 0
⊢ ∀ (x : ℂ × S),
    mfderiv I I (f x.1) x.2 ≠ 0 →
      HolomorphicAt (I.prod I) I (uncurry f) x →
        x ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
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 : 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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f (c, z).1) (c, z).2 ≠ 0
⊢ ∀ (x : ℂ × S),
    mfderiv I I (f x.1) x.2 ≠ 0 →
      HolomorphicAt (I.prod I) I (uncurry f) x →
        x ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
Tactic:
intro ⟨c, z⟩ nc fa
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
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
c✝ : ℂ
z✝ : S
fa✝ : HolomorphicAt (I.prod I) I (uncurry f) (c✝, z✝)
nc✝ : mfderiv I I (f (c✝, z✝).1) (c✝, z✝).2 ≠ 0
c : ℂ
z : S
nc : mfderiv I I (f (c, z).1) (c, z).2 ≠ 0
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
⊢ (c, z) ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
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 : 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
c✝ : ℂ
z✝ : S
fa✝ : HolomorphicAt (I.prod I) I (uncurry f) (c✝, z✝)
nc✝ : mfderiv I I (f (c✝, z✝).1) (c✝, z✝).2 ≠ 0
c : ℂ
z : S
nc : mfderiv I I (f (c, z).1) (c, z).2 ≠ 0
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
⊢ (c, z) ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
Tactic:
use fa, nc
Proof state after:
no goals
Theorem: weak_global_complex_inverse_fun_open
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
s : Set S
fa : HolomorphicOn I I f s
nc : ∀ z ∈ s, mfderiv I I f z ≠ 0
inj : InjOn f s
so : IsOpen s
⊢ ∃ g, HolomorphicOn I I g (f '' s) ∧ ∀ z ∈ s, g (f z) = z
Tactic:
set f' := fun (_ : ℂ) (z : S) ↦ f z
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
s : Set S
fa : HolomorphicOn I I f s
nc : ∀ z ∈ s, mfderiv I I f z ≠ 0
inj : InjOn f s
so : IsOpen s
f' : ℂ → S → T := fun x z => f z
⊢ ∃ g, HolomorphicOn I I g (f '' s) ∧ ∀ z ∈ s, g (f z) = z
Theorem: weak_global_complex_inverse_fun_open
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
s : Set S
fa : HolomorphicOn I I f s
nc : ∀ z ∈ s, mfderiv I I f z ≠ 0
inj : InjOn f s
so : IsOpen s
f' : ℂ → S → T := fun x z => f z
⊢ ∃ g, HolomorphicOn I I g (f '' s) ∧ ∀ z ∈ s, g (f z) = z
Tactic:
have nc' : ∀ p : ℂ × S, p ∈ (univ : Set ℂ) ×ˢ s → mfderiv I I (f' p.1) p.2 ≠ 0 := by
  intro ⟨c, z⟩ ⟨_, zs⟩; exact nc _ zs
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
s : Set S
fa : HolomorphicOn I I f s
nc : ∀ z ∈ s, mfderiv I I f z ≠ 0
inj : InjOn f s
so : IsOpen s
f' : ℂ → S → T := fun x z => f z
nc' : ∀ p ∈ univ ×ˢ s, mfderiv I I (f' p.1) p.2 ≠ 0
⊢ ∃ g, HolomorphicOn I I g (f '' s) ∧ ∀ z ∈ s, g (f z) = z
Theorem: weak_global_complex_inverse_fun_open
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
s : Set S
fa : HolomorphicOn I I f s
nc : ∀ z ∈ s, mfderiv I I f z ≠ 0
inj : InjOn f s
so : IsOpen s
f' : ℂ → S → T := fun x z => f z
nc' : ∀ p ∈ univ ×ˢ s, mfderiv I I (f' p.1) p.2 ≠ 0
⊢ ∃ g, HolomorphicOn I I g (f '' s) ∧ ∀ z ∈ s, g (f z) = z
Tactic:
have inj' : InjOn (fun p : ℂ × S ↦ (p.1, f' p.1 p.2)) (univ ×ˢ s) := by
  intro ⟨c0, z0⟩ ⟨_, zs0⟩ ⟨c1, z1⟩ ⟨_, zs1⟩ h; simp only [Prod.ext_iff] at h zs0 zs1
  rw [h.1, inj zs0 zs1]; exact h.2
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
s : Set S
fa : HolomorphicOn I I f s
nc : ∀ z ∈ s, mfderiv I I f z ≠ 0
inj : InjOn f s
so : IsOpen s
f' : ℂ → S → T := fun x z => f z
nc' : ∀ p ∈ univ ×ˢ s, mfderiv I I (f' p.1) p.2 ≠ 0
inj' : InjOn (fun p => (p.1, f' p.1 p.2)) (univ ×ˢ s)
⊢ ∃ g, HolomorphicOn I I g (f '' s) ∧ ∀ z ∈ s, g (f z) = z
Theorem: weak_global_complex_inverse_fun_open
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
s : Set S
fa : HolomorphicOn I I f s
nc : ∀ z ∈ s, mfderiv I I f z ≠ 0
inj : InjOn f s
so : IsOpen s
f' : ℂ → S → T := fun x z => f z
nc' : ∀ p ∈ univ ×ˢ s, mfderiv I I (f' p.1) p.2 ≠ 0
inj' : InjOn (fun p => (p.1, f' p.1 p.2)) (univ ×ˢ s)
⊢ ∃ g, HolomorphicOn I I g (f '' s) ∧ ∀ z ∈ s, g (f z) = z
Tactic:
have fa' : HolomorphicOn II I (uncurry f') (univ ×ˢ s) := by
  intro ⟨c, z⟩ ⟨_, zs⟩; exact (fa z zs).comp_of_eq holomorphicAt_snd rfl
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
s : Set S
fa : HolomorphicOn I I f s
nc : ∀ z ∈ s, mfderiv I I f z ≠ 0
inj : InjOn f s
so : IsOpen s
f' : ℂ → S → T := fun x z => f z
nc' : ∀ p ∈ univ ×ˢ s, mfderiv I I (f' p.1) p.2 ≠ 0
inj' : InjOn (fun p => (p.1, f' p.1 p.2)) (univ ×ˢ s)
fa' : HolomorphicOn (I.prod I) I (uncurry f') (univ ×ˢ s)
⊢ ∃ g, HolomorphicOn I I g (f '' s) ∧ ∀ z ∈ s, g (f z) = z
Theorem: weak_global_complex_inverse_fun_open
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
s : Set S
fa : HolomorphicOn I I f s
nc : ∀ z ∈ s, mfderiv I I f z ≠ 0
inj : InjOn f s
so : IsOpen s
f' : ℂ → S → T := fun x z => f z
nc' : ∀ p ∈ univ ×ˢ s, mfderiv I I (f' p.1) p.2 ≠ 0
inj' : InjOn (fun p => (p.1, f' p.1 p.2)) (univ ×ˢ s)
fa' : HolomorphicOn (I.prod I) I (uncurry f') (univ ×ˢ s)
⊢ ∃ g, HolomorphicOn I I g (f '' s) ∧ ∀ z ∈ s, g (f z) = z
Tactic:
rcases global_complex_inverse_fun_open fa' nc' inj' (isOpen_univ.prod so) with ⟨g, ga, gf⟩
Proof state after:
case 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
s : Set S
fa : HolomorphicOn I I f s
nc : ∀ z ∈ s, mfderiv I I f z ≠ 0
inj : InjOn f s
so : IsOpen s
f' : ℂ → S → T := fun x z => f z
nc' : ∀ p ∈ univ ×ˢ s, mfderiv I I (f' p.1) p.2 ≠ 0
inj' : InjOn (fun p => (p.1, f' p.1 p.2)) (univ ×ˢ s)
fa' : HolomorphicOn (I.prod I) I (uncurry f') (univ ×ˢ s)
g : ℂ → T → S
ga : HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f' p.1 p.2)) '' univ ×ˢ s)
gf : ∀ p ∈ univ ×ˢ s, g p.1 (f' p.1 p.2) = p.2
⊢ ∃ g, HolomorphicOn I I g (f '' s) ∧ ∀ z ∈ s, g (f z) = z
Theorem: weak_global_complex_inverse_fun_open
Proof state before:
case 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
s : Set S
fa : HolomorphicOn I I f s
nc : ∀ z ∈ s, mfderiv I I f z ≠ 0
inj : InjOn f s
so : IsOpen s
f' : ℂ → S → T := fun x z => f z
nc' : ∀ p ∈ univ ×ˢ s, mfderiv I I (f' p.1) p.2 ≠ 0
inj' : InjOn (fun p => (p.1, f' p.1 p.2)) (univ ×ˢ s)
fa' : HolomorphicOn (I.prod I) I (uncurry f') (univ ×ˢ s)
g : ℂ → T → S
ga : HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f' p.1 p.2)) '' univ ×ˢ s)
gf : ∀ p ∈ univ ×ˢ s, g p.1 (f' p.1 p.2) = p.2
⊢ ∃ g, HolomorphicOn I I g (f '' s) ∧ ∀ z ∈ s, g (f z) = z
Tactic:
use g 0
Proof state after:
case h
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
s : Set S
fa : HolomorphicOn I I f s
nc : ∀ z ∈ s, mfderiv I I f z ≠ 0
inj : InjOn f s
so : IsOpen s
f' : ℂ → S → T := fun x z => f z
nc' : ∀ p ∈ univ ×ˢ s, mfderiv I I (f' p.1) p.2 ≠ 0
inj' : InjOn (fun p => (p.1, f' p.1 p.2)) (univ ×ˢ s)
fa' : HolomorphicOn (I.prod I) I (uncurry f') (univ ×ˢ s)
g : ℂ → T → S
ga : HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f' p.1 p.2)) '' univ ×ˢ s)
gf : ∀ p ∈ univ ×ˢ s, g p.1 (f' p.1 p.2) = p.2
⊢ HolomorphicOn I I (g 0) (f '' s) ∧ ∀ z ∈ s, g 0 (f z) = z