internlm/Lean-Github huggingface dataset:
Theorem: mderiv_comp_ne_zero'
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 : T → U
g : S → T
x : S
⊢ mfderiv I I f (g x) ≠ 0 → mfderiv I I g x ≠ 0 → mfderiv I I (fun x => f (g x)) x ≠ 0
Tactic:
intro df dg
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 : T → U
g : S → T
x : S
df : mfderiv I I f (g x) ≠ 0
dg : mfderiv I I g x ≠ 0
⊢ mfderiv I I (fun x => f (g x)) x ≠ 0
Theorem: mderiv_comp_ne_zero'
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 : T → U
g : S → T
x : S
df : mfderiv I I f (g x) ≠ 0
dg : mfderiv I I g x ≠ 0
⊢ mfderiv I I (fun x => f (g x)) x ≠ 0
Tactic:
have e : (fun x ↦ f (g x)) = f ∘ g := 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 : T → U
g : S → T
x : S
df : mfderiv I I f (g x) ≠ 0
dg : mfderiv I I g x ≠ 0
e : (fun x => f (g x)) = f ∘ g
⊢ mfderiv I I (fun x => f (g x)) x ≠ 0
Theorem: mderiv_comp_ne_zero'
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 : T → U
g : S → T
x : S
df : mfderiv I I f (g x) ≠ 0
dg : mfderiv I I g x ≠ 0
e : (fun x => f (g x)) = f ∘ g
⊢ mfderiv I I (fun x => f (g x)) x ≠ 0
Tactic:
rw [e, mfderiv_comp x (has_mfderiv_at_of_mderiv_ne_zero df) (has_mfderiv_at_of_mderiv_ne_zero dg)]
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 : T → U
g : S → T
x : S
df : mfderiv I I f (g x) ≠ 0
dg : mfderiv I I g x ≠ 0
e : (fun x => f (g x)) = f ∘ g
⊢ (mfderiv I I f (g x)).comp (mfderiv I I g x) ≠ 0
Theorem: mderiv_comp_ne_zero'
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 : T → U
g : S → T
x : S
df : mfderiv I I f (g x) ≠ 0
dg : mfderiv I I g x ≠ 0
e : (fun x => f (g x)) = f ∘ g
⊢ (mfderiv I I f (g x)).comp (mfderiv I I g x) ≠ 0
Tactic:
exact mderiv_comp_ne_zero _ _ df dg
Proof state after:
no goals
Theorem: mderivEquiv_eq
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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
f0 : f ≠ 0
⊢ ↑(mderivEquiv f f0) = f
Tactic:
apply ContinuousLinearMap.ext
Proof state after:
case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
f0 : f ≠ 0
⊢ ∀ (x : TangentSpace I z), ↑(mderivEquiv f f0) x = f x
Theorem: mderivEquiv_eq
Proof state before:
case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
f0 : f ≠ 0
⊢ ∀ (x : TangentSpace I z), ↑(mderivEquiv f f0) x = f x
Tactic:
intro x
Proof state after:
case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
f0 : f ≠ 0
x : TangentSpace I z
⊢ ↑(mderivEquiv f f0) x = f x
Theorem: mderivEquiv_eq
Proof state before:
case 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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
f0 : f ≠ 0
x : TangentSpace I z
⊢ ↑(mderivEquiv f f0) x = f x
Tactic:
rfl
Proof state after:
no goals
Theorem: extChartAt_mderiv_ne_zero'
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
z w : S
m : w ∈ (extChartAt I z).source
⊢ mfderiv I I (↑(extChartAt I z)) w ≠ 0
Tactic:
rcases exists_ne (0 : TangentSpace I z) with ⟨t, t0⟩
Proof state after:
case intro
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
z w : S
m : w ∈ (extChartAt I z).source
t : TangentSpace I z
t0 : t ≠ 0
⊢ mfderiv I I (↑(extChartAt I z)) w ≠ 0
Theorem: extChartAt_mderiv_ne_zero'
Proof state before:
case intro
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
z w : S
m : w ∈ (extChartAt I z).source
t : TangentSpace I z
t0 : t ≠ 0
⊢ mfderiv I I (↑(extChartAt I z)) w ≠ 0
Tactic:
rw [← mderiv_ne_zero_iff' t0]
Proof state after:
case intro
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
z w : S
m : w ∈ (extChartAt I z).source
t : TangentSpace I z
t0 : t ≠ 0
⊢ (mfderiv I I (↑(extChartAt I z)) w) t ≠ 0
Theorem: extChartAt_mderiv_ne_zero'
Proof state before:
case intro
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
z w : S
m : w ∈ (extChartAt I z).source
t : TangentSpace I z
t0 : t ≠ 0
⊢ (mfderiv I I (↑(extChartAt I z)) w) t ≠ 0
Tactic:
contrapose t0
Proof state after:
case intro
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
z w : S
m : w ∈ (extChartAt I z).source
t : TangentSpace I z
t0 : ¬(mfderiv I I (↑(extChartAt I z)) w) t ≠ 0
⊢ ¬t ≠ 0
Theorem: extChartAt_mderiv_ne_zero'
Proof state before:
case intro
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
z w : S
m : w ∈ (extChartAt I z).source
t : TangentSpace I z
t0 : ¬(mfderiv I I (↑(extChartAt I z)) w) t ≠ 0
⊢ ¬t ≠ 0
Tactic:
simp only [not_not] at t0 ⊢
Proof state after:
case intro
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
z w : S
m : w ∈ (extChartAt I z).source
t : TangentSpace I z
t0 : (mfderiv I I (↑(extChartAt I z)) w) t = 0
⊢ t = 0
Theorem: extChartAt_mderiv_ne_zero'
Proof state before:
case intro
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
z w : S
m : w ∈ (extChartAt I z).source
t : TangentSpace I z
t0 : (mfderiv I I (↑(extChartAt I z)) w) t = 0
⊢ t = 0
Tactic:
have h := ContinuousLinearMap.ext_iff.mp (extChartAt_mderiv_left_inverse m) t
Proof state after:
case intro
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
z w : S
m : w ∈ (extChartAt I z).source
t : TangentSpace I z
t0 : (mfderiv I I (↑(extChartAt I z)) w) t = 0
h :
  ((mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w)).comp (mfderiv I I (↑(extChartAt I z)) w)) t =
    (ContinuousLinearMap.id ℂ (TangentSpace I w)) t
⊢ t = 0
Theorem: extChartAt_mderiv_ne_zero'
Proof state before:
case intro
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
z w : S
m : w ∈ (extChartAt I z).source
t : TangentSpace I z
t0 : (mfderiv I I (↑(extChartAt I z)) w) t = 0
h :
  ((mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w)).comp (mfderiv I I (↑(extChartAt I z)) w)) t =
    (ContinuousLinearMap.id ℂ (TangentSpace I w)) t
⊢ t = 0
Tactic:
simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.map_zero] at h
Proof state after:
case intro
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
z w : S
m : w ∈ (extChartAt I z).source
t : TangentSpace I z
t0 : (mfderiv I I (↑(extChartAt I z)) w) t = 0
h :
  (mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w)) ((mfderiv I I (↑(extChartAt I z)) w) t) =
    (ContinuousLinearMap.id ℂ (TangentSpace I w)) t
⊢ t = 0
Theorem: extChartAt_mderiv_ne_zero'
Proof state before:
case intro
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
z w : S
m : w ∈ (extChartAt I z).source
t : TangentSpace I z
t0 : (mfderiv I I (↑(extChartAt I z)) w) t = 0
h :
  (mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w)) ((mfderiv I I (↑(extChartAt I z)) w) t) =
    (ContinuousLinearMap.id ℂ (TangentSpace I w)) t
⊢ t = 0
Tactic:
rw [←h.trans (ContinuousLinearMap.id_apply _), ContinuousLinearMap.apply_eq_zero_of_eq_zero]
Proof state after:
case intro.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
z w : S
m : w ∈ (extChartAt I z).source
t : TangentSpace I z
t0 : (mfderiv I I (↑(extChartAt I z)) w) t = 0
h :
  (mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w)) ((mfderiv I I (↑(extChartAt I z)) w) t) =
    (ContinuousLinearMap.id ℂ (TangentSpace I w)) t
⊢ (mfderiv I I (↑(extChartAt I z)) w) t = 0
Theorem: extChartAt_mderiv_ne_zero'
Proof state before:
case intro.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
z w : S
m : w ∈ (extChartAt I z).source
t : TangentSpace I z
t0 : (mfderiv I I (↑(extChartAt I z)) w) t = 0
h :
  (mfderiv I I (↑(extChartAt I z).symm) (↑(extChartAt I z) w)) ((mfderiv I I (↑(extChartAt I z)) w) t) =
    (ContinuousLinearMap.id ℂ (TangentSpace I w)) t
⊢ (mfderiv I I (↑(extChartAt I z)) w) t = 0
Tactic:
exact t0
Proof state after:
no goals
Theorem: extChartAt_symm_mderiv_ne_zero'
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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
⊢ mfderiv I I (↑(extChartAt I z).symm) w ≠ 0
Tactic:
rcases exists_ne (0 : TangentSpace I (extChartAt I z z)) with ⟨t, t0⟩
Proof state after:
case intro
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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
t : TangentSpace I (↑(extChartAt I z) z)
t0 : t ≠ 0
⊢ mfderiv I I (↑(extChartAt I z).symm) w ≠ 0
Theorem: extChartAt_symm_mderiv_ne_zero'
Proof state before:
case intro
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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
t : TangentSpace I (↑(extChartAt I z) z)
t0 : t ≠ 0
⊢ mfderiv I I (↑(extChartAt I z).symm) w ≠ 0
Tactic:
rw [← mderiv_ne_zero_iff' t0]
Proof state after:
case intro
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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
t : TangentSpace I (↑(extChartAt I z) z)
t0 : t ≠ 0
⊢ (mfderiv I I (↑(extChartAt I z).symm) w) t ≠ 0
Theorem: extChartAt_symm_mderiv_ne_zero'
Proof state before:
case intro
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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
t : TangentSpace I (↑(extChartAt I z) z)
t0 : t ≠ 0
⊢ (mfderiv I I (↑(extChartAt I z).symm) w) t ≠ 0
Tactic:
contrapose t0
Proof state after:
case intro
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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
t : TangentSpace I (↑(extChartAt I z) z)
t0 : ¬(mfderiv I I (↑(extChartAt I z).symm) w) t ≠ 0
⊢ ¬t ≠ 0
Theorem: extChartAt_symm_mderiv_ne_zero'
Proof state before:
case intro
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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
t : TangentSpace I (↑(extChartAt I z) z)
t0 : ¬(mfderiv I I (↑(extChartAt I z).symm) w) t ≠ 0
⊢ ¬t ≠ 0
Tactic:
simp only [not_not] at t0 ⊢
Proof state after:
case intro
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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
t : TangentSpace I (↑(extChartAt I z) z)
t0 : (mfderiv I I (↑(extChartAt I z).symm) w) t = 0
⊢ t = 0
Theorem: extChartAt_symm_mderiv_ne_zero'
Proof state before:
case intro
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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
t : TangentSpace I (↑(extChartAt I z) z)
t0 : (mfderiv I I (↑(extChartAt I z).symm) w) t = 0
⊢ t = 0
Tactic:
have h := ContinuousLinearMap.ext_iff.mp (extChartAt_mderiv_right_inverse m) t
Proof state after:
case intro
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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
t : TangentSpace I (↑(extChartAt I z) z)
t0 : (mfderiv I I (↑(extChartAt I z).symm) w) t = 0
h :
  ((mfderiv I I (↑(extChartAt I z)) (↑(extChartAt I z).symm w)).comp (mfderiv I I (↑(extChartAt I z).symm) w)) t =
    (ContinuousLinearMap.id ℂ (TangentSpace I w)) t
⊢ t = 0
Theorem: extChartAt_symm_mderiv_ne_zero'
Proof state before:
case intro
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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
t : TangentSpace I (↑(extChartAt I z) z)
t0 : (mfderiv I I (↑(extChartAt I z).symm) w) t = 0
h :
  ((mfderiv I I (↑(extChartAt I z)) (↑(extChartAt I z).symm w)).comp (mfderiv I I (↑(extChartAt I z).symm) w)) t =
    (ContinuousLinearMap.id ℂ (TangentSpace I w)) t
⊢ t = 0
Tactic:
simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.map_zero] at h
Proof state after:
case intro
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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
t : TangentSpace I (↑(extChartAt I z) z)
t0 : (mfderiv I I (↑(extChartAt I z).symm) w) t = 0
h :
  (mfderiv I I (↑(extChartAt I z)) (↑(extChartAt I z).symm w)) ((mfderiv I I (↑(extChartAt I z).symm) w) t) =
    (ContinuousLinearMap.id ℂ (TangentSpace I w)) t
⊢ t = 0
Theorem: extChartAt_symm_mderiv_ne_zero'
Proof state before:
case intro
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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
t : TangentSpace I (↑(extChartAt I z) z)
t0 : (mfderiv I I (↑(extChartAt I z).symm) w) t = 0
h :
  (mfderiv I I (↑(extChartAt I z)) (↑(extChartAt I z).symm w)) ((mfderiv I I (↑(extChartAt I z).symm) w) t) =
    (ContinuousLinearMap.id ℂ (TangentSpace I w)) t
⊢ t = 0
Tactic:
rw [←h.trans (ContinuousLinearMap.id_apply _), ContinuousLinearMap.apply_eq_zero_of_eq_zero]
Proof state after:
case intro.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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
t : TangentSpace I (↑(extChartAt I z) z)
t0 : (mfderiv I I (↑(extChartAt I z).symm) w) t = 0
h :
  (mfderiv I I (↑(extChartAt I z)) (↑(extChartAt I z).symm w)) ((mfderiv I I (↑(extChartAt I z).symm) w) t) =
    (ContinuousLinearMap.id ℂ (TangentSpace I w)) t
⊢ (mfderiv I I (↑(extChartAt I z).symm) w) t = 0
Theorem: extChartAt_symm_mderiv_ne_zero'
Proof state before:
case intro.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
z : S
w : ℂ
m : w ∈ (extChartAt I z).target
t : TangentSpace I (↑(extChartAt I z) z)
t0 : (mfderiv I I (↑(extChartAt I z).symm) w) t = 0
h :
  (mfderiv I I (↑(extChartAt I z)) (↑(extChartAt I z).symm w)) ((mfderiv I I (↑(extChartAt I z).symm) w) t) =
    (ContinuousLinearMap.id ℂ (TangentSpace I w)) t
⊢ (mfderiv I I (↑(extChartAt I z).symm) w) t = 0
Tactic:
exact t0
Proof state after:
no goals
Theorem: id_mderiv_ne_zero
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
z : S
⊢ mfderiv I I (fun z => z) z ≠ 0
Tactic:
have d : MDifferentiableAt I I (fun z ↦ z) z := mdifferentiableAt_id 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
z : S
d : MDifferentiableAt I I (fun z => z) z
⊢ mfderiv I I (fun z => z) z ≠ 0
Theorem: id_mderiv_ne_zero
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
z : S
d : MDifferentiableAt I I (fun z => z) z
⊢ mfderiv I I (fun z => z) z ≠ 0
Tactic:
simp only [mfderiv, d, if_true, writtenInExtChartAt, Function.comp,
  ModelWithCorners.Boundaryless.range_eq_univ, fderivWithin_univ]
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
z : S
d : MDifferentiableAt I I (fun z => z) z
⊢ fderiv ℂ (fun x => ↑(extChartAt I z) (↑(extChartAt I z).symm x)) (↑(extChartAt I z) z) ≠ 0