Theorem: ComplexInverseFun.Cinv.dhi_dh (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.dhi (i.dh t) = t
Tactic:
intro ⟨u, v⟩
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
u v : ℂ
⊢ i.dhi (i.dh (u, v)) = (u, v)

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
u v : ℂ
⊢ i.dhi (i.dh (u, v)) = (u, v)
Tactic:
simp only [Cinv.dh, Cinv.dhi, dc, dz, Cinv.dfi', Cinv.df', Cinv.df, i.dei_de', i.dei_de,
  i.dfzi_dfz, ContinuousLinearMap.comp_apply, ContinuousLinearMap.prod_apply,
  ContinuousLinearMap.sub_apply, ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd',
  ContinuousLinearMap.add_apply, ContinuousLinearMap.map_add, ContinuousLinearMap.map_sub,
  add_sub_cancel_left, ContinuousLinearMap.coe_snd]
State after:
no goals