Theorem: complex_inverse_fun' (Ray/AnalyticManifold/Inverse.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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
⊢ ∃ g, HolomorphicAt I I g (f z) ∧ (∀ᶠ (x : S) in 𝓝 z, g (f x) = x) ∧ ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
Tactic:
set f' : ℂ → S → T := fun _ z ↦ f z
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
f' : ℂ → S → T := fun x z => f z
⊢ ∃ g, HolomorphicAt I I g (f z) ∧ (∀ᶠ (x : S) in 𝓝 z, g (f x) = x) ∧ ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x

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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
f' : ℂ → S → T := fun x z => f z
⊢ ∃ g, HolomorphicAt I I g (f z) ∧ (∀ᶠ (x : S) in 𝓝 z, g (f x) = x) ∧ ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
Tactic:
have fa' : HolomorphicAt II I (uncurry f') (0, z) := fa.comp_of_eq holomorphicAt_snd rfl
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
f' : ℂ → S → T := fun x z => f z
fa' : HolomorphicAt (I.prod I) I (uncurry f') (0, z)
⊢ ∃ g, HolomorphicAt I I g (f z) ∧ (∀ᶠ (x : S) in 𝓝 z, g (f x) = x) ∧ ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x

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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
f' : ℂ → S → T := fun x z => f z
fa' : HolomorphicAt (I.prod I) I (uncurry f') (0, z)
⊢ ∃ g, HolomorphicAt I I g (f z) ∧ (∀ᶠ (x : S) in 𝓝 z, g (f x) = x) ∧ ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
Tactic:
rcases complex_inverse_fun fa' nc with ⟨g, ga, gf, fg⟩
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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
f' : ℂ → S → T := fun x z => f z
fa' : HolomorphicAt (I.prod I) I (uncurry f') (0, z)
g : ℂ → T → S
ga : HolomorphicAt (I.prod I) I (uncurry g) (0, f' 0 z)
gf : ∀ᶠ (x : ℂ × S) in 𝓝 (0, z), g x.1 (f' x.1 x.2) = x.2
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (0, f' 0 z), f' x.1 (g x.1 x.2) = x.2
⊢ ∃ g, HolomorphicAt I I g (f z) ∧ (∀ᶠ (x : S) in 𝓝 z, g (f x) = x) ∧ ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x

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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
f' : ℂ → S → T := fun x z => f z
fa' : HolomorphicAt (I.prod I) I (uncurry f') (0, z)
g : ℂ → T → S
ga : HolomorphicAt (I.prod I) I (uncurry g) (0, f' 0 z)
gf : ∀ᶠ (x : ℂ × S) in 𝓝 (0, z), g x.1 (f' x.1 x.2) = x.2
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (0, f' 0 z), f' x.1 (g x.1 x.2) = x.2
⊢ ∃ g, HolomorphicAt I I g (f z) ∧ (∀ᶠ (x : S) in 𝓝 z, g (f x) = x) ∧ ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
Tactic:
use g 0, ga.comp (holomorphicAt_const.prod holomorphicAt_id),
  (continuousAt_const.prod continuousAt_id).eventually gf,
  (continuousAt_const.prod continuousAt_id).eventually fg
State after:
no goals