-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem iteratedFDerivWithin_neg_apply {f : E → F} (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x

Proof state:
case succ.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
x : E
hx : x ∈ s
h : Fin (i + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (i + 1) (-f) s x) h = (-iteratedFDerivWithin 𝕜 (i + 1) f s x) h

Tactic:
calc
  iteratedFDerivWithin 𝕜 (i + 1) (-f) s x h =
      fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x (h 0) (Fin.tail h) :=
    rfl
  _ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
    rw [fderivWithin_congr' (@hi) hx]; rfl
  _ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
    rw [Pi.neg_def, fderivWithin_neg (hu x hx)]; rfl
  _ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := rfl

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 0 (-f) s x = -iteratedFDerivWithin 𝕜 0 f s x

Tactic:
ext

Result:
case zero.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
x✝ : Fin 0 → E
⊢ (iteratedFDerivWithin 𝕜 0 (-f) s x) x✝ = (-iteratedFDerivWithin 𝕜 0 f s x) x✝

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
x : E
hx : x ∈ s
h : Fin (i + 1) → E
⊢ ((fderivWithin 𝕜 (fun x => -iteratedFDerivWithin 𝕜 i f s x) s x) (h 0)) (tail h) =
    ((fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x) (h 0)) (tail h)

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
x : E
i : ℕ
f : E → F
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x

Tactic:
induction' i with i hi generalizing x

Result:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 0 (-f) s x = -iteratedFDerivWithin 𝕜 0 f s x

case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 (i + 1) (-f) s x = -iteratedFDerivWithin 𝕜 (i + 1) f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
x : E
hx : x ∈ s
h : Fin (i + 1) → E
⊢ ((-fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x) (h 0)) (tail h) =
    -((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x) (h 0)) (tail h)

Tactic:
rfl

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 (i + 1) (-f) s x = -iteratedFDerivWithin 𝕜 (i + 1) f s x

Tactic:
ext h

Result:
case succ.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
x : E
hx : x ∈ s
h : Fin (i + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (i + 1) (-f) s x) h = (-iteratedFDerivWithin 𝕜 (i + 1) f s x) h

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
x : E
hx : x ∈ s
h : Fin (i + 1) → E
⊢ ((fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x) (h 0)) (tail h) =
    -((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x) (h 0)) (tail h)

Tactic:
rw [Pi.neg_def, fderivWithin_neg (hu x hx)]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
x : E
hx : x ∈ s
h : Fin (i + 1) → E
⊢ ((-fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x) (h 0)) (tail h) =
    -((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x) (h 0)) (tail h)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
x : E
hx : x ∈ s
h : Fin (i + 1) → E
⊢ ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x) (h 0)) (tail h) =
    ((fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x) (h 0)) (tail h)

Tactic:
rw [fderivWithin_congr' (@hi) hx]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
x : E
hx : x ∈ s
h : Fin (i + 1) → E
⊢ ((fderivWithin 𝕜 (fun x => -iteratedFDerivWithin 𝕜 i f s x) s x) (h 0)) (tail h) =
    ((fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x) (h 0)) (tail h)

Proof state:
case zero.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
x✝ : Fin 0 → E
⊢ (iteratedFDerivWithin 𝕜 0 (-f) s x) x✝ = (-iteratedFDerivWithin 𝕜 0 f s x) x✝

Tactic:
simp

Result:
no goals