Theorem: weak_global_complex_inverse_fun_open (Ray/AnalyticManifold/GlobalInverse.lean)

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
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

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
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

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
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

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
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

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⟩
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

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
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

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
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

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⟩
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

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
State after:
no goals

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
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)

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
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)

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]
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

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
State after:
no goals

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⟩
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)

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
State after:
no goals

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⟩
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

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
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)

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]
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

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
State after:
no goals

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
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

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⟩
State after:
no goals