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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
⊢ f ≠ 0 → g ≠ 0 → f.comp g ≠ 0
Tactic:
intro f0 g0
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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
f0 : f ≠ 0
g0 : g ≠ 0
⊢ f.comp g ≠ 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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
f0 : f ≠ 0
g0 : g ≠ 0
⊢ f.comp g ≠ 0
Tactic:
simp only [Ne, mderiv_comp_eq_zero_iff, f0, g0, or_self_iff, not_false_iff]
State after:
no goals