Theorem: ComplexInverseFun.Cinv.zz (Ray/AnalyticManifold/Inverse.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
i : Cinv f c z
⊢ ↑(extChartAt I z).symm (c, i.z').2 = z
Tactic:
simp only [Prod.snd, Cinv.z', PartialEquiv.left_inv _ (mem_extChartAt_source _ _)]
State after:
no goals