-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mfderiv_neg (f : M → E') (x : M) :
    (mfderiv I 𝓘(𝕜, E') (-f) x : TangentSpace I x →L[𝕜] E') =
      (-mfderiv I 𝓘(𝕜, E') f x : TangentSpace I x →L[𝕜] E')

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : M → E'
x : M
⊢ (if MDifferentiableAt I 𝓘(𝕜, E') (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f)) (range ↑I) (↑(extChartAt I x) x)
    else 0) =
    -if MDifferentiableAt I 𝓘(𝕜, E') f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f) (range ↑I) (↑(extChartAt I x) x)
      else 0

Tactic:
by_cases hf : MDifferentiableAt I 𝓘(𝕜, E') f x

Result:
case pos
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : M → E'
x : M
hf : MDifferentiableAt I 𝓘(𝕜, E') f x
⊢ (if MDifferentiableAt I 𝓘(𝕜, E') (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f)) (range ↑I) (↑(extChartAt I x) x)
    else 0) =
    -if MDifferentiableAt I 𝓘(𝕜, E') f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f) (range ↑I) (↑(extChartAt I x) x)
      else 0

case neg
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : M → E'
x : M
hf : ¬MDifferentiableAt I 𝓘(𝕜, E') f x
⊢ (if MDifferentiableAt I 𝓘(𝕜, E') (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f)) (range ↑I) (↑(extChartAt I x) x)
    else 0) =
    -if MDifferentiableAt I 𝓘(𝕜, E') f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f) (range ↑I) (↑(extChartAt I x) x)
      else 0

Proof state:
case pos
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : M → E'
x : M
hf : MDifferentiableAt I 𝓘(𝕜, E') f x
⊢ (if MDifferentiableAt I 𝓘(𝕜, E') (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f)) (range ↑I) (↑(extChartAt I x) x)
    else 0) =
    -if MDifferentiableAt I 𝓘(𝕜, E') f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f) (range ↑I) (↑(extChartAt I x) x)
      else 0

Tactic:
exact hf.hasMFDerivAt.neg.mfderiv

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : M → E'
x : M
hf : ¬MDifferentiableAt I 𝓘(𝕜, E') f x
⊢ (if MDifferentiableAt I 𝓘(𝕜, E') (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f)) (range ↑I) (↑(extChartAt I x) x)
    else 0) =
    -if MDifferentiableAt I 𝓘(𝕜, E') f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f) (range ↑I) (↑(extChartAt I x) x)
      else 0

Tactic:
rw [if_neg hf]

Result:
case neg
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : M → E'
x : M
hf : ¬MDifferentiableAt I 𝓘(𝕜, E') f x
⊢ (if MDifferentiableAt I 𝓘(𝕜, E') (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f)) (range ↑I) (↑(extChartAt I x) x)
    else 0) =
    -0

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : M → E'
x : M
⊢ mfderiv I 𝓘(𝕜, E') (-f) x = -mfderiv I 𝓘(𝕜, E') f x

Tactic:
simp_rw [mfderiv]

Result:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : M → E'
x : M
⊢ (if MDifferentiableAt I 𝓘(𝕜, E') (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f)) (range ↑I) (↑(extChartAt I x) x)
    else 0) =
    -if MDifferentiableAt I 𝓘(𝕜, E') f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f) (range ↑I) (↑(extChartAt I x) x)
      else 0

Proof state:
case neg
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : M → E'
x : M
hf : ¬MDifferentiableAt I 𝓘(𝕜, E') (-f) x
⊢ (if MDifferentiableAt I 𝓘(𝕜, E') (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f)) (range ↑I) (↑(extChartAt I x) x)
    else 0) =
    -0

Tactic:
rw [if_neg hf, neg_zero]

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : M → E'
x : M
hf : ¬MDifferentiableAt I 𝓘(𝕜, E') f x
⊢ (if MDifferentiableAt I 𝓘(𝕜, E') (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f)) (range ↑I) (↑(extChartAt I x) x)
    else 0) =
    -0

Tactic:
rw [← mdifferentiableAt_neg] at hf

Result:
case neg
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : M → E'
x : M
hf : ¬MDifferentiableAt I 𝓘(𝕜, E') (-f) x
⊢ (if MDifferentiableAt I 𝓘(𝕜, E') (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f)) (range ↑I) (↑(extChartAt I x) x)
    else 0) =
    -0