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), c, z), p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
⊢ ∀ᶠ (p : (ℂ × S) × ℂ × S) in 𝓝 ((c, z), c, z), p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
⊢ ∀ᶠ (p : (ℂ × S) × ℂ × S) in 𝓝 ((c, z), c, z), p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.2 → p.1 = p.2
Tactic:
have n : NontrivialHolomorphicAt (g c) (f c z) := by
  have e : (c, z) = (c, g c (f c z)) := by rw [gf.self_of_nhds]
  rw [e] at fa
  refine (NontrivialHolomorphicAt.anti ?_ fa.along_snd ga.along_snd).2
  refine (nontrivialHolomorphicAt_id _).congr ?_
  refine ((continuousAt_const.prod continuousAt_id).eventually fg).mp (eventually_of_forall ?_)
  exact fun _ e ↦ e.symm
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
⊢ ∀ᶠ (p : (ℂ × S) × ℂ × S) in 𝓝 ((c, z), c, z), p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
⊢ ∀ᶠ (p : (ℂ × S) × ℂ × S) in 𝓝 ((c, z), c, z), p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.2 → p.1 = p.2
Tactic:
have o := n.nhds_eq_map_nhds_param ga
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, g c (f c z)) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
⊢ ∀ᶠ (p : (ℂ × S) × ℂ × S) in 𝓝 ((c, z), c, z), p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, g c (f c z)) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
⊢ ∀ᶠ (p : (ℂ × S) × ℂ × S) in 𝓝 ((c, z), c, z), p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, (c, z).2) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
⊢ ∀ᶠ (p : (ℂ × S) × ℂ × S) in 𝓝 ((c, z), c, z), p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, (c, z).2) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
⊢ ∀ᶠ (p : (ℂ × S) × ℂ × S) in 𝓝 ((c, z), c, z), p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.2 → p.1 = p.2
Tactic:
simp only 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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
⊢ ∀ᶠ (p : (ℂ × S) × ℂ × S) in 𝓝 ((c, z), c, z), p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
⊢ ∀ᶠ (p : (ℂ × S) × ℂ × S) in 𝓝 ((c, z), c, z), p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.2 → p.1 = p.2
Tactic:
rw [nhds_prod_eq, 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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
⊢ ∀ᶠ (p : (ℂ × S) × ℂ × S) in
    Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z)) ×ˢ Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z)),
    p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
⊢ ∀ᶠ (p : (ℂ × S) × ℂ × S) in
    Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z)) ×ˢ Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z)),
    p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.2 → p.1 = p.2
Tactic:
simp only [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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
⊢ ∀ᶠ (a : (ℂ × T) × ℂ × T) in 𝓝 (c, f c z) ×ˢ 𝓝 (c, f c z),
    a.1.1 = a.2.1 → f a.1.1 (g a.1.1 a.1.2) = f a.2.1 (g a.2.1 a.2.2) → (a.1.1, g a.1.1 a.1.2) = (a.2.1, g a.2.1 a.2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
⊢ ∀ᶠ (a : (ℂ × T) × ℂ × T) in 𝓝 (c, f c z) ×ˢ 𝓝 (c, f c z),
    a.1.1 = a.2.1 → f a.1.1 (g a.1.1 a.1.2) = f a.2.1 (g a.2.1 a.2.2) → (a.1.1, g a.1.1 a.1.2) = (a.2.1, g a.2.1 a.2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
⊢ ∀ (x : (ℂ × T) × ℂ × T),
    f x.1.1 (g x.1.1 x.1.2) = x.1.2 ∧ f x.2.1 (g x.2.1 x.2.2) = x.2.2 →
      x.1.1 = x.2.1 →
        f x.1.1 (g x.1.1 x.1.2) = f x.2.1 (g x.2.1 x.2.2) → (x.1.1, g x.1.1 x.1.2) = (x.2.1, g x.2.1 x.2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
⊢ ∀ (x : (ℂ × T) × ℂ × T),
    f x.1.1 (g x.1.1 x.1.2) = x.1.2 ∧ f x.2.1 (g x.2.1 x.2.2) = x.2.2 →
      x.1.1 = x.2.1 →
        f x.1.1 (g x.1.1 x.1.2) = f x.2.1 (g x.2.1 x.2.2) → (x.1.1, g x.1.1 x.1.2) = (x.2.1, g x.2.1 x.2.2)
Tactic:
intro ⟨x, y⟩ ⟨ex, ey⟩ h1 h2
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
x y : ℂ × T
ex : f (x, y).1.1 (g (x, y).1.1 (x, y).1.2) = (x, y).1.2
ey : f (x, y).2.1 (g (x, y).2.1 (x, y).2.2) = (x, y).2.2
h1 : (x, y).1.1 = (x, y).2.1
h2 : f (x, y).1.1 (g (x, y).1.1 (x, y).1.2) = f (x, y).2.1 (g (x, y).2.1 (x, y).2.2)
⊢ ((x, y).1.1, g (x, y).1.1 (x, y).1.2) = ((x, y).2.1, g (x, y).2.1 (x, y).2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
x y : ℂ × T
ex : f (x, y).1.1 (g (x, y).1.1 (x, y).1.2) = (x, y).1.2
ey : f (x, y).2.1 (g (x, y).2.1 (x, y).2.2) = (x, y).2.2
h1 : (x, y).1.1 = (x, y).2.1
h2 : f (x, y).1.1 (g (x, y).1.1 (x, y).1.2) = f (x, y).2.1 (g (x, y).2.1 (x, y).2.2)
⊢ ((x, y).1.1, g (x, y).1.1 (x, y).1.2) = ((x, y).2.1, g (x, y).2.1 (x, y).2.2)
Tactic:
simp only at h1
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
x y : ℂ × T
ex : f (x, y).1.1 (g (x, y).1.1 (x, y).1.2) = (x, y).1.2
ey : f (x, y).2.1 (g (x, y).2.1 (x, y).2.2) = (x, y).2.2
h1 : x.1 = y.1
h2 : f (x, y).1.1 (g (x, y).1.1 (x, y).1.2) = f (x, y).2.1 (g (x, y).2.1 (x, y).2.2)
⊢ ((x, y).1.1, g (x, y).1.1 (x, y).1.2) = ((x, y).2.1, g (x, y).2.1 (x, y).2.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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
x y : ℂ × T
ex : f (x, y).1.1 (g (x, y).1.1 (x, y).1.2) = (x, y).1.2
ey : f (x, y).2.1 (g (x, y).2.1 (x, y).2.2) = (x, y).2.2
h1 : x.1 = y.1
h2 : f (x, y).1.1 (g (x, y).1.1 (x, y).1.2) = f (x, y).2.1 (g (x, y).2.1 (x, y).2.2)
⊢ ((x, y).1.1, g (x, y).1.1 (x, y).1.2) = ((x, y).2.1, g (x, y).2.1 (x, y).2.2)
Tactic:
simp only [h1] at ex ey h2 ⊢
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
x y : ℂ × T
ey : f y.1 (g y.1 y.2) = y.2
h1 : x.1 = y.1
ex : f y.1 (g y.1 x.2) = x.2
h2 : f y.1 (g y.1 x.2) = f y.1 (g y.1 y.2)
⊢ (y.1, g y.1 x.2) = (y.1, g y.1 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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
x y : ℂ × T
ey : f y.1 (g y.1 y.2) = y.2
h1 : x.1 = y.1
ex : f y.1 (g y.1 x.2) = x.2
h2 : f y.1 (g y.1 x.2) = f y.1 (g y.1 y.2)
⊢ (y.1, g y.1 x.2) = (y.1, g y.1 y.2)
Tactic:
simp only [ex, ey] at h2
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
x y : ℂ × T
ey : f y.1 (g y.1 y.2) = y.2
h1 : x.1 = y.1
ex : f y.1 (g y.1 x.2) = x.2
h2 : x.2 = y.2
⊢ (y.1, g y.1 x.2) = (y.1, g y.1 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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
n : NontrivialHolomorphicAt (g c) (f c z)
o : 𝓝 (c, z) = Filter.map (fun p => (p.1, g p.1 p.2)) (𝓝 (c, f c z))
x y : ℂ × T
ey : f y.1 (g y.1 y.2) = y.2
h1 : x.1 = y.1
ex : f y.1 (g y.1 x.2) = x.2
h2 : x.2 = y.2
⊢ (y.1, g y.1 x.2) = (y.1, g y.1 y.2)
Tactic:
simp only [h2]
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 : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
⊢ NontrivialHolomorphicAt (g c) (f c z)
Tactic:
have e : (c, z) = (c, g c (f c z)) := by rw [gf.self_of_nhds]
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 : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
e : (c, z) = (c, g c (f c z))
⊢ NontrivialHolomorphicAt (g c) (f c 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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
e : (c, z) = (c, g c (f c z))
⊢ NontrivialHolomorphicAt (g c) (f c z)
Tactic:
rw [e] 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
c : ℂ
z : S
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, g c (f c z))
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
e : (c, z) = (c, g c (f c z))
⊢ NontrivialHolomorphicAt (g c) (f c 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
c : ℂ
z : S
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, g c (f c z))
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
e : (c, z) = (c, g c (f c z))
⊢ NontrivialHolomorphicAt (g c) (f c z)
Tactic:
refine (NontrivialHolomorphicAt.anti ?_ fa.along_snd ga.along_snd).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
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, g c (f c z))
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
e : (c, z) = (c, g c (f c z))
⊢ NontrivialHolomorphicAt (fun z => f c (g c z)) (f c 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
c : ℂ
z : S
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, g c (f c z))
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
e : (c, z) = (c, g c (f c z))
⊢ NontrivialHolomorphicAt (fun z => f c (g c z)) (f c z)
Tactic:
refine (nontrivialHolomorphicAt_id _).congr ?_
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
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, g c (f c z))
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
e : (c, z) = (c, g c (f c z))
⊢ (𝓝 (f c z)).EventuallyEq (fun w => w) fun z => f c (g c 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
c : ℂ
z : S
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, g c (f c z))
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
e : (c, z) = (c, g c (f c z))
⊢ (𝓝 (f c z)).EventuallyEq (fun w => w) fun z => f c (g c z)
Tactic:
refine ((continuousAt_const.prod continuousAt_id).eventually fg).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
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, g c (f c z))
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
e : (c, z) = (c, g c (f c z))
⊢ ∀ (x : T), f (c, id x).1 (g (c, id x).1 (c, id x).2) = (c, id x).2 → (fun w => w) x = (fun z => f c (g c z)) 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
c : ℂ
z : S
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, g c (f c z))
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
e : (c, z) = (c, g c (f c z))
⊢ ∀ (x : T), f (c, id x).1 (g (c, id x).1 (c, id x).2) = (c, id x).2 → (fun w => w) x = (fun z => f c (g c z)) x
Tactic:
exact fun _ e ↦ e.symm
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 : ℂ → T → S
ga : 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
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
⊢ (c, z) = (c, g c (f c z))
Tactic:
rw [gf.self_of_nhds]
State after:
no goals