Theorem: extChartAt_symm_mderiv_ne_zero' (Ray/AnalyticManifold/OneDimension.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
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⟩
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

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]
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

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
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

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 ⊢
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

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
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

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
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

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]
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

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
State after:
no goals