-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
/-- The iterated derivative commutes with shifting the function by a constant on the left. -/
lemma iteratedFDerivWithin_comp_add_left' (n : ℕ) (a : E) :
    iteratedFDerivWithin 𝕜 n (fun z ↦ f (a + z)) s =
      fun x ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)

Proof state:
𝕜 : Type u
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
n : ℕ
a : E
⊢ iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s = fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)

Tactic:
induction n with
| zero => simp [iteratedFDerivWithin]
| succ n IH =>
  ext v
  rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left]
  simp only [Nat.succ_eq_add_one, IH, comp_apply, continuousMultilinearCurryLeftEquiv_symm_apply]
  congr 2
  rw [fderivWithin_comp_add_left]

Result:
no goals

Proof state:
case succ.h.H
𝕜 : Type u
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
a : E
n : ℕ
IH : iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s = fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
v : E
x✝ : Fin (n + 1) → E
⊢ ((fderivWithin 𝕜 (fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)) s v) (x✝ 0)) (tail x✝) =
    ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f (a +ᵥ s)) (a +ᵥ s) (a + v)) (x✝ 0)) (tail x✝)

Tactic:
congr 2

Result:
case succ.h.H.e_a.e_a
𝕜 : Type u
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
a : E
n : ℕ
IH : iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s = fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
v : E
x✝ : Fin (n + 1) → E
⊢ fderivWithin 𝕜 (fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)) s v =
    fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f (a +ᵥ s)) (a +ᵥ s) (a + v)

Proof state:
case succ
𝕜 : Type u
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
a : E
n : ℕ
IH : iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s = fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
⊢ iteratedFDerivWithin 𝕜 (n + 1) (fun z => f (a + z)) s = fun x => iteratedFDerivWithin 𝕜 (n + 1) f (a +ᵥ s) (a + x)

Tactic:
ext v

Result:
case succ.h.H
𝕜 : Type u
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
a : E
n : ℕ
IH : iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s = fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
v : E
x✝ : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) (fun z => f (a + z)) s v) x✝ = (iteratedFDerivWithin 𝕜 (n + 1) f (a +ᵥ s) (a + v)) x✝

Proof state:
case zero
𝕜 : Type u
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
a : E
⊢ iteratedFDerivWithin 𝕜 0 (fun z => f (a + z)) s = fun x => iteratedFDerivWithin 𝕜 0 f (a +ᵥ s) (a + x)

Tactic:
simp [iteratedFDerivWithin]

Result:
no goals

Proof state:
case succ.h.H
𝕜 : Type u
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
a : E
n : ℕ
IH : iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s = fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
v : E
x✝ : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) (fun z => f (a + z)) s v) x✝ = (iteratedFDerivWithin 𝕜 (n + 1) f (a +ᵥ s) (a + v)) x✝

Tactic:
rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left]

Result:
case succ.h.H
𝕜 : Type u
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
a : E
n : ℕ
IH : iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s = fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
v : E
x✝ : Fin (n + 1) → E
⊢ ((⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘
          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s) s)
        v)
      x✝ =
    ((⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘
          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f (a +ᵥ s)) (a +ᵥ s))
        (a + v))
      x✝

Proof state:
case succ.h.H
𝕜 : Type u
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
a : E
n : ℕ
IH : iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s = fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
v : E
x✝ : Fin (n + 1) → E
⊢ ((⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘
          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s) s)
        v)
      x✝ =
    ((⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘
          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f (a +ᵥ s)) (a +ᵥ s))
        (a + v))
      x✝

Tactic:
simp only [Nat.succ_eq_add_one, IH, comp_apply, continuousMultilinearCurryLeftEquiv_symm_apply]

Result:
case succ.h.H
𝕜 : Type u
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
a : E
n : ℕ
IH : iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s = fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
v : E
x✝ : Fin (n + 1) → E
⊢ ((fderivWithin 𝕜 (fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)) s v) (x✝ 0)) (tail x✝) =
    ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f (a +ᵥ s)) (a +ᵥ s) (a + v)) (x✝ 0)) (tail x✝)

Proof state:
case succ.h.H.e_a.e_a
𝕜 : Type u
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
a : E
n : ℕ
IH : iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s = fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
v : E
x✝ : Fin (n + 1) → E
⊢ fderivWithin 𝕜 (fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)) s v =
    fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f (a +ᵥ s)) (a +ᵥ s) (a + v)

Tactic:
rw [fderivWithin_comp_add_left]

Result:
no goals