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 : ℂ), 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 : ℂ
⊢ 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 : ℂ
⊢ 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
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

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

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