internlm/Lean-Github huggingface dataset:
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
⊢ 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
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
⊢ 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 : 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]
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
⊢ mfderiv I I (f e) w = 0 ↔ mfderiv I I (inChart f c z e) (↑(extChartAt I z) w) = 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 : 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
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)
⊢ mfderiv I I (f e) w = 0 ↔ mfderiv I I (inChart f c z e) (↑(extChartAt I z) w) = 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 : 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)
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)
⊢ mfderiv I I (f e) w = 0 ↔ mfderiv I I (inChart f c z e) (↑(extChartAt I z) w) = 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 : 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
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 (inChart f c z e) (↑(extChartAt I z) w) = 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 : 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]
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)
⊢ HolomorphicAt I I (fun x => f e (↑(extChartAt I z).symm x)) (↑(extChartAt I z) w)
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)
⊢ 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)
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)
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]
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))) = 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
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 (↑(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]
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 w) = 0 ∨
      mfderiv I I (fun y => f e y) w = 0 ∨ mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 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 : 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]
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 (fun y => f e y) w = 0 ∨ mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w) = 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 : 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
Proof 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
Theorem: inChart_critical
Proof 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
Proof 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
Theorem: inChart_critical
Proof 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
Proof 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
Theorem: inChart_critical
Proof 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
Proof state after:
no goals