internlm/Lean-Github huggingface dataset:
Theorem: critical_iter
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 → S
n : ℕ
z : S
fa : Holomorphic I I f
c : Critical f^[n] z
⊢ Precritical f z
Tactic:
induction' n with n h
Proof state after:
case zero
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 → S
z : S
fa : Holomorphic I I f
c : Critical f^[0] z
⊢ Precritical f z

case succ
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 → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : Critical f^[n + 1] z
⊢ Precritical f z
Theorem: critical_iter
Proof state before:
case zero
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 → S
z : S
fa : Holomorphic I I f
c : Critical f^[0] z
⊢ Precritical f z
Tactic:
rw [Function.iterate_zero, Critical, mfderiv_id, ← ContinuousLinearMap.opNorm_zero_iff,
  ContinuousLinearMap.norm_id] at c
Proof state after:
case zero
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 → S
z : S
fa : Holomorphic I I f
c : 1 = 0
⊢ Precritical f z
Theorem: critical_iter
Proof state before:
case zero
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 → S
z : S
fa : Holomorphic I I f
c : 1 = 0
⊢ Precritical f z
Tactic:
norm_num at c
Proof state after:
no goals
Theorem: critical_iter
Proof state before:
case succ
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 → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : Critical f^[n + 1] z
⊢ Precritical f z
Tactic:
rw [Function.iterate_succ', Critical,
  mfderiv_comp z (fa _).mdifferentiableAt (fa.iter _ _).mdifferentiableAt,
  mderiv_comp_eq_zero_iff] at c
Proof state after:
case succ
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 → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f (f^[n] z) = 0 ∨ mfderiv I I f^[n] z = 0
⊢ Precritical f z
Theorem: critical_iter
Proof state before:
case succ
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 → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f (f^[n] z) = 0 ∨ mfderiv I I f^[n] z = 0
⊢ Precritical f z
Tactic:
cases' c with c c
Proof state after:
case succ.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 → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f (f^[n] z) = 0
⊢ Precritical f z

case succ.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 → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f^[n] z = 0
⊢ Precritical f z
Theorem: critical_iter
Proof state before:
case succ.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 → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f (f^[n] z) = 0
⊢ Precritical f z

case succ.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 → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f^[n] z = 0
⊢ Precritical f z
Tactic:
use n, c
Proof state after:
case succ.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 → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f^[n] z = 0
⊢ Precritical f z
Theorem: critical_iter
Proof state before:
case succ.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 → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f^[n] z = 0
⊢ Precritical f z
Tactic:
exact h c
Proof state after:
no goals
Theorem: HolomorphicAt.inChart
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)
⊢ AnalyticAt ℂ (uncurry (_root_.inChart f c z)) (c, ↑(_root_.extChartAt I z) z)
Tactic:
apply HolomorphicAt.analyticAt II I
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)
⊢ HolomorphicAt (I.prod I) I (uncurry (_root_.inChart f c z)) (c, ↑(_root_.extChartAt I z) z)
Theorem: HolomorphicAt.inChart
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)
⊢ HolomorphicAt (I.prod I) I (uncurry (_root_.inChart f c z)) (c, ↑(_root_.extChartAt I z) z)
Tactic:
apply (HolomorphicAt.extChartAt (mem_extChartAt_source I (f c z))).comp_of_eq
Proof state after:
case gh
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)
⊢ HolomorphicAt (I.prod I) I (fun x => f x.1 (↑(_root_.extChartAt I z).symm x.2)) (c, ↑(_root_.extChartAt I z) z)

case e
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)
⊢ f (c, ↑(_root_.extChartAt I z) z).1 (↑(_root_.extChartAt I z).symm (c, ↑(_root_.extChartAt I z) z).2) = f c z
Theorem: HolomorphicAt.inChart
Proof state before:
case gh
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)
⊢ HolomorphicAt (I.prod I) I (fun x => f x.1 (↑(_root_.extChartAt I z).symm x.2)) (c, ↑(_root_.extChartAt I z) z)

case e
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)
⊢ f (c, ↑(_root_.extChartAt I z) z).1 (↑(_root_.extChartAt I z).symm (c, ↑(_root_.extChartAt I z) z).2) = f c z
Tactic:
apply fa.comp₂_of_eq holomorphicAt_fst
Proof state after:
case gh.ga
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)
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(_root_.extChartAt I z).symm x.2) (c, ↑(_root_.extChartAt I z) z)

case gh.e
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)
⊢ ((c, ↑(_root_.extChartAt I z) z).1, ↑(_root_.extChartAt I z).symm (c, ↑(_root_.extChartAt I z) z).2) = (c, z)

case e
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)
⊢ f (c, ↑(_root_.extChartAt I z) z).1 (↑(_root_.extChartAt I z).symm (c, ↑(_root_.extChartAt I z) z).2) = f c z
Theorem: HolomorphicAt.inChart
Proof state before:
case gh.ga
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)
⊢ HolomorphicAt (I.prod I) I (fun x => ↑(_root_.extChartAt I z).symm x.2) (c, ↑(_root_.extChartAt I z) z)

case gh.e
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)
⊢ ((c, ↑(_root_.extChartAt I z) z).1, ↑(_root_.extChartAt I z).symm (c, ↑(_root_.extChartAt I z) z).2) = (c, z)

case e
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)
⊢ f (c, ↑(_root_.extChartAt I z) z).1 (↑(_root_.extChartAt I z).symm (c, ↑(_root_.extChartAt I z) z).2) = f c z
Tactic:
apply (HolomorphicAt.extChartAt_symm (mem_extChartAt_target I z)).comp_of_eq holomorphicAt_snd
Proof state after:
case gh.ga
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)
⊢ (c, ↑(_root_.extChartAt I z) z).2 = ↑(_root_.extChartAt I z) z

case gh.e
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)
⊢ ((c, ↑(_root_.extChartAt I z) z).1, ↑(_root_.extChartAt I z).symm (c, ↑(_root_.extChartAt I z) z).2) = (c, z)

case e
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)
⊢ f (c, ↑(_root_.extChartAt I z) z).1 (↑(_root_.extChartAt I z).symm (c, ↑(_root_.extChartAt I z) z).2) = f c z
Theorem: HolomorphicAt.inChart
Proof state before:
case gh.ga
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)
⊢ (c, ↑(_root_.extChartAt I z) z).2 = ↑(_root_.extChartAt I z) z

case gh.e
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)
⊢ ((c, ↑(_root_.extChartAt I z) z).1, ↑(_root_.extChartAt I z).symm (c, ↑(_root_.extChartAt I z) z).2) = (c, z)

case e
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)
⊢ f (c, ↑(_root_.extChartAt I z) z).1 (↑(_root_.extChartAt I z).symm (c, ↑(_root_.extChartAt I z) z).2) = f c z
Tactic:
repeat' simp only [PartialEquiv.left_inv _ (mem_extChartAt_source I z)]
Proof state after:
no goals
Theorem: HolomorphicAt.inChart
Proof state before:
case e
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)
⊢ f (c, ↑(_root_.extChartAt I z) z).1 (↑(_root_.extChartAt I z).symm (c, ↑(_root_.extChartAt I z) z).2) = f c z
Tactic:
simp only [PartialEquiv.left_inv _ (mem_extChartAt_source I z)]
Proof state after:
no goals
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)
⊢ ∀ᶠ (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
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)
⊢ ∀ᶠ (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)
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)
⊢ ∀ᶠ (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
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)
⊢ ∀ᶠ (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)
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)
⊢ ∀ᶠ (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 ?_)
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)
⊢ ∀ (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)
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)
⊢ ∀ (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
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)
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
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)
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
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 : 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
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 : 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
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
⊢ 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