internlm/Lean-Github huggingface dataset:
Theorem: id_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
z : S
d : MDifferentiableAt I I (fun z => z) z
⊢ fderiv ℂ (fun x => ↑(extChartAt I z) (↑(extChartAt I z).symm x)) (↑(extChartAt I z) z) ≠ 0
Tactic:
have e : (fun w ↦ extChartAt I z ((extChartAt I z).symm w)) =ᶠ[𝓝 (extChartAt I z z)] id := by
  apply ((isOpen_extChartAt_target I z).eventually_mem (mem_extChartAt_target I z)).mp
  refine eventually_of_forall fun w m ↦ ?_
  simp only [id, PartialEquiv.right_inv _ m]
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
d : MDifferentiableAt I I (fun z => z) z
e : (𝓝 (↑(extChartAt I z) z)).EventuallyEq (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) id
⊢ fderiv ℂ (fun x => ↑(extChartAt I z) (↑(extChartAt I z).symm x)) (↑(extChartAt I z) z) ≠ 0
Theorem: id_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
z : S
d : MDifferentiableAt I I (fun z => z) z
e : (𝓝 (↑(extChartAt I z) z)).EventuallyEq (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) id
⊢ fderiv ℂ (fun x => ↑(extChartAt I z) (↑(extChartAt I z).symm x)) (↑(extChartAt I z) z) ≠ 0
Tactic:
simp only [e.fderiv_eq, fderiv_id, Ne, ContinuousLinearMap.ext_iff, not_forall,
  ContinuousLinearMap.zero_apply, ContinuousLinearMap.id_apply]
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
d : MDifferentiableAt I I (fun z => z) z
e : (𝓝 (↑(extChartAt I z) z)).EventuallyEq (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) id
⊢ ∃ x, ¬x = 0 x
Theorem: id_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
z : S
d : MDifferentiableAt I I (fun z => z) z
e : (𝓝 (↑(extChartAt I z) z)).EventuallyEq (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) id
⊢ ∃ x, ¬x = 0 x
Tactic:
use 1, one_ne_zero
Proof state after:
no goals
Theorem: id_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
z : S
d : MDifferentiableAt I I (fun z => z) z
⊢ (𝓝 (↑(extChartAt I z) z)).EventuallyEq (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) id
Tactic:
apply ((isOpen_extChartAt_target I z).eventually_mem (mem_extChartAt_target I z)).mp
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
d : MDifferentiableAt I I (fun z => z) z
⊢ ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I z) z),
    x ∈ (extChartAt I z).target → (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) x = id x
Theorem: id_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
z : S
d : MDifferentiableAt I I (fun z => z) z
⊢ ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I z) z),
    x ∈ (extChartAt I z).target → (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) x = id x
Tactic:
refine eventually_of_forall fun w m ↦ ?_
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
d : MDifferentiableAt I I (fun z => z) z
w : ℂ
m : w ∈ (extChartAt I z).target
⊢ (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) w = id w
Theorem: id_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
z : S
d : MDifferentiableAt I I (fun z => z) z
w : ℂ
m : w ∈ (extChartAt I z).target
⊢ (fun w => ↑(extChartAt I z) (↑(extChartAt I z).symm w)) w = id w
Tactic:
simp only [id, PartialEquiv.right_inv _ m]
Proof state after:
no goals
Theorem: mfderiv_eq_zero_iff_deriv_eq_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 : ℂ → ℂ
z : ℂ
⊢ mfderiv I I f z = 0 ↔ deriv f z = 0
Tactic:
by_cases d : DifferentiableAt ℂ f z
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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
⊢ mfderiv I I f z = 0 ↔ deriv f z = 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
f : ℂ → ℂ
z : ℂ
d : ¬DifferentiableAt ℂ f z
⊢ mfderiv I I f z = 0 ↔ deriv f z = 0
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
⊢ mfderiv I I f z = 0 ↔ deriv f z = 0
Tactic:
constructor
Proof state after:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
⊢ mfderiv I I f z = 0 → deriv f z = 0

case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
⊢ deriv f z = 0 → mfderiv I I f z = 0
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
Proof state before:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
⊢ mfderiv I I f z = 0 → deriv f z = 0
Tactic:
have h := d.mdifferentiableAt.hasMFDerivAt
Proof state after:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasMFDerivAt I I f z (mfderiv I I f z)
⊢ mfderiv I I f z = 0 → deriv f z = 0
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
Proof state before:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasMFDerivAt I I f z (mfderiv I I f z)
⊢ mfderiv I I f z = 0 → deriv f z = 0
Tactic:
intro e
Proof state after:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasMFDerivAt I I f z (mfderiv I I f z)
e : mfderiv I I f z = 0
⊢ deriv f z = 0
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
Proof state before:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasMFDerivAt I I f z (mfderiv I I f z)
e : mfderiv I I f z = 0
⊢ deriv f z = 0
Tactic:
rw [e] at h
Proof state after:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasMFDerivAt I I f z 0
e : mfderiv I I f z = 0
⊢ deriv f z = 0
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
Proof state before:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasMFDerivAt I I f z 0
e : mfderiv I I f z = 0
⊢ deriv f z = 0
Tactic:
have p := h.hasFDerivAt.hasDerivAt
Proof state after:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasMFDerivAt I I f z 0
e : mfderiv I I f z = 0
p : HasDerivAt f (0 1) z
⊢ deriv f z = 0
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
Proof state before:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasMFDerivAt I I f z 0
e : mfderiv I I f z = 0
p : HasDerivAt f (0 1) z
⊢ deriv f z = 0
Tactic:
exact p.deriv
Proof state after:
no goals
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
Proof state before:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
⊢ deriv f z = 0 → mfderiv I I f z = 0
Tactic:
have h := d.hasDerivAt
Proof state after:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f (deriv f z) z
⊢ deriv f z = 0 → mfderiv I I f z = 0
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
Proof state before:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f (deriv f z) z
⊢ deriv f z = 0 → mfderiv I I f z = 0
Tactic:
intro e
Proof state after:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f (deriv f z) z
e : deriv f z = 0
⊢ mfderiv I I f z = 0
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
Proof state before:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f (deriv f z) z
e : deriv f z = 0
⊢ mfderiv I I f z = 0
Tactic:
rw [e] at h
Proof state after:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f 0 z
e : deriv f z = 0
⊢ mfderiv I I f z = 0
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
Proof state before:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f 0 z
e : deriv f z = 0
⊢ mfderiv I I f z = 0
Tactic:
have s0 : (1 : ℂ →L[ℂ] ℂ).smulRight (0 : ℂ) = 0 := by
  apply ContinuousLinearMap.ext
  simp only [ContinuousLinearMap.smulRight_apply, Algebra.id.smul_eq_mul,
    MulZeroClass.mul_zero, ContinuousLinearMap.zero_apply, forall_const]
Proof state after:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f 0 z
e : deriv f z = 0
s0 : ContinuousLinearMap.smulRight 1 0 = 0
⊢ mfderiv I I f z = 0
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
Proof state before:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f 0 z
e : deriv f z = 0
s0 : ContinuousLinearMap.smulRight 1 0 = 0
⊢ mfderiv I I f z = 0
Tactic:
have p := h.hasFDerivAt.hasMFDerivAt
Proof state after:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f 0 z
e : deriv f z = 0
s0 : ContinuousLinearMap.smulRight 1 0 = 0
p : HasMFDerivAt I I f z (ContinuousLinearMap.smulRight 1 0)
⊢ mfderiv I I f z = 0
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
Proof state before:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f 0 z
e : deriv f z = 0
s0 : ContinuousLinearMap.smulRight 1 0 = 0
p : HasMFDerivAt I I f z (ContinuousLinearMap.smulRight 1 0)
⊢ mfderiv I I f z = 0
Tactic:
rw [s0] at p
Proof state after:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f 0 z
e : deriv f z = 0
s0 : ContinuousLinearMap.smulRight 1 0 = 0
p : HasMFDerivAt I I f z 0
⊢ mfderiv I I f z = 0
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
Proof state before:
case pos.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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f 0 z
e : deriv f z = 0
s0 : ContinuousLinearMap.smulRight 1 0 = 0
p : HasMFDerivAt I I f z 0
⊢ mfderiv I I f z = 0
Tactic:
exact p.mfderiv
Proof state after:
no goals
Theorem: mfderiv_eq_zero_iff_deriv_eq_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 : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f 0 z
e : deriv f z = 0
⊢ ContinuousLinearMap.smulRight 1 0 = 0
Tactic:
apply ContinuousLinearMap.ext
Proof state after:
case 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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f 0 z
e : deriv f z = 0
⊢ ∀ (x : ℂ), (ContinuousLinearMap.smulRight 1 0) x = 0 x
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
Proof state before:
case 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
f : ℂ → ℂ
z : ℂ
d : DifferentiableAt ℂ f z
h : HasDerivAt f 0 z
e : deriv f z = 0
⊢ ∀ (x : ℂ), (ContinuousLinearMap.smulRight 1 0) x = 0 x
Tactic:
simp only [ContinuousLinearMap.smulRight_apply, Algebra.id.smul_eq_mul,
  MulZeroClass.mul_zero, ContinuousLinearMap.zero_apply, forall_const]
Proof state after:
no goals
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
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
f : ℂ → ℂ
z : ℂ
d : ¬DifferentiableAt ℂ f z
⊢ mfderiv I I f z = 0 ↔ deriv f z = 0
Tactic:
have d' : ¬MDifferentiableAt I I f z := by
  contrapose d; simp only [not_not] at d ⊢; exact d.differentiableAt
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
f : ℂ → ℂ
z : ℂ
d : ¬DifferentiableAt ℂ f z
d' : ¬MDifferentiableAt I I f z
⊢ mfderiv I I f z = 0 ↔ deriv f z = 0
Theorem: mfderiv_eq_zero_iff_deriv_eq_zero
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
f : ℂ → ℂ
z : ℂ
d : ¬DifferentiableAt ℂ f z
d' : ¬MDifferentiableAt I I f z
⊢ mfderiv I I f z = 0 ↔ deriv f z = 0
Tactic:
simp only [deriv_zero_of_not_differentiableAt d, mfderiv_zero_of_not_mdifferentiableAt d',
  eq_self_iff_true]
Proof state after:
no goals
Theorem: mfderiv_eq_zero_iff_deriv_eq_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 : ℂ → ℂ
z : ℂ
d : ¬DifferentiableAt ℂ f z
⊢ ¬MDifferentiableAt I I f z
Tactic:
contrapose d
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 : ℂ → ℂ
z : ℂ
d : ¬¬MDifferentiableAt I I f z
⊢ ¬¬DifferentiableAt ℂ f z
Theorem: mfderiv_eq_zero_iff_deriv_eq_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 : ℂ → ℂ
z : ℂ
d : ¬¬MDifferentiableAt I I f z
⊢ ¬¬DifferentiableAt ℂ f z
Tactic:
simp only [not_not] at d ⊢
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 : ℂ → ℂ
z : ℂ
d : MDifferentiableAt I I f z
⊢ DifferentiableAt ℂ f z
Theorem: mfderiv_eq_zero_iff_deriv_eq_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 : ℂ → ℂ
z : ℂ
d : MDifferentiableAt I I f z
⊢ DifferentiableAt ℂ f z
Tactic:
exact d.differentiableAt
Proof state after:
no goals
Theorem: mfderiv_ne_zero_iff_deriv_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 : ℂ → ℂ
z : ℂ
⊢ mfderiv I I f z ≠ 0 ↔ deriv f z ≠ 0
Tactic:
rw [not_iff_not, mfderiv_eq_zero_iff_deriv_eq_zero]
Proof state after:
no goals