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
⊢ ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
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
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
c : ℂ
z : S
m : (c, z) ∈ s
⊢ g c (f c z) = z
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
c : ℂ
z : S
m : (c, z) ∈ s
⊢ g c (f c z) = z
Tactic:
have h : ∃ x, (c, x) ∈ s ∧ f c x = f c z := ⟨z, m, 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.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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
⊢ g c (f c z) = z
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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
⊢ g c (f c z) = z
Tactic:
simp only [← hg, dif_pos h]
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.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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
⊢ choose h = z
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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
⊢ choose h = z
Tactic:
rcases choose_spec h with ⟨m0, w0⟩
Proof state after:
case 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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
⊢ choose h = z
Theorem: global_complex_inverse_fun_open
Proof state before:
case 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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
⊢ choose h = z
Tactic:
have left := (i _ m).left_inv.self_of_nhds
Proof state after:
case 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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g ((c, z).1, (c, z).2).1 (f ((c, z).1, (c, z).2).1 ((c, z).1, (c, z).2).2) = ((c, z).1, (c, z).2).2
⊢ choose h = z
Theorem: global_complex_inverse_fun_open
Proof state before:
case 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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g ((c, z).1, (c, z).2).1 (f ((c, z).1, (c, z).2).1 ((c, z).1, (c, z).2).2) = ((c, z).1, (c, z).2).2
⊢ choose h = z
Tactic:
simp only at left
Proof state after:
case 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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
⊢ choose h = z
Theorem: global_complex_inverse_fun_open
Proof state before:
case 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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
e : (c, choose h) = (c, ⋯.g c (f c z))
⊢ choose h = z
Tactic:
rw [left] at e
Proof state after:
case 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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
e : (c, choose h) = (c, z)
⊢ choose h = z
Theorem: global_complex_inverse_fun_open
Proof state before:
case 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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
e : (c, choose h) = (c, z)
⊢ choose h = z
Tactic:
exact (Prod.ext_iff.mp e).2
Proof state after:
no goals
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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
⊢ (c, choose h) = (c, ⋯.g c (f c z))
Tactic:
refine (inj.eq_iff m0 ?_).mp ?_
Proof state after:
case refine_1
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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
⊢ (c, ⋯.g c (f c z)) ∈ s

case refine_2
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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
⊢ ((c, choose h).1, f (c, choose h).1 (c, choose h).2) =
    ((c, ⋯.g c (f c z)).1, f (c, ⋯.g c (f c z)).1 (c, ⋯.g c (f c z)).2)
Theorem: global_complex_inverse_fun_open
Proof state before:
case refine_1
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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
⊢ (c, ⋯.g c (f c z)) ∈ s
Tactic:
simp only [left, m]
Proof state after:
no goals
Theorem: global_complex_inverse_fun_open
Proof state before:
case refine_2
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
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
⊢ ((c, choose h).1, f (c, choose h).1 (c, choose h).2) =
    ((c, ⋯.g c (f c z)).1, f (c, ⋯.g c (f c z)).1 (c, ⋯.g c (f c z)).2)
Tactic:
simp only [left, w0]
Proof state after:
no goals
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
⊢ ∀ (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
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
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
⊢ ∀ᶠ (q : ℂ × T) in 𝓝 ((c, z).1, f (c, z).1 (c, z).2), g q.1 q.2 = ⋯.g q.1 q.2
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
⊢ ∀ᶠ (q : ℂ × T) in 𝓝 ((c, z).1, f (c, z).1 (c, z).2), g q.1 q.2 = ⋯.g q.1 q.2
Tactic:
simp only
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.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
⊢ ∀ᶠ (q : ℂ × T) in 𝓝 (c, f c z), g q.1 q.2 = ⋯.g q.1 q.2
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
⊢ ∀ᶠ (q : ℂ × T) in 𝓝 (c, f c z), g q.1 q.2 = ⋯.g q.1 q.2
Tactic:
have n := nontrivialHolomorphicAt_of_mfderiv_ne_zero (fa _ m).along_snd (nc _ 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
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
⊢ ∀ᶠ (q : ℂ × T) in 𝓝 (c, f c z), g q.1 q.2 = ⋯.g q.1 q.2
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
⊢ ∀ᶠ (q : ℂ × T) in 𝓝 (c, f c z), g q.1 q.2 = ⋯.g q.1 q.2
Tactic:
simp only [n.nhds_eq_map_nhds_param (fa _ m), Filter.eventually_map]
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.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
⊢ ∀ᶠ (a : ℂ × S) in 𝓝 (c, z), g a.1 (f a.1 a.2) = ⋯.g a.1 (f a.1 a.2)
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
⊢ ∀ᶠ (a : ℂ × S) in 𝓝 (c, z), g a.1 (f a.1 a.2) = ⋯.g a.1 (f a.1 a.2)
Tactic:
apply (i _ m).left_inv.mp
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.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).1, (c, z).2), ⋯.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:
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).1, (c, z).2), ⋯.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 (so.eventually_mem m).mp
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.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)