Theorem: mderiv_comp_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
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
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

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

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

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