Theorem: mderiv_ne_zero_iff' (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 : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
u0 : u ≠ 0
⊢ f u ≠ 0 ↔ f ≠ 0
Tactic:
simp only [ne_eq, mderiv_ne_zero_iff, u0, not_false_eq_true, and_true]
State after:
no goals