internlm/Lean-Github huggingface dataset:
Theorem: ComplexInverseFun.Cinv.has_df'
Proof state before:
case hf.hh
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
⊢ HasMFDerivAt (I.prod I) I (fun y => ↑(extChartAt I z).symm y.2) (c, i.z') (i.de.comp dz)

case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
refine HasMFDerivAt.comp _ ?_ (hasMFDerivAt_snd _ _ _)
Proof state after:
case hf.hh
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
⊢ HasMFDerivAt I I ↑(extChartAt I z).symm (c, i.z').2 i.de

case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Theorem: ComplexInverseFun.Cinv.has_df'
Proof state before:
case hf.hh
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
⊢ HasMFDerivAt I I ↑(extChartAt I z).symm (c, i.z').2 i.de

case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
exact (HolomorphicAt.extChartAt_symm (mem_extChartAt_target _ _)).mdifferentiableAt.hasMFDerivAt
Proof state after:
case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Theorem: ComplexInverseFun.Cinv.has_df'
Proof state before:
case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y (↑(extChartAt I z).symm (c, i.z').2)) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
rw [i.zz]
Proof state after:
case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y z) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Theorem: ComplexInverseFun.Cinv.has_df'
Proof state before:
case hf.fh0
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
⊢ HasMFDerivAt I I (fun y => f y z) (c, i.z').1 i.dfc

case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
exact i.fa.along_fst.mdifferentiableAt.hasMFDerivAt
Proof state after:
case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Theorem: ComplexInverseFun.Cinv.has_df'
Proof state before:
case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) (↑(extChartAt I z).symm (c, i.z').2) i.dfz
Tactic:
rw [i.zz]
Proof state after:
case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) z i.dfz
Theorem: ComplexInverseFun.Cinv.has_df'
Proof state before:
case hf.fh1
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
⊢ HasMFDerivAt I I (fun y => f (c, i.z').1 y) z i.dfz
Tactic:
exact i.fa.along_snd.mdifferentiableAt.hasMFDerivAt
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.has_dh
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
⊢ HasMFDerivAt (I.prod I) (I.prod I) i.h (c, i.z') i.dh
Tactic:
refine HasMFDerivAt.prod ?_ i.has_df'
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
⊢ HasMFDerivAt (I.prod I) I (fun y => y.1) (c, i.z') dc
Theorem: ComplexInverseFun.Cinv.has_dh
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
⊢ HasMFDerivAt (I.prod I) I (fun y => y.1) (c, i.z') dc
Tactic:
apply hasMFDerivAt_fst
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.dei_de
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 : ℂ), i.dei (i.de t) = t
Tactic:
intro t
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
t : ℂ
⊢ i.dei (i.de t) = t
Theorem: ComplexInverseFun.Cinv.dei_de
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 : ℂ
⊢ i.dei (i.de t) = t
Tactic:
have h := ContinuousLinearMap.ext_iff.mp
  (extChartAt_mderiv_right_inverse' (mem_extChartAt_source I z)) t
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
t : ℂ
h :
  ((mfderiv I I (↑(extChartAt I z)) z).comp (mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) z))) t =
    (ContinuousLinearMap.id ℂ (TangentSpace I (↑(extChartAt I z) z))) t
⊢ i.dei (i.de t) = t
Theorem: ComplexInverseFun.Cinv.dei_de
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 : ℂ
h :
  ((mfderiv I I (↑(extChartAt I z)) z).comp (mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) z))) t =
    (ContinuousLinearMap.id ℂ (TangentSpace I (↑(extChartAt I z) z))) t
⊢ i.dei (i.de t) = t
Tactic:
simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.id_apply] at h
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
t : ℂ
h : (mfderiv I I (↑(extChartAt I z)) z) ((mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) z)) t) = t
⊢ i.dei (i.de t) = t
Theorem: ComplexInverseFun.Cinv.dei_de
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 : ℂ
h : (mfderiv I I (↑(extChartAt I z)) z) ((mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) z)) t) = t
⊢ i.dei (i.de t) = t
Tactic:
exact h
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.dei_de'
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 : TangentSpace I (f c z)), i.dei' (i.de' t) = t
Tactic:
intro t
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
t : TangentSpace I (f c z)
⊢ i.dei' (i.de' t) = t
Theorem: ComplexInverseFun.Cinv.dei_de'
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 : TangentSpace I (f c z)
⊢ i.dei' (i.de' t) = t
Tactic:
have h := ContinuousLinearMap.ext_iff.mp (extChartAt_mderiv_left_inverse
  (mem_extChartAt_source I (f c z))) t
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
t : TangentSpace I (f c z)
h :
  ((mfderiv I I (↑(extChartAt I (f c z)).symm) (↑(extChartAt I (f c z)) (f c z))).comp
        (mfderiv I I (↑(extChartAt I (f c z))) (f c z)))
      t =
    (ContinuousLinearMap.id ℂ (TangentSpace I (f c z))) t
⊢ i.dei' (i.de' t) = t
Theorem: ComplexInverseFun.Cinv.dei_de'
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 : TangentSpace I (f c z)
h :
  ((mfderiv I I (↑(extChartAt I (f c z)).symm) (↑(extChartAt I (f c z)) (f c z))).comp
        (mfderiv I I (↑(extChartAt I (f c z))) (f c z)))
      t =
    (ContinuousLinearMap.id ℂ (TangentSpace I (f c z))) t
⊢ i.dei' (i.de' t) = t
Tactic:
simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.id_apply] at h
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
t : TangentSpace I (f c z)
h :
  (mfderiv I I (↑(extChartAt I (f c z)).symm) (↑(extChartAt I (f c z)) (f c z)))
      ((mfderiv I I (↑(extChartAt I (f c z))) (f c z)) t) =
    (ContinuousLinearMap.id ℂ (TangentSpace I (f c z))) t
⊢ i.dei' (i.de' t) = t
Theorem: ComplexInverseFun.Cinv.dei_de'
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 : TangentSpace I (f c z)
h :
  (mfderiv I I (↑(extChartAt I (f c z)).symm) (↑(extChartAt I (f c z)) (f c z)))
      ((mfderiv I I (↑(extChartAt I (f c z))) (f c z)) t) =
    (ContinuousLinearMap.id ℂ (TangentSpace I (f c z))) t
⊢ i.dei' (i.de' t) = t
Tactic:
exact h
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.de_dei
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 : TangentSpace I z), i.de (i.dei t) = t
Tactic:
intro t
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
t : TangentSpace I z
⊢ i.de (i.dei t) = t
Theorem: ComplexInverseFun.Cinv.de_dei
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 : TangentSpace I z
⊢ i.de (i.dei t) = t
Tactic:
have h := ContinuousLinearMap.ext_iff.mp (extChartAt_mderiv_left_inverse
  (mem_extChartAt_source I z)) t
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
t : TangentSpace I z
h :
  ((mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) z)).comp (mfderiv I I (↑(extChartAt I z)) z)) t =
    (ContinuousLinearMap.id ℂ (TangentSpace I z)) t
⊢ i.de (i.dei t) = t
Theorem: ComplexInverseFun.Cinv.de_dei
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 : TangentSpace I z
h :
  ((mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) z)).comp (mfderiv I I (↑(extChartAt I z)) z)) t =
    (ContinuousLinearMap.id ℂ (TangentSpace I z)) t
⊢ i.de (i.dei t) = t
Tactic:
simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.id_apply] at h
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
t : TangentSpace I z
h :
  (mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) z)) ((mfderiv I I (↑(extChartAt I z)) z) t) =
    (ContinuousLinearMap.id ℂ (TangentSpace I z)) t
⊢ i.de (i.dei t) = t
Theorem: ComplexInverseFun.Cinv.de_dei
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 : TangentSpace I z
h :
  (mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) z)) ((mfderiv I I (↑(extChartAt I z)) z) t) =
    (ContinuousLinearMap.id ℂ (TangentSpace I z)) t
⊢ i.de (i.dei t) = t
Tactic:
exact h
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.de_dei'
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 : ℂ), i.de' (i.dei' t) = t
Tactic:
intro t
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
t : ℂ
⊢ i.de' (i.dei' t) = t
Theorem: ComplexInverseFun.Cinv.de_dei'
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 : ℂ
⊢ i.de' (i.dei' t) = t
Tactic:
have h := ContinuousLinearMap.ext_iff.mp (extChartAt_mderiv_right_inverse'
  (mem_extChartAt_source I (f c z))) t
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
t : ℂ
h :
  ((mfderiv I I (↑(extChartAt I (f c z))) (f c z)).comp
        (mfderiv I I (↑(extChartAt I (f c z)).symm) (↑(extChartAt I (f c z)) (f c z))))
      t =
    (ContinuousLinearMap.id ℂ (TangentSpace I (↑(extChartAt I (f c z)) (f c z)))) t
⊢ i.de' (i.dei' t) = t
Theorem: ComplexInverseFun.Cinv.de_dei'
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 : ℂ
h :
  ((mfderiv I I (↑(extChartAt I (f c z))) (f c z)).comp
        (mfderiv I I (↑(extChartAt I (f c z)).symm) (↑(extChartAt I (f c z)) (f c z))))
      t =
    (ContinuousLinearMap.id ℂ (TangentSpace I (↑(extChartAt I (f c z)) (f c z)))) t
⊢ i.de' (i.dei' t) = t
Tactic:
simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.id_apply] at h
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
t : ℂ
h :
  (mfderiv I I (↑(extChartAt I (f c z))) (f c z))
      ((mfderiv I I (↑(extChartAt I (f c z)).symm) (↑(extChartAt I (f c z)) (f c z))) t) =
    t
⊢ i.de' (i.dei' t) = t
Theorem: ComplexInverseFun.Cinv.de_dei'
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 : ℂ
h :
  (mfderiv I I (↑(extChartAt I (f c z))) (f c z))
      ((mfderiv I I (↑(extChartAt I (f c z)).symm) (↑(extChartAt I (f c z)) (f c z))) t) =
    t
⊢ i.de' (i.dei' t) = t
Tactic:
exact h
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.dhi_dh
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 : ℂ × ℂ), i.dhi (i.dh t) = t
Tactic:
intro ⟨u, v⟩
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
u v : ℂ
⊢ i.dhi (i.dh (u, v)) = (u, v)
Theorem: ComplexInverseFun.Cinv.dhi_dh
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
u v : ℂ
⊢ i.dhi (i.dh (u, v)) = (u, v)
Tactic:
simp only [Cinv.dh, Cinv.dhi, dc, dz, Cinv.dfi', Cinv.df', Cinv.df, i.dei_de', i.dei_de,
  i.dfzi_dfz, ContinuousLinearMap.comp_apply, ContinuousLinearMap.prod_apply,
  ContinuousLinearMap.sub_apply, ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd',
  ContinuousLinearMap.add_apply, ContinuousLinearMap.map_add, ContinuousLinearMap.map_sub,
  add_sub_cancel_left, ContinuousLinearMap.coe_snd]
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.dh_dhi
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 : ℂ × ℂ), i.dh (i.dhi t) = t
Tactic:
intro ⟨u, v⟩
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
u v : ℂ
⊢ i.dh (i.dhi (u, v)) = (u, v)
Theorem: ComplexInverseFun.Cinv.dh_dhi
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
u v : ℂ
⊢ i.dh (i.dhi (u, v)) = (u, v)
Tactic:
simp only [Cinv.dh, Cinv.dhi, dc, dz, Cinv.dfi', Cinv.df', Cinv.df, i.de_dei', i.de_dei,
  i.dfz_dfzi, ContinuousLinearMap.comp_apply, ContinuousLinearMap.prod_apply,
  ContinuousLinearMap.sub_apply, ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd',
  ContinuousLinearMap.add_apply, ContinuousLinearMap.map_add, ContinuousLinearMap.map_sub,
  add_sub_cancel_left, ← add_sub_assoc, ContinuousLinearMap.coe_snd, ContinuousLinearMap.coe_fst]
Proof state after:
no goals
Theorem: ComplexInverseFun.Cinv.inv_at
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
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) z
Tactic:
have a := ContDiffAt.localInverse_apply_image i.ha.contDiffAt i.has_dhe le_top
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
a : ⋯.localInverse ⋯ ⋯ (i.h (c, i.z')) = (c, i.z')
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) z