Theorem: ComplexInverseFun.Cinv.inv_at (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
⊢ (↑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
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

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
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
Tactic:
have e : ContDiffAt.localInverse i.ha.contDiffAt i.has_dhe le_top = i.he.symm := rfl
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')
e : ⋯.localInverse ⋯ ⋯ = ↑i.he.symm
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) 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
i : Cinv f c z
a : ⋯.localInverse ⋯ ⋯ (i.h (c, i.z')) = (c, i.z')
e : ⋯.localInverse ⋯ ⋯ = ↑i.he.symm
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) z
Tactic:
rw [e] at a
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 : ↑i.he.symm (i.h (c, i.z')) = (c, i.z')
e : ⋯.localInverse ⋯ ⋯ = ↑i.he.symm
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) 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
i : Cinv f c z
a : ↑i.he.symm (i.h (c, i.z')) = (c, i.z')
e : ⋯.localInverse ⋯ ⋯ = ↑i.he.symm
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) z
Tactic:
clear e
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 : ↑i.he.symm (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

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
a : ↑i.he.symm (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
Tactic:
simp only [Cinv.z', Cinv.h, Cinv.f', PartialEquiv.left_inv _ (mem_extChartAt_source _ _)] at a
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 : ↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z)) = (c, ↑(extChartAt I z) z)
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) 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
i : Cinv f c z
a : ↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z)) = (c, ↑(extChartAt I z) z)
⊢ (↑i.he.symm (c, ↑(extChartAt I (f c z)) (f c z))).2 = ↑(extChartAt I z) z
Tactic:
rw [a]
State after:
no goals