internlm/Lean-Github huggingface dataset:
Theorem: 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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), x ∈ s → ⋯.g x.1 (f x.1 x.2) = x.2 → g x.1 (f x.1 x.2) = ⋯.g x.1 (f x.1 x.2)
Tactic:
apply eventually_of_forall
Proof state after:
case hp
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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
⊢ ∀ x ∈ s, ⋯.g x.1 (f x.1 x.2) = x.2 → g x.1 (f x.1 x.2) = ⋯.g x.1 (f x.1 x.2)
Theorem: global_complex_inverse_fun_open
Proof state before:
case hp
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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
⊢ ∀ x ∈ s, ⋯.g x.1 (f x.1 x.2) = x.2 → g x.1 (f x.1 x.2) = ⋯.g x.1 (f x.1 x.2)
Tactic:
intro ⟨e, w⟩ wm gf
Proof state after:
case hp
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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
e : ℂ
w : S
wm : (e, w) ∈ s
gf : ⋯.g (e, w).1 (f (e, w).1 (e, w).2) = (e, w).2
⊢ g (e, w).1 (f (e, w).1 (e, w).2) = ⋯.g (e, w).1 (f (e, w).1 (e, w).2)
Theorem: global_complex_inverse_fun_open
Proof state before:
case hp
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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
e : ℂ
w : S
wm : (e, w) ∈ s
gf : ⋯.g (e, w).1 (f (e, w).1 (e, w).2) = (e, w).2
⊢ g (e, w).1 (f (e, w).1 (e, w).2) = ⋯.g (e, w).1 (f (e, w).1 (e, w).2)
Tactic:
simp only at gf
Proof state after:
case hp
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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
e : ℂ
w : S
wm : (e, w) ∈ s
gf : ⋯.g e (f e w) = w
⊢ g (e, w).1 (f (e, w).1 (e, w).2) = ⋯.g (e, w).1 (f (e, w).1 (e, w).2)
Theorem: global_complex_inverse_fun_open
Proof state before:
case hp
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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
e : ℂ
w : S
wm : (e, w) ∈ s
gf : ⋯.g e (f e w) = w
⊢ g (e, w).1 (f (e, w).1 (e, w).2) = ⋯.g (e, w).1 (f (e, w).1 (e, w).2)
Tactic:
simp only [left _ _ wm, gf]
Proof state after:
no goals
Theorem: global_complex_inverse_fun_open
Proof state before:
case h.left
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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s)
Tactic:
intro ⟨c, w⟩ wm
Proof state after:
case h.left
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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)
Theorem: global_complex_inverse_fun_open
Proof state before:
case h.left
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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)
Tactic:
rcases(mem_image _ _ _).mp wm with ⟨⟨c', z⟩, zm, e⟩
Proof state after:
case h.left.intro.mk.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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
zm : (c', z) ∈ s
e : ((c', z).1, f (c', z).1 (c', z).2) = (c, w)
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)
Theorem: global_complex_inverse_fun_open
Proof state before:
case h.left.intro.mk.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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
zm : (c', z) ∈ s
e : ((c', z).1, f (c', z).1 (c', z).2) = (c, w)
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)
Tactic:
simp only [Prod.ext_iff] at e
Proof state after:
case h.left.intro.mk.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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
zm : (c', z) ∈ s
e : c' = c ∧ f c' z = w
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)
Theorem: global_complex_inverse_fun_open
Proof state before:
case h.left.intro.mk.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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
zm : (c', z) ∈ s
e : c' = c ∧ f c' z = w
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)
Tactic:
simp only [e.1] at e zm
Proof state after:
case h.left.intro.mk.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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
e : True ∧ f c z = w
zm : (c, z) ∈ s
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)
Theorem: global_complex_inverse_fun_open
Proof state before:
case h.left.intro.mk.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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
e : True ∧ f c z = w
zm : (c, z) ∈ s
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)
Tactic:
simp only [← e.2]
Proof state after:
case h.left.intro.mk.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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
e : True ∧ f c z = w
zm : (c, z) ∈ s
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
Theorem: global_complex_inverse_fun_open
Proof state before:
case h.left.intro.mk.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.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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
e : True ∧ f c z = w
zm : (c, z) ∈ s
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
Tactic:
exact (i _ zm).ga.congr (Filter.EventuallyEq.symm (ge _ zm))
Proof state after:
no goals
Theorem: global_complex_inverse_fun_open
Proof state before:
case h.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
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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Tactic:
intro ⟨c, z⟩ m
Proof state after:
case h.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
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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
z : S
m : (c, z) ∈ s
⊢ g (c, z).1 (f (c, z).1 (c, z).2) = (c, z).2
Theorem: global_complex_inverse_fun_open
Proof state before:
case h.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
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
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
z : S
m : (c, z) ∈ s
⊢ g (c, z).1 (f (c, z).1 (c, z).2) = (c, z).2
Tactic:
exact left _ _ m
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
⊢ ∃ 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 t : ∃ t, IsOpen t ∧ s ⊆ t ∧ InjOn (fun p : ℂ × S ↦ (p.1, f p.1 p.2)) t := by
  apply inj.exists_isOpen_superset sc (fun _ m ↦ continuousAt_fst.prod (fa _ m).continuousAt)
  intro ⟨c, z⟩ m; rcases complex_inverse_fun (fa _ m) (nc _ m) with ⟨g, _, gf, _⟩
  rcases eventually_nhds_iff.mp gf with ⟨t, gf, o, m⟩
  use t, o.mem_nhds m; intro ⟨c0, z0⟩ m0 ⟨c1, z1⟩ m1 e
  simp only [uncurry, Prod.ext_iff] at e ⊢; use e.1
  have e0 := gf _ m0; have e1 := gf _ m1; simp only at e0 e1
  rw [← e0, ← e1, e.2, ← e.1]
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 : ∃ t, IsOpen t ∧ s ⊆ t ∧ InjOn (fun p => (p.1, f p.1 p.2)) 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:
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 : ∃ t, IsOpen t ∧ s ⊆ t ∧ InjOn (fun p => (p.1, f p.1 p.2)) 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:
rcases t with ⟨t, ot, st, ti⟩
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
⊢ ∃ 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
⊢ ∃ 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:
set u := t ∩ {p | HolomorphicAt II I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
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}
⊢ ∃ 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