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 : TangentSpace I (f c z)), 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 : TangentSpace I (f c z)
⊢ 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 : TangentSpace I (f c z)
⊢ i.dei' (i.de' t) = t
Tactic:
have h := ContinuousLinearMap.ext_iff.mp (extChartAt_mderiv_left_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 : TangentSpace I (f c z)
h :
  ((mfderiv I I (↑(extChartAt I (f c z)).symm) (↑(extChartAt I (f c z)) (f c z))).comp
        (mfderiv I I (↑(extChartAt I (f c z))) (f c z)))
      t =
    (ContinuousLinearMap.id ℂ (TangentSpace I (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 : TangentSpace I (f c z)
h :
  ((mfderiv I I (↑(extChartAt I (f c z)).symm) (↑(extChartAt I (f c z)) (f c z))).comp
        (mfderiv I I (↑(extChartAt I (f c z))) (f c z)))
      t =
    (ContinuousLinearMap.id ℂ (TangentSpace I (f c 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 : TangentSpace I (f c z)
h :
  (mfderiv I I (↑(extChartAt I (f c z)).symm) (↑(extChartAt I (f c z)) (f c z)))
      ((mfderiv I I (↑(extChartAt I (f c z))) (f c z)) t) =
    (ContinuousLinearMap.id ℂ (TangentSpace I (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 : TangentSpace I (f c z)
h :
  (mfderiv I I (↑(extChartAt I (f c z)).symm) (↑(extChartAt I (f c z)) (f c z)))
      ((mfderiv I I (↑(extChartAt I (f c z))) (f c z)) t) =
    (ContinuousLinearMap.id ℂ (TangentSpace I (f c z))) t
⊢ i.dei' (i.de' t) = t
Tactic:
exact h
State after:
no goals