Theorem: id_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
⊢ mfderiv I I (fun z => z) z ≠ 0
Tactic:
have d : MDifferentiableAt I I (fun z ↦ z) z := mdifferentiableAt_id I
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

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

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
⊢ fderiv ℂ (fun x => ↑(extChartAt I z) (↑(extChartAt I z).symm x)) (↑(extChartAt I z) z) ≠ 0
Tactic:
have e : (fun w ↦ extChartAt I z ((extChartAt I z).symm w)) =ᶠ[𝓝 (extChartAt I z z)] id := by
  apply ((isOpen_extChartAt_target I z).eventually_mem (mem_extChartAt_target I z)).mp
  refine eventually_of_forall fun w m ↦ ?_
  simp only [id, PartialEquiv.right_inv _ m]
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
e : (𝓝 (↑(extChartAt I z) z)).EventuallyEq (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) id
⊢ fderiv ℂ (fun x => ↑(extChartAt I z) (↑(extChartAt I z).symm x)) (↑(extChartAt I z) z) ≠ 0

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
e : (𝓝 (↑(extChartAt I z) z)).EventuallyEq (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) id
⊢ fderiv ℂ (fun x => ↑(extChartAt I z) (↑(extChartAt I z).symm x)) (↑(extChartAt I z) z) ≠ 0
Tactic:
simp only [e.fderiv_eq, fderiv_id, Ne, ContinuousLinearMap.ext_iff, not_forall,
  ContinuousLinearMap.zero_apply, ContinuousLinearMap.id_apply]
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
e : (𝓝 (↑(extChartAt I z) z)).EventuallyEq (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) id
⊢ ∃ x, ¬x = 0 x

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
e : (𝓝 (↑(extChartAt I z) z)).EventuallyEq (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) id
⊢ ∃ x, ¬x = 0 x
Tactic:
use 1, one_ne_zero
State after:
no goals

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
⊢ (𝓝 (↑(extChartAt I z) z)).EventuallyEq (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) id
Tactic:
apply ((isOpen_extChartAt_target I z).eventually_mem (mem_extChartAt_target I z)).mp
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
⊢ ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I z) z),
    x ∈ (extChartAt I z).target → (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) x = id x

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
⊢ ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I z) z),
    x ∈ (extChartAt I z).target → (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) x = id x
Tactic:
refine eventually_of_forall fun w m ↦ ?_
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
w : ℂ
m : w ∈ (extChartAt I z).target
⊢ (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) w = id w

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
w : ℂ
m : w ∈ (extChartAt I z).target
⊢ (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) w = id w
Tactic:
simp only [id, PartialEquiv.right_inv _ m]
State after:
no goals