Theorem: global_complex_inverse_fun_compact (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
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]
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

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

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

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
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
Tactic:
have tu : u ⊆ t := inter_subset_left t _
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}
tu : u ⊆ 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

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
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
⊢ ∃ 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 su : s ⊆ u := subset_inter st (subset_inter fa nc)
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}
tu : u ⊆ t
su : s ⊆ u
⊢ ∃ 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

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
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
⊢ ∃ 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 uo : IsOpen u := by
  apply ot.inter; rw [isOpen_iff_eventually]; intro ⟨c, z⟩ ⟨fa, nc⟩
  refine fa.eventually.mp ((mfderiv_ne_zero_eventually' fa nc).mp (eventually_of_forall ?_))
  intro ⟨c, z⟩ nc fa; use fa, nc
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}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
⊢ ∃ 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

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
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
⊢ ∃ 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 fa' : HolomorphicOn II I (uncurry f) u := fun _ m ↦ (inter_subset_right _ _ m).1
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}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
fa' : HolomorphicOn (I.prod I) I (uncurry f) u
⊢ ∃ 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

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
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
fa' : HolomorphicOn (I.prod I) I (uncurry f) u
⊢ ∃ 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 d0 : ∀ (p : ℂ × S), p ∈ u → mfderiv I I (f p.fst) p.snd ≠ 0 :=
  fun _ m ↦ (inter_subset_right _ _ m).2
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}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
fa' : HolomorphicOn (I.prod I) I (uncurry f) u
d0 : ∀ p ∈ u, 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

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
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
fa' : HolomorphicOn (I.prod I) I (uncurry f) u
d0 : ∀ p ∈ u, 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
Tactic:
rcases global_complex_inverse_fun_open fa' d0 (ti.mono tu) uo with ⟨g, ga, gf⟩
State after:
case intro.intro.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}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
fa' : HolomorphicOn (I.prod I) I (uncurry f) u
d0 : ∀ p ∈ u, mfderiv I I (f p.1) p.2 ≠ 0
g : ℂ → T → S
ga : HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' u)
gf : ∀ p ∈ u, g p.1 (f p.1 p.2) = p.2
⊢ ∃ 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

State before:
case intro.intro.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}
tu : u ⊆ t
su : s ⊆ u
uo : IsOpen u
fa' : HolomorphicOn (I.prod I) I (uncurry f) u
d0 : ∀ p ∈ u, mfderiv I I (f p.1) p.2 ≠ 0
g : ℂ → T → S
ga : HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' u)
gf : ∀ p ∈ u, g p.1 (f p.1 p.2) = p.2
⊢ ∃ 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:
use g, ga.mono (image_subset _ su), Filter.eventually_of_mem (uo.mem_nhdsSet.mpr su) gf
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
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, IsOpen t ∧ s ⊆ t ∧ InjOn (fun p => (p.1, f p.1 p.2)) t
Tactic:
apply inj.exists_isOpen_superset sc (fun _ m ↦ continuousAt_fst.prod (fa _ m).continuousAt)
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
⊢ ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn (fun p => (p.1, f p.1 p.2)) u

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
⊢ ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn (fun p => (p.1, f p.1 p.2)) u
Tactic:
intro ⟨c, z⟩ m
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
c : ℂ
z : S
m : (c, z) ∈ s
⊢ ∃ u ∈ 𝓝 (c, z), InjOn (fun p => (p.1, f p.1 p.2)) u

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
c : ℂ
z : S
m : (c, z) ∈ s
⊢ ∃ u ∈ 𝓝 (c, z), InjOn (fun p => (p.1, f p.1 p.2)) u
Tactic:
rcases complex_inverse_fun (fa _ m) (nc _ m) with ⟨g, _, gf, _⟩
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
c : ℂ
z : S
m : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
⊢ ∃ u ∈ 𝓝 (c, z), InjOn (fun p => (p.1, f p.1 p.2)) u

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
c : ℂ
z : S
m : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
⊢ ∃ u ∈ 𝓝 (c, z), InjOn (fun p => (p.1, f p.1 p.2)) u
Tactic:
rcases eventually_nhds_iff.mp gf with ⟨t, gf, o, m⟩
State after:
case intro.intro.intro.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
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
⊢ ∃ u ∈ 𝓝 (c, z), InjOn (fun p => (p.1, f p.1 p.2)) u

State before:
case intro.intro.intro.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
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
⊢ ∃ u ∈ 𝓝 (c, z), InjOn (fun p => (p.1, f p.1 p.2)) u
Tactic:
use t, o.mem_nhds m
State after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
⊢ InjOn (fun p => (p.1, f p.1 p.2)) t

State before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
⊢ InjOn (fun p => (p.1, f p.1 p.2)) t
Tactic:
intro ⟨c0, z0⟩ m0 ⟨c1, z1⟩ m1 e
State after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : (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:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : (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 [uncurry, Prod.ext_iff] at e ⊢
State after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : c0 = c1 ∧ f c0 z0 = f c1 z1
⊢ c0 = c1 ∧ z0 = z1

State before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : c0 = c1 ∧ f c0 z0 = f c1 z1
⊢ c0 = c1 ∧ z0 = z1
Tactic:
use e.1
State after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : c0 = c1 ∧ f c0 z0 = f c1 z1
⊢ z0 = z1

State before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : c0 = c1 ∧ f c0 z0 = f c1 z1
⊢ z0 = z1
Tactic:
have e0 := gf _ m0
State after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : c0 = c1 ∧ f c0 z0 = f c1 z1
e0 : g (c0, z0).1 (f (c0, z0).1 (c0, z0).2) = (c0, z0).2
⊢ z0 = z1

State before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : c0 = c1 ∧ f c0 z0 = f c1 z1
e0 : g (c0, z0).1 (f (c0, z0).1 (c0, z0).2) = (c0, z0).2
⊢ z0 = z1
Tactic:
have e1 := gf _ m1
State after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : c0 = c1 ∧ f c0 z0 = f c1 z1
e0 : g (c0, z0).1 (f (c0, z0).1 (c0, z0).2) = (c0, z0).2
e1 : g (c1, z1).1 (f (c1, z1).1 (c1, z1).2) = (c1, z1).2
⊢ z0 = z1

State before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : c0 = c1 ∧ f c0 z0 = f c1 z1
e0 : g (c0, z0).1 (f (c0, z0).1 (c0, z0).2) = (c0, z0).2
e1 : g (c1, z1).1 (f (c1, z1).1 (c1, z1).2) = (c1, z1).2
⊢ z0 = z1
Tactic:
simp only at e0 e1
State after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : c0 = c1 ∧ f c0 z0 = f c1 z1
e0 : g c0 (f c0 z0) = z0
e1 : g c1 (f c1 z1) = z1
⊢ z0 = z1

State before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
c : ℂ
z : S
m✝ : (c, z) ∈ s
g : ℂ → T → S
left✝ : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf✝ : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
right✝ : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
t : Set (ℂ × S)
gf : ∀ x ∈ t, g x.1 (f x.1 x.2) = x.2
o : IsOpen t
m : (c, z) ∈ t
c0 : ℂ
z0 : S
m0 : (c0, z0) ∈ t
c1 : ℂ
z1 : S
m1 : (c1, z1) ∈ t
e : c0 = c1 ∧ f c0 z0 = f c1 z1
e0 : g c0 (f c0 z0) = z0
e1 : g c1 (f c1 z1) = z1
⊢ z0 = z1
Tactic:
rw [← e0, ← e1, e.2, ← e.1]
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
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
⊢ IsOpen u
Tactic:
apply ot.inter
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
⊢ IsOpen {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
⊢ IsOpen {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
Tactic:
rw [isOpen_iff_eventually]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
⊢ ∀ x ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0},
    ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
⊢ ∀ x ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0},
    ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
Tactic:
intro ⟨c, z⟩ ⟨fa, nc⟩
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa✝ : HolomorphicOn (I.prod I) I (uncurry f) s
nc✝ : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f (c, z).1) (c, z).2 ≠ 0
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa✝ : HolomorphicOn (I.prod I) I (uncurry f) s
nc✝ : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f (c, z).1) (c, z).2 ≠ 0
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
Tactic:
refine fa.eventually.mp ((mfderiv_ne_zero_eventually' fa nc).mp (eventually_of_forall ?_))
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa✝ : HolomorphicOn (I.prod I) I (uncurry f) s
nc✝ : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f (c, z).1) (c, z).2 ≠ 0
⊢ ∀ (x : ℂ × S),
    mfderiv I I (f x.1) x.2 ≠ 0 →
      HolomorphicAt (I.prod I) I (uncurry f) x →
        x ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa✝ : HolomorphicOn (I.prod I) I (uncurry f) s
nc✝ : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f (c, z).1) (c, z).2 ≠ 0
⊢ ∀ (x : ℂ × S),
    mfderiv I I (f x.1) x.2 ≠ 0 →
      HolomorphicAt (I.prod I) I (uncurry f) x →
        x ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
Tactic:
intro ⟨c, z⟩ nc fa
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa✝¹ : HolomorphicOn (I.prod I) I (uncurry f) s
nc✝¹ : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
c✝ : ℂ
z✝ : S
fa✝ : HolomorphicAt (I.prod I) I (uncurry f) (c✝, z✝)
nc✝ : mfderiv I I (f (c✝, z✝).1) (c✝, z✝).2 ≠ 0
c : ℂ
z : S
nc : mfderiv I I (f (c, z).1) (c, z).2 ≠ 0
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
⊢ (c, z) ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝¹ : Nonempty S
inst✝ : T2Space T
s : Set (ℂ × S)
fa✝¹ : HolomorphicOn (I.prod I) I (uncurry f) s
nc✝¹ : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
sc : IsCompact s
t : Set (ℂ × S)
ot : IsOpen t
st : s ⊆ t
ti : InjOn (fun p => (p.1, f p.1 p.2)) t
u : Set (ℂ × S) := t ∩ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
tu : u ⊆ t
su : s ⊆ u
c✝ : ℂ
z✝ : S
fa✝ : HolomorphicAt (I.prod I) I (uncurry f) (c✝, z✝)
nc✝ : mfderiv I I (f (c✝, z✝).1) (c✝, z✝).2 ≠ 0
c : ℂ
z : S
nc : mfderiv I I (f (c, z).1) (c, z).2 ≠ 0
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
⊢ (c, z) ∈ {p | HolomorphicAt (I.prod I) I (uncurry f) p ∧ mfderiv I I (f p.1) p.2 ≠ 0}
Tactic:
use fa, nc
State after:
no goals