internlm/Lean-Github huggingface dataset:
Theorem: mderiv_eq_zero_iff
Proof 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]
Proof 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
Theorem: mderiv_eq_zero_iff
Proof 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]
Proof state after:
no goals
Theorem: mderiv_eq_zero_iff'
Proof 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 [mderiv_eq_zero_iff, u0, or_false_iff]
Proof state after:
no goals
Theorem: mderiv_ne_zero_iff
Proof 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:
simp only [← not_or]
Proof 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
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
⊢ f u ≠ 0 ↔ ¬(f = 0 ∨ u = 0)
Theorem: mderiv_ne_zero_iff
Proof 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:
exact Iff.not (mderiv_eq_zero_iff _ _)
Proof state after:
no goals
Theorem: mderiv_ne_zero_iff'
Proof 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]
Proof state after:
no goals
Theorem: mderiv_comp_eq_zero_iff
Proof 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.comp g = 0 ↔ f = 0 ∨ g = 0
Tactic:
rcases exists_ne (0 : TangentSpace I x) with ⟨t, t0⟩
Proof state after:
case intro
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
t : TangentSpace I x
t0 : t ≠ 0
⊢ f.comp g = 0 ↔ f = 0 ∨ g = 0
Theorem: mderiv_comp_eq_zero_iff
Proof state before:
case intro
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
t : TangentSpace I x
t0 : t ≠ 0
⊢ f.comp g = 0 ↔ f = 0 ∨ g = 0
Tactic:
constructor
Proof state after:
case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
⊢ f.comp g = 0 → f = 0 ∨ g = 0

case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
⊢ f = 0 ∨ g = 0 → f.comp g = 0
Theorem: mderiv_comp_eq_zero_iff
Proof state before:
case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
⊢ f.comp g = 0 → f = 0 ∨ g = 0
Tactic:
intro h
Proof state after:
case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f.comp g = 0
⊢ f = 0 ∨ g = 0
Theorem: mderiv_comp_eq_zero_iff
Proof state before:
case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f.comp g = 0
⊢ f = 0 ∨ g = 0
Tactic:
simp only [← mderiv_eq_zero_iff' t0, ContinuousLinearMap.comp_apply] at h
Proof state after:
case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
⊢ f = 0 ∨ g = 0
Theorem: mderiv_comp_eq_zero_iff
Proof state before:
case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
⊢ f = 0 ∨ g = 0
Tactic:
by_cases g0 : g t = 0
Proof state after:
case pos
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
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : g t = 0
⊢ f = 0 ∨ g = 0

case neg
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
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0
Theorem: mderiv_comp_eq_zero_iff
Proof state before:
case pos
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
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : g t = 0
⊢ f = 0 ∨ g = 0

case neg
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
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0
Tactic:
right
Proof state after:
case pos.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : g t = 0
⊢ g = 0

case neg
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
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0
Theorem: mderiv_comp_eq_zero_iff
Proof state before:
case pos.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : g t = 0
⊢ g = 0

case neg
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
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0
Tactic:
rw [mderiv_eq_zero_iff' t0] at g0
Proof state after:
case pos.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : g = 0
⊢ g = 0

case neg
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
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0
Theorem: mderiv_comp_eq_zero_iff
Proof state before:
case pos.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : g = 0
⊢ g = 0

case neg
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
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0
Tactic:
exact g0
Proof state after:
case neg
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
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0
Theorem: mderiv_comp_eq_zero_iff
Proof state before:
case neg
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
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0 ∨ g = 0
Tactic:
left
Proof state after:
case neg.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0
Theorem: mderiv_comp_eq_zero_iff
Proof state before:
case neg.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f (g t) = 0
g0 : ¬g t = 0
⊢ f = 0
Tactic:
rwa [← mderiv_eq_zero_iff' g0]
Proof state after:
no goals
Theorem: mderiv_comp_eq_zero_iff
Proof state before:
case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
⊢ f = 0 ∨ g = 0 → f.comp g = 0
Tactic:
intro h
Proof state after:
case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f = 0 ∨ g = 0
⊢ f.comp g = 0
Theorem: mderiv_comp_eq_zero_iff
Proof state before:
case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f = 0 ∨ g = 0
⊢ f.comp g = 0
Tactic:
cases' h with h h
Proof state after:
case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f = 0
⊢ f.comp g = 0

case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : g = 0
⊢ f.comp g = 0
Theorem: mderiv_comp_eq_zero_iff
Proof state before:
case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : f = 0
⊢ f.comp g = 0

case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : g = 0
⊢ f.comp g = 0
Tactic:
simp only [h, g.zero_comp]
Proof state after:
case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : g = 0
⊢ f.comp g = 0
Theorem: mderiv_comp_eq_zero_iff
Proof state before:
case intro.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
x : S
y : T
z : U
f : TangentSpace I y →L[ℂ] TangentSpace I z
g : TangentSpace I x →L[ℂ] TangentSpace I y
t : TangentSpace I x
t0 : t ≠ 0
h : g = 0
⊢ f.comp g = 0
Tactic:
simp only [h, f.comp_zero]
Proof state after:
no goals
Theorem: mderiv_comp_ne_zero
Proof 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
Proof 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
Theorem: mderiv_comp_ne_zero
Proof 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]
Proof state after:
no goals
Theorem: has_mfderiv_at_of_mderiv_ne_zero
Proof 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 : S → T
x : S
d0 : mfderiv I I f x ≠ 0
⊢ MDifferentiableAt I I f x
Tactic:
contrapose d0
Proof 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 : S → T
x : S
d0 : ¬MDifferentiableAt I I f x
⊢ ¬mfderiv I I f x ≠ 0
Theorem: has_mfderiv_at_of_mderiv_ne_zero
Proof 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 : S → T
x : S
d0 : ¬MDifferentiableAt I I f x
⊢ ¬mfderiv I I f x ≠ 0
Tactic:
simp only [mfderiv, d0, if_false, Ne, eq_self_iff_true, not_true, not_false_iff]
Proof state after:
no goals