Theorem: ComplexInverseFun.Cinv.de_dei (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 : TangentSpace I z), i.de (i.dei 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 : TangentSpace I z
⊢ i.de (i.dei 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 : 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
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

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

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