Theorem: ComplexInverseFun.Cinv.dei_de (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
⊢ ∀ (t : ℂ), i.dei (i.de t) = t
Tactic:
intro t
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

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
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

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
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

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
State after:
no goals