Theorem: HolomorphicAt.local_inj (Ray/AnalyticManifold/LocalInj.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
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = p.2
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
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = 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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = p.2
Tactic:
have n : NontrivialHolomorphicAt g (f z) := by
  rw [← gf.self_of_nhds] at fa
  refine (NontrivialHolomorphicAt.anti ?_ fa ga).2
  exact (nontrivialHolomorphicAt_id _).congr (Filter.EventuallyEq.symm 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
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = 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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = p.2
Tactic:
have o := n.nhds_eq_map_nhds
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
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 (g (f z)) = Filter.map g (𝓝 (f z))
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = 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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 (g (f z)) = Filter.map g (𝓝 (f z))
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = p.2
Tactic:
rw [gf.self_of_nhds] at o
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
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = 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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = p.2
Tactic:
simp only [nhds_prod_eq, o, Filter.prod_map_map_eq, Filter.eventually_map]
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
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
⊢ ∀ᶠ (a : T × T) in 𝓝 (f z) ×ˢ 𝓝 (f z), f (g a.1) = f (g a.2) → g a.1 = g a.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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
⊢ ∀ᶠ (a : T × T) in 𝓝 (f z) ×ˢ 𝓝 (f z), f (g a.1) = f (g a.2) → g a.1 = g a.2
Tactic:
refine (fg.prod_mk fg).mp (eventually_of_forall ?_)
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
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
⊢ ∀ (x : T × T), f (g x.1) = x.1 ∧ f (g x.2) = x.2 → f (g x.1) = f (g x.2) → g x.1 = g x.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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
⊢ ∀ (x : T × T), f (g x.1) = x.1 ∧ f (g x.2) = x.2 → f (g x.1) = f (g x.2) → g x.1 = g x.2
Tactic:
intro ⟨x, y⟩ ⟨ex, ey⟩ h
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
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
x y : T
ex : f (g (x, y).1) = (x, y).1
ey : f (g (x, y).2) = (x, y).2
h : f (g (x, y).1) = f (g (x, y).2)
⊢ g (x, y).1 = g (x, y).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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
x y : T
ex : f (g (x, y).1) = (x, y).1
ey : f (g (x, y).2) = (x, y).2
h : f (g (x, y).1) = f (g (x, y).2)
⊢ g (x, y).1 = g (x, y).2
Tactic:
simp only at ex ey
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
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
x y : T
ex : f (g x) = x
ey : f (g y) = y
h : f (g (x, y).1) = f (g (x, y).2)
⊢ g (x, y).1 = g (x, y).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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
x y : T
ex : f (g x) = x
ey : f (g y) = y
h : f (g (x, y).1) = f (g (x, y).2)
⊢ g (x, y).1 = g (x, y).2
Tactic:
simp only [ex, ey] at h
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
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
x y : T
ex : f (g x) = x
ey : f (g y) = y
h : x = y
⊢ g (x, y).1 = g (x, y).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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
x y : T
ex : f (g x) = x
ey : f (g y) = y
h : x = y
⊢ g (x, y).1 = g (x, y).2
Tactic:
simp only [h]
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
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
⊢ NontrivialHolomorphicAt g (f z)
Tactic:
rw [← gf.self_of_nhds] at 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
z : S
nc : mfderiv I I f z ≠ 0
g : T → S
fa : HolomorphicAt I I f (g (f z))
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
⊢ NontrivialHolomorphicAt g (f 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
z : S
nc : mfderiv I I f z ≠ 0
g : T → S
fa : HolomorphicAt I I f (g (f z))
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
⊢ NontrivialHolomorphicAt g (f z)
Tactic:
refine (NontrivialHolomorphicAt.anti ?_ fa ga).2
State after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
nc : mfderiv I I f z ≠ 0
g : T → S
fa : HolomorphicAt I I f (g (f z))
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
⊢ NontrivialHolomorphicAt (fun z => f (g z)) (f 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
z : S
nc : mfderiv I I f z ≠ 0
g : T → S
fa : HolomorphicAt I I f (g (f z))
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
⊢ NontrivialHolomorphicAt (fun z => f (g z)) (f z)
Tactic:
exact (nontrivialHolomorphicAt_id _).congr (Filter.EventuallyEq.symm fg)
State after:
no goals