internlm/Lean-Github huggingface dataset:
Theorem: weak_global_complex_inverse_fun_open
Proof state before:
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
Tactic:
constructor
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 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)

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 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
⊢ ∀ z ∈ s, g 0 (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
⊢ ∀ p ∈ univ ×ˢ s, mfderiv I I (f' p.1) p.2 ≠ 0
Tactic:
intro ⟨c, z⟩ ⟨_, 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
c : ℂ
z : S
left✝ : (c, z).1 ∈ univ
zs : (c, z).2 ∈ s
⊢ mfderiv I I (f' (c, z).1) (c, z).2 ≠ 0
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
c : ℂ
z : S
left✝ : (c, z).1 ∈ univ
zs : (c, z).2 ∈ s
⊢ mfderiv I I (f' (c, z).1) (c, z).2 ≠ 0
Tactic:
exact nc _ zs
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
f' : ℂ → S → T := fun x z => f z
nc' : ∀ p ∈ univ ×ˢ s, mfderiv I I (f' p.1) p.2 ≠ 0
⊢ InjOn (fun p => (p.1, f' p.1 p.2)) (univ ×ˢ s)
Tactic:
intro ⟨c0, z0⟩ ⟨_, zs0⟩ ⟨c1, z1⟩ ⟨_, zs1⟩ 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 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
c0 : ℂ
z0 : S
left✝¹ : (c0, z0).1 ∈ univ
zs0 : (c0, z0).2 ∈ s
c1 : ℂ
z1 : S
left✝ : (c1, z1).1 ∈ univ
zs1 : (c1, z1).2 ∈ s
h : (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: 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
c0 : ℂ
z0 : S
left✝¹ : (c0, z0).1 ∈ univ
zs0 : (c0, z0).2 ∈ s
c1 : ℂ
z1 : S
left✝ : (c1, z1).1 ∈ univ
zs1 : (c1, z1).2 ∈ s
h : (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 [Prod.ext_iff] at h zs0 zs1
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
c0 : ℂ
z0 : S
left✝¹ : (c0, z0).1 ∈ univ
zs0 : z0 ∈ s
c1 : ℂ
z1 : S
left✝ : (c1, z1).1 ∈ univ
zs1 : z1 ∈ s
h : c0 = c1 ∧ f' c0 z0 = f' c1 z1
⊢ (c0, z0) = (c1, z1)
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
c0 : ℂ
z0 : S
left✝¹ : (c0, z0).1 ∈ univ
zs0 : z0 ∈ s
c1 : ℂ
z1 : S
left✝ : (c1, z1).1 ∈ univ
zs1 : z1 ∈ s
h : c0 = c1 ∧ f' c0 z0 = f' c1 z1
⊢ (c0, z0) = (c1, z1)
Tactic:
rw [h.1, inj zs0 zs1]
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
c0 : ℂ
z0 : S
left✝¹ : (c0, z0).1 ∈ univ
zs0 : z0 ∈ s
c1 : ℂ
z1 : S
left✝ : (c1, z1).1 ∈ univ
zs1 : z1 ∈ s
h : c0 = c1 ∧ f' c0 z0 = f' c1 z1
⊢ f z0 = f z1
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
c0 : ℂ
z0 : S
left✝¹ : (c0, z0).1 ∈ univ
zs0 : z0 ∈ s
c1 : ℂ
z1 : S
left✝ : (c1, z1).1 ∈ univ
zs1 : z1 ∈ s
h : c0 = c1 ∧ f' c0 z0 = f' c1 z1
⊢ f z0 = f z1
Tactic:
exact h.2
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
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)
⊢ HolomorphicOn (I.prod I) I (uncurry f') (univ ×ˢ s)
Tactic:
intro ⟨c, z⟩ ⟨_, 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
inj' : InjOn (fun p => (p.1, f' p.1 p.2)) (univ ×ˢ s)
c : ℂ
z : S
left✝ : (c, z).1 ∈ univ
zs : (c, z).2 ∈ s
⊢ HolomorphicAt (I.prod I) I (uncurry f') (c, 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)
c : ℂ
z : S
left✝ : (c, z).1 ∈ univ
zs : (c, z).2 ∈ s
⊢ HolomorphicAt (I.prod I) I (uncurry f') (c, z)
Tactic:
exact (fa z zs).comp_of_eq holomorphicAt_snd rfl
Proof state after:
no goals
Theorem: weak_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 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)
Tactic:
intro z ⟨w, m⟩
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 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
z : T
w : S
m : w ∈ s ∧ f w = z
⊢ HolomorphicAt I I (g 0) z
Theorem: weak_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 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
z : T
w : S
m : w ∈ s ∧ f w = z
⊢ HolomorphicAt I I (g 0) z
Tactic:
refine (ga ⟨0, z⟩ ⟨⟨0, w⟩, ⟨mem_univ _, m.1⟩, ?_⟩).along_snd
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 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
z : T
w : S
m : w ∈ s ∧ f w = z
⊢ (fun p => (p.1, f' p.1 p.2)) (0, w) = (0, z)
Theorem: weak_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 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
z : T
w : S
m : w ∈ s ∧ f w = z
⊢ (fun p => (p.1, f' p.1 p.2)) (0, w) = (0, z)
Tactic:
simp only [Prod.ext_iff, eq_self_iff_true, true_and_iff]
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 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
z : T
w : S
m : w ∈ s ∧ f w = z
⊢ f' 0 w = z
Theorem: weak_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 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
z : T
w : S
m : w ∈ s ∧ f w = z
⊢ f' 0 w = z
Tactic:
exact m.2
Proof state after:
no goals
Theorem: weak_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 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
⊢ ∀ z ∈ s, g 0 (f z) = z
Tactic:
intro 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 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
z : S
m : z ∈ s
⊢ g 0 (f z) = z
Theorem: weak_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 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
z : S
m : z ∈ s
⊢ g 0 (f z) = z
Tactic:
exact gf ⟨0, z⟩ ⟨mem_univ _, m⟩
Proof state after:
no goals
Theorem: dualVector_le
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x y : E
⊢ Complex.abs ((dualVector x) y) ≤ ‖y‖
Tactic:
rw [← Complex.norm_eq_abs]
Proof state after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x y : E
⊢ ‖(dualVector x) y‖ ≤ ‖y‖
Theorem: dualVector_le
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x y : E
⊢ ‖(dualVector x) y‖ ≤ ‖y‖
Tactic:
calc ‖dualVector x y‖
  _ ≤ ‖dualVector x‖ * ‖y‖ := (dualVector x).le_op_norm y
  _ ≤ 1 * ‖y‖ := by bound
  _ = ‖y‖ := by simp only [one_mul]
Proof state after:
no goals
Theorem: dualVector_le
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x y : E
⊢ ‖dualVector x‖ * ‖y‖ ≤ 1 * ‖y‖
Tactic:
bound
Proof state after:
no goals
Theorem: dualVector_le
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x y : E
⊢ 1 * ‖y‖ = ‖y‖
Tactic:
simp only [one_mul]
Proof state after:
no goals
Theorem: LipschitzWith.is_const
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
g0 : LipschitzWith 0 g
⊢ ∀ (x y : ℝ), g x = g y
Tactic:
intro x y
Proof state after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
g0 : LipschitzWith 0 g
x y : ℝ
⊢ g x = g y
Theorem: LipschitzWith.is_const
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
g0 : LipschitzWith 0 g
x y : ℝ
⊢ g x = g y
Tactic:
simpa only [ENNReal.coe_zero, zero_mul, nonpos_iff_eq_zero, edist_eq_zero] using g0 x y
Proof state after:
no goals
Theorem: duals_bddAbove
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
⊢ BddAbove (range fun n => g ‖(duals n) x‖)
Tactic:
rw [bddAbove_def]
Proof state after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
⊢ ∃ x_1, ∀ y ∈ range fun n => g ‖(duals n) x‖, y ≤ x_1
Theorem: duals_bddAbove
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
⊢ ∃ x_1, ∀ y ∈ range fun n => g ‖(duals n) x‖, y ≤ x_1
Tactic:
use g ‖x‖
Proof state after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
⊢ ∀ y ∈ range fun n => g ‖(duals n) x‖, y ≤ g ‖x‖
Theorem: duals_bddAbove
Proof state before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
⊢ ∀ y ∈ range fun n => g ‖(duals n) x‖, y ≤ g ‖x‖
Tactic:
simp only [Complex.norm_eq_abs, Set.mem_range, forall_exists_index,
  forall_apply_eq_imp_iff']
Proof state after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
⊢ ∀ (y : ℝ) (x_1 : ℕ), g (Complex.abs ((duals x_1) x)) = y → y ≤ g ‖x‖
Theorem: duals_bddAbove
Proof state before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
⊢ ∀ (y : ℝ) (x_1 : ℕ), g (Complex.abs ((duals x_1) x)) = y → y ≤ g ‖x‖
Tactic:
intro _ _ h
Proof state after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
y✝ : ℝ
x✝ : ℕ
h : g (Complex.abs ((duals x✝) x)) = y✝
⊢ y✝ ≤ g ‖x‖
Theorem: duals_bddAbove
Proof state before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
y✝ : ℝ
x✝ : ℕ
h : g (Complex.abs ((duals x✝) x)) = y✝
⊢ y✝ ≤ g ‖x‖
Tactic:
rw [←h]
Proof state after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
y✝ : ℝ
x✝ : ℕ
h : g (Complex.abs ((duals x✝) x)) = y✝
⊢ g (Complex.abs ((duals x✝) x)) ≤ g ‖x‖
Theorem: duals_bddAbove
Proof state before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
y✝ : ℝ
x✝ : ℕ
h : g (Complex.abs ((duals x✝) x)) = y✝
⊢ g (Complex.abs ((duals x✝) x)) ≤ g ‖x‖
Tactic:
apply gm
Proof state after:
case h.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
y✝ : ℝ
x✝ : ℕ
h : g (Complex.abs ((duals x✝) x)) = y✝
⊢ Complex.abs ((duals x✝) x) ≤ ‖x‖
Theorem: duals_bddAbove
Proof state before:
case h.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
y✝ : ℝ
x✝ : ℕ
h : g (Complex.abs ((duals x✝) x)) = y✝
⊢ Complex.abs ((duals x✝) x) ≤ ‖x‖
Tactic:
apply dualVector_le
Proof state after:
no goals
Theorem: LipschitzWith.le
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
f : G → ℝ
k : ℝ≥0
fk : LipschitzWith k f
x y : G
⊢ f x ≤ f y + ↑k * dist x y
Tactic:
calc f x
  _ = f y + (f x - f y) := by ring_nf
  _ ≤ f y + |f x - f y| := by bound
  _ = f y + dist (f x) (f y) := by rw [Real.dist_eq]
  _ ≤ f y + k * dist x y := by linarith [fk.dist_le_mul x y]
Proof state after:
no goals