internlm/Lean-Github huggingface dataset:
Theorem: inChart_critical
Proof 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
Proof 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
Theorem: inChart_critical
Proof 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
Proof 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
Theorem: inChart_critical
Proof 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
Proof 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
Theorem: inChart_critical
Proof 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
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
⊢ ↑(extChartAt I z).symm (↑(extChartAt I z) w) = w
Tactic:
exact PartialEquiv.left_inv _ m
Proof state after:
no goals
Theorem: inChart_critical
Proof 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]
Proof state after:
no goals
Theorem: mfderiv_ne_zero_eventually'
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)
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
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)
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
Theorem: mfderiv_ne_zero_eventually'
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)
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
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)
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
Theorem: mfderiv_ne_zero_eventually'
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)
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 ↦ ?_))
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)
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
Theorem: mfderiv_ne_zero_eventually'
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)
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]
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)
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
Theorem: mfderiv_ne_zero_eventually'
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)
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
Proof state after:
no goals
Theorem: mfderiv_ne_zero_eventually'
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)
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 ?_ ?_
Proof 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
Theorem: mfderiv_ne_zero_eventually'
Proof 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
Proof 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)
Theorem: mfderiv_ne_zero_eventually'
Proof 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]
Proof 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)
Theorem: mfderiv_ne_zero_eventually'
Proof 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
Proof state after:
no goals
Theorem: mfderiv_ne_zero_eventually'
Proof 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
Proof 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