Theorem: mderiv_eq_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
⊢ f u = 0 ↔ f = 0 ∨ u = 0
Tactic:
constructor
State after:
case mp
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
⊢ f u = 0 → f = 0 ∨ u = 0

case mpr
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
⊢ f = 0 ∨ u = 0 → f u = 0

State before:
case mp
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
⊢ f u = 0 → f = 0 ∨ u = 0
Tactic:
rw [or_iff_not_imp_right]
State after:
case mp
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
⊢ f u = 0 → ¬u = 0 → f = 0

State before:
case mp
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
⊢ f u = 0 → ¬u = 0 → f = 0
Tactic:
intro f0 u0
State after:
case mp
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
f0 : f u = 0
u0 : ¬u = 0
⊢ f = 0

State before:
case mp
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
f0 : f u = 0
u0 : ¬u = 0
⊢ f = 0
Tactic:
apply ContinuousLinearMap.ext
State after:
case mp.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 : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
f0 : f u = 0
u0 : ¬u = 0
⊢ ∀ (x : TangentSpace I z), f x = 0 x

State before:
case mp.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 : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
f0 : f u = 0
u0 : ¬u = 0
⊢ ∀ (x : TangentSpace I z), f x = 0 x
Tactic:
intro v
State after:
case mp.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 : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
f0 : f u = 0
u0 : ¬u = 0
v : TangentSpace I z
⊢ f v = 0 v

State before:
case mp.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 : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
f0 : f u = 0
u0 : ¬u = 0
v : TangentSpace I z
⊢ f v = 0 v
Tactic:
simp only [TangentSpace] at f u v u0
State after:
case mp.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 : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
⊢ f v = 0 v

State before:
case mp.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 : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
⊢ f v = 0 v
Tactic:
have e : v = (v * u⁻¹) • u := by simp only [smul_eq_mul, mul_assoc, inv_mul_cancel u0, mul_one]
State after:
case mp.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 : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ f v = 0 v

State before:
case mp.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 : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ f v = 0 v
Tactic:
rw [ContinuousLinearMap.zero_apply, e]
State after:
case mp.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 : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ f ((v * u⁻¹) • u) = 0

State before:
case mp.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 : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ f ((v * u⁻¹) • u) = 0
Tactic:
refine Eq.trans (f.map_smul _ _) ?_
State after:
case mp.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 : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ (v * u⁻¹) • f u = 0

State before:
case mp.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 : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ (v * u⁻¹) • f u = 0
Tactic:
rw [smul_eq_zero]
State after:
case mp.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 : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ v * u⁻¹ = 0 ∨ f u = 0

State before:
case mp.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 : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ v * u⁻¹ = 0 ∨ f u = 0
Tactic:
right
State after:
case mp.h.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 : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ f u = 0

State before:
case mp.h.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 : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
e : v = (v * u⁻¹) • u
⊢ f u = 0
Tactic:
exact f0
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
w : T
f : ℂ →L[ℂ] ℂ
u : ℂ
f0 : f u = 0
u0 : ¬u = 0
v : ℂ
⊢ v = (v * u⁻¹) • u
Tactic:
simp only [smul_eq_mul, mul_assoc, inv_mul_cancel u0, mul_one]
State after:
no goals

State before:
case mpr
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
⊢ f = 0 ∨ u = 0 → f u = 0
Tactic:
intro h
State after:
case mpr
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
h : f = 0 ∨ u = 0
⊢ f u = 0

State before:
case mpr
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
h : f = 0 ∨ u = 0
⊢ f u = 0
Tactic:
cases' h with h h
State after:
case mpr.inl
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
h : f = 0
⊢ f u = 0

case mpr.inr
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
h : u = 0
⊢ f u = 0

State before:
case mpr.inl
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
h : f = 0
⊢ f u = 0

case mpr.inr
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
h : u = 0
⊢ f u = 0
Tactic:
simp only [h, ContinuousLinearMap.zero_apply]
State after:
case mpr.inr
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
h : u = 0
⊢ f u = 0

State before:
case mpr.inr
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
h : u = 0
⊢ f u = 0
Tactic:
simp only [h, ContinuousLinearMap.map_zero]
State after:
no goals