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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
⊢ ∀ᶠ (p : ℂ × S × S) in 𝓝 (c, z, z), f p.1 p.2.1 = f p.1 p.2.2 → p.2.1 = p.2.2
Tactic:
set g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p ↦ ((p.1, p.2.1), (p.1, p.2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ ∀ᶠ (p : ℂ × S × S) in 𝓝 (c, z, z), f p.1 p.2.1 = f p.1 p.2.2 → p.2.1 = p.2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
t : Tendsto g (𝓝 (c, z, z)) (𝓝 ((c, z), c, z))
⊢ ∀ᶠ (p : ℂ × S × S) in 𝓝 (c, z, z), f p.1 p.2.1 = f p.1 p.2.2 → p.2.1 = p.2.2
Tactic:
refine (t.eventually (fa.local_inj'' 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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
t : Tendsto g (𝓝 (c, z, z)) (𝓝 ((c, z), c, z))
⊢ ∀ (x : ℂ × S × S),
    ((g x).1.1 = (g x).2.1 → f (g x).1.1 (g x).1.2 = f (g x).2.1 (g x).2.2 → (g x).1 = (g x).2) →
      f x.1 x.2.1 = f x.1 x.2.2 → x.2.1 = x.2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
t : Tendsto g (𝓝 (c, z, z)) (𝓝 ((c, z), c, z))
⊢ ∀ (x : ℂ × S × S),
    ((g x).1.1 = (g x).2.1 → f (g x).1.1 (g x).1.2 = f (g x).2.1 (g x).2.2 → (g x).1 = (g x).2) →
      f x.1 x.2.1 = f x.1 x.2.2 → x.2.1 = x.2.2
Tactic:
intro ⟨e, x, y⟩ inj fe
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
t : Tendsto g (𝓝 (c, z, z)) (𝓝 ((c, z), c, z))
e : ℂ
x y : S
inj :
  (g (e, x, y)).1.1 = (g (e, x, y)).2.1 →
    f (g (e, x, y)).1.1 (g (e, x, y)).1.2 = f (g (e, x, y)).2.1 (g (e, x, y)).2.2 → (g (e, x, y)).1 = (g (e, x, y)).2
fe : f (e, x, y).1 (e, x, y).2.1 = f (e, x, y).1 (e, x, y).2.2
⊢ (e, x, y).2.1 = (e, x, y).2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
t : Tendsto g (𝓝 (c, z, z)) (𝓝 ((c, z), c, z))
e : ℂ
x y : S
inj :
  (g (e, x, y)).1.1 = (g (e, x, y)).2.1 →
    f (g (e, x, y)).1.1 (g (e, x, y)).1.2 = f (g (e, x, y)).2.1 (g (e, x, y)).2.2 → (g (e, x, y)).1 = (g (e, x, y)).2
fe : f (e, x, y).1 (e, x, y).2.1 = f (e, x, y).1 (e, x, y).2.2
⊢ (e, x, y).2.1 = (e, x, y).2.2
Tactic:
exact (Prod.ext_iff.mp (inj rfl fe)).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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ Tendsto g (𝓝 (c, z, z)) (𝓝 ((c, z), c, z))
Tactic:
apply Continuous.continuousAt
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ Continuous g

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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ Continuous g
Tactic:
apply Continuous.prod_mk
State after:
case h.hf
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ Continuous fun x => (x.1, x.2.1)

case h.hg
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ Continuous fun x => (x.1, x.2.2)

State before:
case h.hf
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ Continuous fun x => (x.1, x.2.1)
Tactic:
exact continuous_fst.prod_mk (continuous_fst.comp continuous_snd)
State after:
no goals

State before:
case h.hg
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ Continuous fun x => (x.1, x.2.2)
Tactic:
exact continuous_fst.prod_mk (continuous_snd.comp continuous_snd)
State after:
no goals