-- Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean
theorem mfderivWithin_eq_fderivWithin :
    mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x = fderivWithin 𝕜 f s x

Proof state:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ 0 = fderivWithin 𝕜 f s x

Tactic:
exact (fderivWithin_zero_of_not_differentiableWithinAt h).symm

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
h : MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x
⊢ mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x = fderivWithin 𝕜 f s x

Tactic:
simp only [mfderivWithin, h, if_pos, mfld_simps]

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
h : ¬MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x
⊢ 0 = fderivWithin 𝕜 f s x

Tactic:
rw [mdifferentiableWithinAt_iff_differentiableWithinAt] at h

Result:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ 0 = fderivWithin 𝕜 f s x

Proof state:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
h : ¬MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x
⊢ mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x = fderivWithin 𝕜 f s x

Tactic:
simp only [mfderivWithin, h, if_neg, not_false_iff]

Result:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
h : ¬MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x
⊢ 0 = fderivWithin 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
⊢ mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x = fderivWithin 𝕜 f s x

Tactic:
by_cases h : MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x

Result:
case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
h : MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x
⊢ mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x = fderivWithin 𝕜 f s x

case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
h : ¬MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x
⊢ mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x = fderivWithin 𝕜 f s x