Theorem: mfderiv_eq_zero_iff_deriv_eq_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
f : ℂ → ℂ
z : ℂ
⊢ mfderiv I I f z = 0 ↔ deriv f z = 0
Tactic:
by_cases d : DifferentiableAt ℂ f z
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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]
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

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
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

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
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

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
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
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
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

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]
State after:
no goals

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
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

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]
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
f : ℂ → ℂ
z : ℂ
d : ¬DifferentiableAt ℂ f z
⊢ ¬MDifferentiableAt I I f z
Tactic:
contrapose d
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

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 ⊢
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

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
State after:
no goals