Theorem: inChart_critical
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
c : ℂ
z : S
fa✝ : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
e : ℂ
w : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (e, w)
fm : f e w ∈ (extChartAt I (f c z)).source
m : w ∈ (extChartAt I z).source
m' : ↑(extChartAt I z) w ∈ (extChartAt I z).target
cd : HolomorphicAt I I (↑(extChartAt I (f c z))) (f e w)
fd : HolomorphicAt I I (f e ∘ ↑(extChartAt I z).symm) (↑(extChartAt I z) w)
ce : inChart f c z e = ↑(extChartAt I (f c z)) ∘ f e ∘ ↑(extChartAt I z).symm
⊢ mfderiv I I (f e) w = 0 ↔ mfderiv I I (inChart f c z e) (↑(extChartAt I z) w) = 0
Tactic:
rw [ce, mfderiv_comp_of_eq cd.mdifferentiableAt fd.mdifferentiableAt ?blah,
  mfderiv_comp_of_eq fa.along_snd.mdifferentiableAt
    (HolomorphicAt.extChartAt_symm m').mdifferentiableAt]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
c : ℂ
z : S
fa✝ : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
e : ℂ
w : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (e, w)
fm : f e w ∈ (extChartAt I (f c z)).source
m : w ∈ (extChartAt I z).source
m' : ↑(extChartAt I z) w ∈ (extChartAt I z).target
cd : HolomorphicAt I I (↑(extChartAt I (f c z))) (f e w)
fd : HolomorphicAt I I (f e ∘ ↑(extChartAt I z).symm) (↑(extChartAt I z) w)
ce : inChart f c z e = ↑(extChartAt I (f c z)) ∘ f e ∘ ↑(extChartAt I z).symm
⊢ mfderiv I I (f e) w = 0 ↔
    (mfderiv I I (↑(extChartAt I (f c z))) ((f e ∘ ↑(extChartAt I z).symm) (↑(extChartAt I z) w))).comp
        ((mfderiv I I (fun y => f e y) (↑(extChartAt I z).symm (↑(extChartAt I z) w))).comp
          (mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w))) =
      0

S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
c : ℂ
z : S
fa✝ : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
e : ℂ
w : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (e, w)
fm : f e w ∈ (extChartAt I (f c z)).source
m : w ∈ (extChartAt I z).source
m' : ↑(extChartAt I z) w ∈ (extChartAt I z).target
cd : HolomorphicAt I I (↑(extChartAt I (f c z))) (f e w)
fd : HolomorphicAt I I (f e ∘ ↑(extChartAt I z).symm) (↑(extChartAt I z) w)
ce : inChart f c z e = ↑(extChartAt I (f c z)) ∘ f e ∘ ↑(extChartAt I z).symm
⊢ ↑(extChartAt I z).symm (↑(extChartAt I z) w) = w

case blah
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
c : ℂ
z : S
fa✝ : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
e : ℂ
w : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (e, w)
fm : f e w ∈ (extChartAt I (f c z)).source
m : w ∈ (extChartAt I z).source
m' : ↑(extChartAt I z) w ∈ (extChartAt I z).target
cd : HolomorphicAt I I (↑(extChartAt I (f c z))) (f e w)
fd : HolomorphicAt I I (f e ∘ ↑(extChartAt I z).symm) (↑(extChartAt I z) w)
ce : inChart f c z e = ↑(extChartAt I (f c z)) ∘ f e ∘ ↑(extChartAt I z).symm
⊢ (f e ∘ ↑(extChartAt I z).symm) (↑(extChartAt I z) w) = f e w