internlm/Lean-Github huggingface dataset:
Theorem: ComplexInverseFun.Cinv.right_inv
Proof state before:
case refine_1.hh.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
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) (c, f c z)
Tactic:
apply continuousAt_snd.comp
Proof state after:
case refine_1.hh.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
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => ↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)) (c, f c z)
Theorem: ComplexInverseFun.Cinv.right_inv
Proof state before:
case refine_1.hh.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
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => ↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)) (c, f c z)
Tactic:
refine (PartialHomeomorph.continuousAt i.he.symm ?_).comp ?_
Proof state after:
case refine_1.hh.refine_2.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
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2) ∈ i.he.symm.source

case refine_1.hh.refine_2.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
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => (x.1, ↑(extChartAt I (f c z)) x.2)) (c, f c z)
Theorem: ComplexInverseFun.Cinv.right_inv
Proof state before:
case refine_1.hh.refine_2.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
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2) ∈ i.he.symm.source
Tactic:
simp only [m', (he i).symm_source]
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.right_inv
Proof state before:
case refine_1.hh.refine_2.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
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => (x.1, ↑(extChartAt I (f c z)) x.2)) (c, f c z)
Tactic:
apply continuousAt_fst.prod
Proof state after:
case refine_1.hh.refine_2.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
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => ↑(extChartAt I (f c z)) x.2) (c, f c z)
Theorem: ComplexInverseFun.Cinv.right_inv
Proof state before:
case refine_1.hh.refine_2.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
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => ↑(extChartAt I (f c z)) x.2) (c, f c z)
Tactic:
apply (continuousAt_extChartAt I _).comp_of_eq
Proof state after:
case refine_1.hh.refine_2.refine_2.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
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => x.2) (c, f c z)

case refine_1.hh.refine_2.refine_2.hy
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
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ (c, f c z).2 = f c z
Theorem: ComplexInverseFun.Cinv.right_inv
Proof state before:
case refine_1.hh.refine_2.refine_2.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
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ContinuousAt (fun x => x.2) (c, f c z)
Tactic:
exact continuousAt_snd
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.right_inv
Proof state before:
case refine_1.hh.refine_2.refine_2.hy
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
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ (c, f c z).2 = f c z
Tactic:
rfl
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.right_inv
Proof state before:
case refine_1.e
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
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ ((c, f c z).1, (extChartAt I z).symm.1 (↑i.he.symm ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2)).2) = (c, z)
Tactic:
simp only [i.inv_at, PartialEquiv.left_inv _ (mem_extChartAt_source _ _),
  PartialEquiv.invFun_as_coe]
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ f (c, f c z).1 (↑(extChartAt I z).symm (↑i.he.symm ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2)).2) ∈
    (extChartAt I (f c z)).source
Tactic:
simp only [i.inv_at, PartialEquiv.left_inv _ (mem_extChartAt_source _ _)]
Proof state after:
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
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ f c z ∈ (extChartAt I (f c z)).source
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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
c : ℂ
z : S
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m : (c, f c z) ∈ t
⊢ f c z ∈ (extChartAt I (f c z)).source
Tactic:
apply mem_extChartAt_source
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.right_inv
Proof 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
i : Cinv f c z
t : Set (ℂ × T)
ht : (extChartAt (I.prod I) (c, f c z)).source ∩ ↑(extChartAt (I.prod I) (c, f c z)) ⁻¹' i.he.target = t
o : IsOpen t
m' : (c, ↑(extChartAt I (f c z)) (f c z)) ∈ i.he.target
m✝ : (c, f c z) ∈ t
fm :
  ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z),
    f x.1 (↑(extChartAt I z).symm (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
x : ℂ × T
m : x.2 ∈ (extChartAt I (f c z)).source ∧ (x.1, ↑(extChartAt I (f c z)) x.2) ∈ i.he.target
q : PartialHomeomorph (ℂ × ℂ) (ℂ × ℂ)
mf : f x.1 (↑(extChartAt I z).symm (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).2) ∈ (extChartAt I (f c z)).source
inv : i.h (↑q (x.1, ↑(extChartAt I (f c z)) x.2)) = (x.1, ↑(extChartAt I (f c z)) x.2)
hq : i.he.symm = q
⊢ (↑q (x.1, ↑(extChartAt I (f c z)) x.2)).1 = x.1
Tactic:
simp only [← hq, i.inv_fst _ m.2]
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.he_symm_holomorphic
Proof 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
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) (I.prod I) ↑i.he.symm (c, i.fz')
Tactic:
apply AnalyticAt.holomorphicAt
Proof state after:
case fa
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
i : Cinv f c z
⊢ AnalyticAt ℂ ↑i.he.symm (c, i.fz')
Theorem: ComplexInverseFun.Cinv.he_symm_holomorphic
Proof state before:
case fa
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
i : Cinv f c z
⊢ AnalyticAt ℂ ↑i.he.symm (c, i.fz')
Tactic:
have d : ContDiffAt ℂ ⊤ i.he.symm _ :=
  ContDiffAt.to_localInverse i.ha.contDiffAt i.has_dhe le_top
Proof state after:
case fa
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
i : Cinv f c z
d : ContDiffAt ℂ ⊤ (↑i.he.symm) (i.h (c, i.z'))
⊢ AnalyticAt ℂ ↑i.he.symm (c, i.fz')
Theorem: ComplexInverseFun.Cinv.he_symm_holomorphic
Proof state before:
case fa
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
i : Cinv f c z
d : ContDiffAt ℂ ⊤ (↑i.he.symm) (i.h (c, i.z'))
⊢ AnalyticAt ℂ ↑i.he.symm (c, i.fz')
Tactic:
have e : i.h (c, i.z') = (c, i.fz') := by
  simp only [Cinv.h, Cinv.fz', Cinv.f']
  simp only [Cinv.z', (extChartAt I z).left_inv (mem_extChartAt_source _ _)]
Proof state after:
case fa
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
i : Cinv f c z
d : ContDiffAt ℂ ⊤ (↑i.he.symm) (i.h (c, i.z'))
e : i.h (c, i.z') = (c, i.fz')
⊢ AnalyticAt ℂ ↑i.he.symm (c, i.fz')
Theorem: ComplexInverseFun.Cinv.he_symm_holomorphic
Proof state before:
case fa
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
i : Cinv f c z
d : ContDiffAt ℂ ⊤ (↑i.he.symm) (i.h (c, i.z'))
e : i.h (c, i.z') = (c, i.fz')
⊢ AnalyticAt ℂ ↑i.he.symm (c, i.fz')
Tactic:
rw [e] at d
Proof state after:
case fa
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
i : Cinv f c z
d : ContDiffAt ℂ ⊤ ↑i.he.symm (c, i.fz')
e : i.h (c, i.z') = (c, i.fz')
⊢ AnalyticAt ℂ ↑i.he.symm (c, i.fz')
Theorem: ComplexInverseFun.Cinv.he_symm_holomorphic
Proof state before:
case fa
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
i : Cinv f c z
d : ContDiffAt ℂ ⊤ ↑i.he.symm (c, i.fz')
e : i.h (c, i.z') = (c, i.fz')
⊢ AnalyticAt ℂ ↑i.he.symm (c, i.fz')
Tactic:
exact (contDiffAt_iff_analytic_at2 le_top).mp d
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.he_symm_holomorphic
Proof 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
i : Cinv f c z
d : ContDiffAt ℂ ⊤ (↑i.he.symm) (i.h (c, i.z'))
⊢ i.h (c, i.z') = (c, i.fz')
Tactic:
simp only [Cinv.h, Cinv.fz', Cinv.f']
Proof 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
i : Cinv f c z
d : ContDiffAt ℂ ⊤ (↑i.he.symm) (i.h (c, i.z'))
⊢ (c, ↑(extChartAt I (f c z)) (f c (↑(extChartAt I z).symm i.z'))) = (c, ↑(extChartAt I (f c z)) (f c z))
Theorem: ComplexInverseFun.Cinv.he_symm_holomorphic
Proof 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
i : Cinv f c z
d : ContDiffAt ℂ ⊤ (↑i.he.symm) (i.h (c, i.z'))
⊢ (c, ↑(extChartAt I (f c z)) (f c (↑(extChartAt I z).symm i.z'))) = (c, ↑(extChartAt I (f c z)) (f c z))
Tactic:
simp only [Cinv.z', (extChartAt I z).left_inv (mem_extChartAt_source _ _)]
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.ga
Proof 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
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) I (uncurry i.g) (c, f c z)
Tactic:
apply (HolomorphicAt.extChartAt_symm (mem_extChartAt_target I z)).comp_of_eq
Proof state after:
case gh
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
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) I (fun x => (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) (c, f c z)

case e
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
i : Cinv f c z
⊢ (↑i.he.symm ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2)).2 = ↑(extChartAt I z) z
Theorem: ComplexInverseFun.Cinv.ga
Proof state before:
case gh
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
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) I (fun x => (↑i.he.symm (x.1, ↑(extChartAt I (f c z)) x.2)).2) (c, f c z)
Tactic:
refine holomorphicAt_snd.comp (i.he_symm_holomorphic.comp_of_eq ?_ ?_)
Proof state after:
case gh.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
c : ℂ
z : S
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) (I.prod I) (fun x => (x.1, ↑(extChartAt I (f c z)) x.2)) (c, f c z)

case gh.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
c : ℂ
z : S
i : Cinv f c z
⊢ ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2) = (c, i.fz')
Theorem: ComplexInverseFun.Cinv.ga
Proof state before:
case gh.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
c : ℂ
z : S
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) (I.prod I) (fun x => (x.1, ↑(extChartAt I (f c z)) x.2)) (c, f c z)
Tactic:
apply holomorphicAt_fst.prod
Proof state after:
case gh.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
c : ℂ
z : S
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(extChartAt I (f c z)) x.2) (c, f c z)
Theorem: ComplexInverseFun.Cinv.ga
Proof state before:
case gh.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
c : ℂ
z : S
i : Cinv f c z
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(extChartAt I (f c z)) x.2) (c, f c z)
Tactic:
refine (HolomorphicAt.extChartAt ?_).comp holomorphicAt_snd
Proof state after:
case gh.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
c : ℂ
z : S
i : Cinv f c z
⊢ (c, f c z).2 ∈ (extChartAt I (f c z)).source
Theorem: ComplexInverseFun.Cinv.ga
Proof state before:
case gh.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
c : ℂ
z : S
i : Cinv f c z
⊢ (c, f c z).2 ∈ (extChartAt I (f c z)).source
Tactic:
exact mem_extChartAt_source _ _
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.ga
Proof state before:
case gh.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
c : ℂ
z : S
i : Cinv f c z
⊢ ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2) = (c, i.fz')
Tactic:
rfl
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.ga
Proof state before:
case e
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
i : Cinv f c z
⊢ (↑i.he.symm ((c, f c z).1, ↑(extChartAt I (f c z)) (c, f c z).2)).2 = ↑(extChartAt I z) z
Tactic:
exact i.inv_at
Proof state after:
no goals
Theorem: complex_inverse_fun
Proof 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,
    HolomorphicAt (I.prod I) I (uncurry g) (c, f c z) ∧
      (∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2) ∧ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
Tactic:
have i : ComplexInverseFun.Cinv f c z :=
  { fa
    nc }
Proof 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
i : ComplexInverseFun.Cinv f c z
⊢ ∃ g,
    HolomorphicAt (I.prod I) I (uncurry g) (c, f c z) ∧
      (∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2) ∧ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
Theorem: complex_inverse_fun
Proof 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
i : ComplexInverseFun.Cinv f c z
⊢ ∃ g,
    HolomorphicAt (I.prod I) I (uncurry g) (c, f c z) ∧
      (∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2) ∧ ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
Tactic:
use i.g, i.ga, i.left_inv, i.right_inv
Proof state after:
no goals
Theorem: complex_inverse_fun'
Proof 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
Proof 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