Theorem: inChart_critical (Ray/AnalyticManifold/OneDimension.lean)

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)
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), mfderiv I I (f p.1) p.2 = 0 ↔ deriv (inChart f c z p.1) (↑(extChartAt I z) p.2) = 0
Tactic:
apply (fa.continuousAt.eventually_mem ((isOpen_extChartAt_source I (f c z)).mem_nhds
  (mem_extChartAt_source I (f c z)))).mp
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)
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z),
    uncurry f x ∈ (extChartAt I (f c z)).source →
      (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c z x.1) (↑(extChartAt I z) x.2) = 0)

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)
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z),
    uncurry f x ∈ (extChartAt I (f c z)).source →
      (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c z x.1) (↑(extChartAt I z) x.2) = 0)
Tactic:
apply ((isOpen_extChartAt_source II (c, z)).eventually_mem (mem_extChartAt_source _ _)).mp
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)
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z),
    x ∈ (extChartAt (I.prod I) (c, z)).source →
      uncurry f x ∈ (extChartAt I (f c z)).source →
        (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c z x.1) (↑(extChartAt I z) x.2) = 0)

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)
⊢ ∀ᶠ (x : ℂ × S) in 𝓝 (c, z),
    x ∈ (extChartAt (I.prod I) (c, z)).source →
      uncurry f x ∈ (extChartAt I (f c z)).source →
        (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c z x.1) (↑(extChartAt I z) x.2) = 0)
Tactic:
refine fa.eventually.mp (eventually_of_forall ?_)
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)
⊢ ∀ (x : ℂ × S),
    HolomorphicAt (I.prod I) I (uncurry f) x →
      x ∈ (extChartAt (I.prod I) (c, z)).source →
        uncurry f x ∈ (extChartAt I (f c z)).source →
          (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c z x.1) (↑(extChartAt I z) x.2) = 0)

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)
⊢ ∀ (x : ℂ × S),
    HolomorphicAt (I.prod I) I (uncurry f) x →
      x ∈ (extChartAt (I.prod I) (c, z)).source →
        uncurry f x ∈ (extChartAt I (f c z)).source →
          (mfderiv I I (f x.1) x.2 = 0 ↔ deriv (inChart f c z x.1) (↑(extChartAt I z) x.2) = 0)
Tactic:
intro ⟨e, w⟩ fa m fm
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)
m : (e, w) ∈ (extChartAt (I.prod I) (c, z)).source
fm : uncurry f (e, w) ∈ (extChartAt I (f c z)).source
⊢ mfderiv I I (f (e, w).1) (e, w).2 = 0 ↔ deriv (inChart f c z (e, w).1) (↑(extChartAt I z) (e, w).2) = 0

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)
m : (e, w) ∈ (extChartAt (I.prod I) (c, z)).source
fm : uncurry f (e, w) ∈ (extChartAt I (f c z)).source
⊢ mfderiv I I (f (e, w).1) (e, w).2 = 0 ↔ deriv (inChart f c z (e, w).1) (↑(extChartAt I z) (e, w).2) = 0
Tactic:
simp only [extChartAt_prod, PartialEquiv.prod_source, extChartAt_eq_refl, PartialEquiv.refl_source,
  mem_prod, mem_univ, true_and_iff] at m
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 : uncurry f (e, w) ∈ (extChartAt I (f c z)).source
m : w ∈ (extChartAt I z).source
⊢ mfderiv I I (f (e, w).1) (e, w).2 = 0 ↔ deriv (inChart f c z (e, w).1) (↑(extChartAt I z) (e, w).2) = 0

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 : uncurry f (e, w) ∈ (extChartAt I (f c z)).source
m : w ∈ (extChartAt I z).source
⊢ mfderiv I I (f (e, w).1) (e, w).2 = 0 ↔ deriv (inChart f c z (e, w).1) (↑(extChartAt I z) (e, w).2) = 0
Tactic:
simp only [uncurry] at fm
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
⊢ mfderiv I I (f (e, w).1) (e, w).2 = 0 ↔ deriv (inChart f c z (e, w).1) (↑(extChartAt I z) (e, w).2) = 0

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
⊢ mfderiv I I (f (e, w).1) (e, w).2 = 0 ↔ deriv (inChart f c z (e, w).1) (↑(extChartAt I z) (e, w).2) = 0
Tactic:
have m' := PartialEquiv.map_source _ m
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
⊢ mfderiv I I (f (e, w).1) (e, w).2 = 0 ↔ deriv (inChart f c z (e, w).1) (↑(extChartAt I z) (e, w).2) = 0

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
⊢ mfderiv I I (f (e, w).1) (e, w).2 = 0 ↔ deriv (inChart f c z (e, w).1) (↑(extChartAt I z) (e, w).2) = 0
Tactic:
simp only [← mfderiv_eq_zero_iff_deriv_eq_zero]
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
⊢ mfderiv I I (f e) w = 0 ↔ mfderiv I I (inChart f c z e) (↑(extChartAt I z) w) = 0

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
⊢ mfderiv I I (f e) w = 0 ↔ mfderiv I I (inChart f c z e) (↑(extChartAt I z) w) = 0
Tactic:
have cd : HolomorphicAt I I (extChartAt I (f c z)) (f e w) := HolomorphicAt.extChartAt fm
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)
⊢ mfderiv I I (f e) w = 0 ↔ mfderiv I I (inChart f c z e) (↑(extChartAt I z) w) = 0

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)
⊢ mfderiv I I (f e) w = 0 ↔ mfderiv I I (inChart f c z e) (↑(extChartAt I z) w) = 0
Tactic:
have fd : HolomorphicAt I I (f e ∘ (extChartAt I z).symm) (extChartAt I z w) := by
  simp only [Function.comp]
  exact HolomorphicAt.comp_of_eq fa.along_snd (HolomorphicAt.extChartAt_symm m')
    (PartialEquiv.right_inv _ m)
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)
⊢ mfderiv I I (f e) w = 0 ↔ mfderiv I I (inChart f c z e) (↑(extChartAt I z) w) = 0

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)
⊢ mfderiv I I (f e) w = 0 ↔ mfderiv I I (inChart f c z e) (↑(extChartAt I z) w) = 0
Tactic:
have ce : inChart f c z e = extChartAt I (f c z) ∘ f e ∘ (extChartAt I z).symm := rfl
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 (inChart f c z e) (↑(extChartAt I z) w) = 0

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

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)
⊢ HolomorphicAt I I (f e ∘ ↑(extChartAt I z).symm) (↑(extChartAt I z) w)
Tactic:
simp only [Function.comp]
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)
⊢ HolomorphicAt I I (fun x => f e (↑(extChartAt I z).symm x)) (↑(extChartAt I z) w)

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)
⊢ HolomorphicAt I I (fun x => f e (↑(extChartAt I z).symm x)) (↑(extChartAt I z) w)
Tactic:
exact HolomorphicAt.comp_of_eq fa.along_snd (HolomorphicAt.extChartAt_symm m')
  (PartialEquiv.right_inv _ m)
State after:
no goals

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 (↑(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
Tactic:
simp only [mderiv_comp_eq_zero_iff, Function.comp]
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))) = 0 ∨
      mfderiv I I (fun y => f e y) (↑(extChartAt I z).symm (↑(extChartAt I z) w)) = 0 ∨
        mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0

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 (↑(extChartAt I (f c z))) (f e (↑(extChartAt I z).symm (↑(extChartAt I z) w))) = 0 ∨
      mfderiv I I (fun y => f e y) (↑(extChartAt I z).symm (↑(extChartAt I z) w)) = 0 ∨
        mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0
Tactic:
rw [(extChartAt I z).left_inv m]
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 w) = 0 ∨
      mfderiv I I (fun y => f e y) w = 0 ∨ mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0

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 (↑(extChartAt I (f c z))) (f e w) = 0 ∨
      mfderiv I I (fun y => f e y) w = 0 ∨ mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0
Tactic:
simp only [extChartAt_mderiv_ne_zero' fm, false_or]
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 (fun y => f e y) w = 0 ∨ mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0

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 (fun y => f e y) w = 0 ∨ mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0
Tactic:
constructor
State after:
case mp
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 (fun y => f e y) w = 0 ∨ mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0

case mpr
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 (fun y => f e y) w = 0 ∨ mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0 →
    mfderiv I I (f e) w = 0

State before:
case mp
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 (fun y => f e y) w = 0 ∨ mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0
Tactic:
intro h
State after:
case mp
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
h : mfderiv I I (f e) w = 0
⊢ mfderiv I I (fun y => f e y) w = 0 ∨ mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0

State before:
case mp
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
h : mfderiv I I (f e) w = 0
⊢ mfderiv I I (fun y => f e y) w = 0 ∨ mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0
Tactic:
left
State after:
case mp.h
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
h : mfderiv I I (f e) w = 0
⊢ mfderiv I I (fun y => f e y) w = 0

State before:
case mp.h
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
h : mfderiv I I (f e) w = 0
⊢ mfderiv I I (fun y => f e y) w = 0
Tactic:
exact h
State after:
no goals

State before:
case mpr
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 (fun y => f e y) w = 0 ∨ mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0 →
    mfderiv I I (f e) w = 0
Tactic:
intro h
State after:
case mpr
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
h : mfderiv I I (fun y => f e y) w = 0 ∨ mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0
⊢ mfderiv I I (f e) w = 0

State before:
case mpr
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
h : mfderiv I I (fun y => f e y) w = 0 ∨ mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0
⊢ mfderiv I I (f e) w = 0
Tactic:
cases' h with h h
State after:
case mpr.inl
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
h : mfderiv I I (fun y => f e y) w = 0
⊢ mfderiv I I (f e) w = 0

case mpr.inr
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
h : mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0
⊢ mfderiv I I (f e) w = 0

State before:
case mpr.inl
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
h : mfderiv I I (fun y => f e y) w = 0
⊢ mfderiv I I (f e) w = 0

case mpr.inr
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
h : mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0
⊢ mfderiv I I (f e) w = 0
Tactic:
exact h
State after:
case mpr.inr
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
h : mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0
⊢ mfderiv I I (f e) w = 0

State before:
case mpr.inr
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
h : mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 0
⊢ mfderiv I I (f e) w = 0
Tactic:
simpa only using extChartAt_symm_mderiv_ne_zero' m' h
State after:
no goals

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
⊢ ↑(extChartAt I z).symm (↑(extChartAt I z) w) = w
Tactic:
exact PartialEquiv.left_inv _ m
State after:
no goals

State before:
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
Tactic:
simp only [Function.comp, PartialEquiv.left_inv _ m]
State after:
no goals