Theorem: mfderiv_ne_zero_eventually' (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)
f0 : mfderiv I I (f c) z ≠ 0
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), mfderiv I I (f p.1) p.2 ≠ 0
Tactic:
set g := inChart f c z
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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), mfderiv I I (f p.1) p.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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), mfderiv I I (f p.1) p.2 ≠ 0
Tactic:
have g0 := inChart_critical fa
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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), mfderiv I I (f p.1) p.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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
g0n : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), deriv (g p.1) (↑(extChartAt I z) p.2) ≠ 0
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), mfderiv I I (f p.1) p.2 ≠ 0
Tactic:
refine g0.mp (g0n.mp (eventually_of_forall fun w g0 e ↦ ?_))
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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0✝ : ∀ᶠ (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
g0n : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), deriv (g p.1) (↑(extChartAt I z) p.2) ≠ 0
w : ℂ × S
g0 : deriv (g w.1) (↑(extChartAt I z) w.2) ≠ 0
e : mfderiv I I (f w.1) w.2 = 0 ↔ deriv (inChart f c z w.1) (↑(extChartAt I z) w.2) = 0
⊢ mfderiv I I (f w.1) 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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0✝ : ∀ᶠ (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
g0n : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), deriv (g p.1) (↑(extChartAt I z) p.2) ≠ 0
w : ℂ × S
g0 : deriv (g w.1) (↑(extChartAt I z) w.2) ≠ 0
e : mfderiv I I (f w.1) w.2 = 0 ↔ deriv (inChart f c z w.1) (↑(extChartAt I z) w.2) = 0
⊢ mfderiv I I (f w.1) w.2 ≠ 0
Tactic:
rw [Ne, e]
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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0✝ : ∀ᶠ (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
g0n : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), deriv (g p.1) (↑(extChartAt I z) p.2) ≠ 0
w : ℂ × S
g0 : deriv (g w.1) (↑(extChartAt I z) w.2) ≠ 0
e : mfderiv I I (f w.1) w.2 = 0 ↔ deriv (inChart f c z w.1) (↑(extChartAt I z) w.2) = 0
⊢ ¬deriv (inChart f c z w.1) (↑(extChartAt I z) 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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0✝ : ∀ᶠ (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
g0n : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), deriv (g p.1) (↑(extChartAt I z) p.2) ≠ 0
w : ℂ × S
g0 : deriv (g w.1) (↑(extChartAt I z) w.2) ≠ 0
e : mfderiv I I (f w.1) w.2 = 0 ↔ deriv (inChart f c z w.1) (↑(extChartAt I z) w.2) = 0
⊢ ¬deriv (inChart f c z w.1) (↑(extChartAt I z) w.2) = 0
Tactic:
exact g0
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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), deriv (g p.1) (↑(extChartAt I z) p.2) ≠ 0
Tactic:
refine ContinuousAt.eventually_ne ?_ ?_
State after:
case refine_1
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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
⊢ ContinuousAt (fun p => deriv (g p.1) (↑(extChartAt I z) p.2)) (c, z)

case refine_2
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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
⊢ deriv (g (c, z).1) (↑(extChartAt I z) (c, z).2) ≠ 0

State before:
case refine_1
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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
⊢ ContinuousAt (fun p => deriv (g p.1) (↑(extChartAt I z) p.2)) (c, z)
Tactic:
have e : (fun p : ℂ × S ↦ deriv (g p.1) (extChartAt I z p.2)) =
  (fun p : ℂ × ℂ ↦ deriv (g p.1) p.2) ∘ fun p : ℂ × S ↦ (p.1, extChartAt I z p.2) := rfl
State after:
case refine_1
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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
e :
  (fun p => deriv (g p.1) (↑(extChartAt I z) p.2)) =
    (fun p => deriv (g p.1) p.2) ∘ fun p => (p.1, ↑(extChartAt I z) p.2)
⊢ ContinuousAt (fun p => deriv (g p.1) (↑(extChartAt I z) p.2)) (c, z)

State before:
case refine_1
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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
e :
  (fun p => deriv (g p.1) (↑(extChartAt I z) p.2)) =
    (fun p => deriv (g p.1) p.2) ∘ fun p => (p.1, ↑(extChartAt I z) p.2)
⊢ ContinuousAt (fun p => deriv (g p.1) (↑(extChartAt I z) p.2)) (c, z)
Tactic:
rw [e]
State after:
case refine_1
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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
e :
  (fun p => deriv (g p.1) (↑(extChartAt I z) p.2)) =
    (fun p => deriv (g p.1) p.2) ∘ fun p => (p.1, ↑(extChartAt I z) p.2)
⊢ ContinuousAt ((fun p => deriv (g p.1) p.2) ∘ fun p => (p.1, ↑(extChartAt I z) p.2)) (c, z)

State before:
case refine_1
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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
e :
  (fun p => deriv (g p.1) (↑(extChartAt I z) p.2)) =
    (fun p => deriv (g p.1) p.2) ∘ fun p => (p.1, ↑(extChartAt I z) p.2)
⊢ ContinuousAt ((fun p => deriv (g p.1) p.2) ∘ fun p => (p.1, ↑(extChartAt I z) p.2)) (c, z)
Tactic:
exact fa.inChart.deriv2.continuousAt.comp_of_eq
  (continuousAt_fst.prod ((continuousAt_extChartAt I z).comp_of_eq continuousAt_snd rfl))
  rfl
State after:
no goals

State before:
case refine_2
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)
f0 : mfderiv I I (f c) z ≠ 0
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
⊢ deriv (g (c, z).1) (↑(extChartAt I z) (c, z).2) ≠ 0
Tactic:
contrapose f0
State after:
case refine_2
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)
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
f0 : ¬deriv (g (c, z).1) (↑(extChartAt I z) (c, z).2) ≠ 0
⊢ ¬mfderiv I I (f c) z ≠ 0

State before:
case refine_2
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)
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
f0 : ¬deriv (g (c, z).1) (↑(extChartAt I z) (c, z).2) ≠ 0
⊢ ¬mfderiv I I (f c) z ≠ 0
Tactic:
simp only [not_not, Function.comp] at f0 ⊢
State after:
case refine_2
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)
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
f0 : deriv (g c) (↑(extChartAt I z) z) = 0
⊢ mfderiv I I (f c) z = 0

State before:
case refine_2
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)
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
f0 : deriv (g c) (↑(extChartAt I z) z) = 0
⊢ mfderiv I I (f c) z = 0
Tactic:
rw [g0.self_of_nhds]
State after:
case refine_2
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)
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
f0 : deriv (g c) (↑(extChartAt I z) z) = 0
⊢ deriv (inChart f c z (c, z).1) (↑(extChartAt I z) (c, z).2) = 0

State before:
case refine_2
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)
g : ℂ → ℂ → ℂ := inChart f c z
g0 : ∀ᶠ (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
f0 : deriv (g c) (↑(extChartAt I z) z) = 0
⊢ deriv (inChart f c z (c, z).1) (↑(extChartAt I z) (c, z).2) = 0
Tactic:
exact f0
State after:
no goals