Theorem: 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.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
⊢ ∃ g, HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Tactic:
have i : ∀ p : ℂ × S, p ∈ s → ComplexInverseFun.Cinv f p.1 p.2 := by
  intro ⟨c, z⟩ m; exact
    { fa := fa _ m
      nc := nc _ 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
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
⊢ ∃ g, HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ 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
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
⊢ ∃ g, HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Tactic:
generalize hg : (fun c w ↦
  if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
⊢ ∃ g, HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ 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
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
⊢ ∃ g, HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Tactic:
have ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ q : ℂ × T in 𝓝 (p.1, f p.1 p.2),
    g q.1 q.2 = (i p m).g q.1 q.2 := by
  intro ⟨c, z⟩ m; simp only
  have n := nontrivialHolomorphicAt_of_mfderiv_ne_zero (fa _ m).along_snd (nc _ m); simp only at n
  simp only [n.nhds_eq_map_nhds_param (fa _ m), Filter.eventually_map]
  apply (i _ m).left_inv.mp; apply (so.eventually_mem m).mp
  apply eventually_of_forall; intro ⟨e, w⟩ wm gf
  simp only at gf
  simp only [left _ _ wm, gf]
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ ∃ g, HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ 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
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ ∃ g, HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Tactic:
use g
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.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2

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.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
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.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s)

case h.right
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
⊢ ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
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
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
c : ℂ
z : S
m : (c, z) ∈ s
⊢ ComplexInverseFun.Cinv f (c, z).1 (c, z).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
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
c : ℂ
z : S
m : (c, z) ∈ s
⊢ ComplexInverseFun.Cinv f (c, z).1 (c, z).2
Tactic:
exact
{ fa := fa _ m
nc := nc _ m }
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.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
⊢ ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
Tactic:
intro c z m
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
⊢ g c (f c z) = z

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
⊢ g c (f c z) = z
Tactic:
have h : ∃ x, (c, x) ∈ s ∧ f c x = f c z := ⟨z, m, rfl⟩
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
⊢ g c (f c z) = z

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
⊢ g c (f c z) = z
Tactic:
simp only [← hg, dif_pos h]
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
⊢ choose h = z

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
⊢ choose h = z
Tactic:
rcases choose_spec h with ⟨m0, w0⟩
State after:
case intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
⊢ choose h = z

State before:
case intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
⊢ choose h = z
Tactic:
have left := (i _ m).left_inv.self_of_nhds
State after:
case intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g ((c, z).1, (c, z).2).1 (f ((c, z).1, (c, z).2).1 ((c, z).1, (c, z).2).2) = ((c, z).1, (c, z).2).2
⊢ choose h = z

State before:
case intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g ((c, z).1, (c, z).2).1 (f ((c, z).1, (c, z).2).1 ((c, z).1, (c, z).2).2) = ((c, z).1, (c, z).2).2
⊢ choose h = z
Tactic:
simp only at left
State after:
case intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
⊢ choose h = z

State before:
case intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
e : (c, choose h) = (c, ⋯.g c (f c z))
⊢ choose h = z
Tactic:
rw [left] at e
State after:
case intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
e : (c, choose h) = (c, z)
⊢ choose h = z

State before:
case intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
e : (c, choose h) = (c, z)
⊢ choose h = z
Tactic:
exact (Prod.ext_iff.mp e).2
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.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
⊢ (c, choose h) = (c, ⋯.g c (f c z))
Tactic:
refine (inj.eq_iff m0 ?_).mp ?_
State after:
case refine_1
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
⊢ (c, ⋯.g c (f c z)) ∈ s

case refine_2
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
⊢ ((c, choose h).1, f (c, choose h).1 (c, choose h).2) =
    ((c, ⋯.g c (f c z)).1, f (c, ⋯.g c (f c z)).1 (c, ⋯.g c (f c z)).2)

State before:
case refine_1
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
⊢ (c, ⋯.g c (f c z)) ∈ s
Tactic:
simp only [left, m]
State after:
no goals

State before:
case refine_2
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
c : ℂ
z : S
m : (c, z) ∈ s
h : ∃ x, (c, x) ∈ s ∧ f c x = f c z
m0 : (c, choose h) ∈ s
w0 : f c (choose h) = f c z
left : ⋯.g c (f c z) = z
⊢ ((c, choose h).1, f (c, choose h).1 (c, choose h).2) =
    ((c, ⋯.g c (f c z)).1, f (c, ⋯.g c (f c z)).1 (c, ⋯.g c (f c z)).2)
Tactic:
simp only [left, w0]
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.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
⊢ ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
Tactic:
intro ⟨c, z⟩ m
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
⊢ ∀ᶠ (q : ℂ × T) in 𝓝 ((c, z).1, f (c, z).1 (c, z).2), g q.1 q.2 = ⋯.g q.1 q.2

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
⊢ ∀ᶠ (q : ℂ × T) in 𝓝 ((c, z).1, f (c, z).1 (c, z).2), g q.1 q.2 = ⋯.g q.1 q.2
Tactic:
simp only
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
⊢ ∀ᶠ (q : ℂ × T) in 𝓝 (c, f c z), g q.1 q.2 = ⋯.g q.1 q.2

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
⊢ ∀ᶠ (q : ℂ × T) in 𝓝 (c, f c z), g q.1 q.2 = ⋯.g q.1 q.2
Tactic:
have n := nontrivialHolomorphicAt_of_mfderiv_ne_zero (fa _ m).along_snd (nc _ m)
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
⊢ ∀ᶠ (q : ℂ × T) in 𝓝 (c, f c z), g q.1 q.2 = ⋯.g q.1 q.2

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
⊢ ∀ᶠ (q : ℂ × T) in 𝓝 (c, f c z), g q.1 q.2 = ⋯.g q.1 q.2
Tactic:
simp only [n.nhds_eq_map_nhds_param (fa _ m), Filter.eventually_map]
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
⊢ ∀ᶠ (a : ℂ × S) in 𝓝 (c, z), g a.1 (f a.1 a.2) = ⋯.g a.1 (f a.1 a.2)

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
⊢ ∀ᶠ (a : ℂ × S) in 𝓝 (c, z), g a.1 (f a.1 a.2) = ⋯.g a.1 (f a.1 a.2)
Tactic:
apply (i _ m).left_inv.mp
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 ((c, z).1, (c, z).2), ⋯.g x.1 (f x.1 x.2) = x.2 → g x.1 (f x.1 x.2) = ⋯.g x.1 (f x.1 x.2)

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 ((c, z).1, (c, z).2), ⋯.g x.1 (f x.1 x.2) = x.2 → g x.1 (f x.1 x.2) = ⋯.g x.1 (f x.1 x.2)
Tactic:
apply (so.eventually_mem m).mp
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), x ∈ s → ⋯.g x.1 (f x.1 x.2) = x.2 → g x.1 (f x.1 x.2) = ⋯.g x.1 (f x.1 x.2)

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), x ∈ s → ⋯.g x.1 (f x.1 x.2) = x.2 → g x.1 (f x.1 x.2) = ⋯.g x.1 (f x.1 x.2)
Tactic:
apply eventually_of_forall
State after:
case hp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
⊢ ∀ x ∈ s, ⋯.g x.1 (f x.1 x.2) = x.2 → g x.1 (f x.1 x.2) = ⋯.g x.1 (f x.1 x.2)

State before:
case hp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
⊢ ∀ x ∈ s, ⋯.g x.1 (f x.1 x.2) = x.2 → g x.1 (f x.1 x.2) = ⋯.g x.1 (f x.1 x.2)
Tactic:
intro ⟨e, w⟩ wm gf
State after:
case hp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
e : ℂ
w : S
wm : (e, w) ∈ s
gf : ⋯.g (e, w).1 (f (e, w).1 (e, w).2) = (e, w).2
⊢ g (e, w).1 (f (e, w).1 (e, w).2) = ⋯.g (e, w).1 (f (e, w).1 (e, w).2)

State before:
case hp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
e : ℂ
w : S
wm : (e, w) ∈ s
gf : ⋯.g (e, w).1 (f (e, w).1 (e, w).2) = (e, w).2
⊢ g (e, w).1 (f (e, w).1 (e, w).2) = ⋯.g (e, w).1 (f (e, w).1 (e, w).2)
Tactic:
simp only at gf
State after:
case hp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
e : ℂ
w : S
wm : (e, w) ∈ s
gf : ⋯.g e (f e w) = w
⊢ g (e, w).1 (f (e, w).1 (e, w).2) = ⋯.g (e, w).1 (f (e, w).1 (e, w).2)

State before:
case hp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
c : ℂ
z : S
m : (c, z) ∈ s
n : NontrivialHolomorphicAt (fun y => f c y) z
e : ℂ
w : S
wm : (e, w) ∈ s
gf : ⋯.g e (f e w) = w
⊢ g (e, w).1 (f (e, w).1 (e, w).2) = ⋯.g (e, w).1 (f (e, w).1 (e, w).2)
Tactic:
simp only [left _ _ wm, gf]
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.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s)
Tactic:
intro ⟨c, w⟩ wm
State after:
case h.left
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)

State before:
case h.left
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)
Tactic:
rcases(mem_image _ _ _).mp wm with ⟨⟨c', z⟩, zm, e⟩
State after:
case h.left.intro.mk.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
zm : (c', z) ∈ s
e : ((c', z).1, f (c', z).1 (c', z).2) = (c, w)
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)

State before:
case h.left.intro.mk.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
zm : (c', z) ∈ s
e : ((c', z).1, f (c', z).1 (c', z).2) = (c, w)
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)
Tactic:
simp only [Prod.ext_iff] at e
State after:
case h.left.intro.mk.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
zm : (c', z) ∈ s
e : c' = c ∧ f c' z = w
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)

State before:
case h.left.intro.mk.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
zm : (c', z) ∈ s
e : c' = c ∧ f c' z = w
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)
Tactic:
simp only [e.1] at e zm
State after:
case h.left.intro.mk.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
e : True ∧ f c z = w
zm : (c, z) ∈ s
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)

State before:
case h.left.intro.mk.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
e : True ∧ f c z = w
zm : (c, z) ∈ s
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, w)
Tactic:
simp only [← e.2]
State after:
case h.left.intro.mk.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
e : True ∧ f c z = w
zm : (c, z) ∈ s
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)

State before:
case h.left.intro.mk.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
w : T
wm : (c, w) ∈ (fun p => (p.1, f p.1 p.2)) '' s
c' : ℂ
z : S
e : True ∧ f c z = w
zm : (c, z) ∈ s
⊢ HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
Tactic:
exact (i _ zm).ga.congr (Filter.EventuallyEq.symm (ge _ zm))
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.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Tactic:
intro ⟨c, z⟩ m
State after:
case h.right
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
z : S
m : (c, z) ∈ s
⊢ g (c, z).1 (f (c, z).1 (c, z).2) = (c, z).2

State before:
case h.right
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
c : ℂ
z : S
m : (c, z) ∈ s
⊢ g (c, z).1 (f (c, z).1 (c, z).2) = (c, z).2
Tactic:
exact left _ _ m
State after:
no goals