awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
m : (i : Fin (n + 1)) → E
H :
  Eq.{uF + 1} (α := F)
    ((((iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x : (a : (i : Fin n) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (n + 1)) ↦ E) m) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last n)) :
      F)
    ((comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F)) :
                (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                  ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
              (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
            (iteratedFDeriv 𝕜 n fun (y : E) ↦ fderiv 𝕜 f y :
              E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            x :
          (a : (i : Fin (n + 1)) → E) → F)
        m :
      F)
⊢ Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) m : F)
    ((comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F)) :
                (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                  ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
              (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
            (iteratedFDeriv 𝕜 n fun (y : E) ↦ fderiv 𝕜 f y :
              E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            x :
          (a : (i : Fin (n + 1)) → E) → F)
        m :
      F)
have H₁ : Eq.{uF + 1} (α := F)
  ((((iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x : (a : (i : Fin n) → E) → E →L[𝕜] F)
            (init (α := fun (i : Fin (n + 1)) ↦ E) m) :
          E →L[𝕜] F) :
        (a : E) → F)
      (m (last n)) :
    F)
  ((((LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F) :
              (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
                ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ E) F)
            (iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x) :
          ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
        (a : (i : Fin (n + 1)) → E) → F)
      m :
    F)
Tactic: rw [iteratedFDeriv_succ_apply_right, comp_apply, continuousMultilinearCurryRightEquiv_symm_apply']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) (iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (iteratedFDeriv 𝕜 (n + 1) f x)
have rw : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) (iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) =
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F)) :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
          ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
      (iteratedFDeriv 𝕜 n fun (y : E) ↦ fderiv 𝕜 f y : E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      x)
Tactic: rw [iteratedFDeriv_succ_eq_comp_right, comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) (iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
        ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
        (iteratedFDeriv 𝕜 n fun (y : E) ↦ fderiv 𝕜 f y :
          E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
        x)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) (iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (iteratedFDeriv 𝕜 (n + 1) f x)
have rw₁ : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) (iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) =
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ E) F)
        (iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
Tactic: rw [iteratedFDeriv_succ_eq_comp_right, comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) (iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
        ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F)) :
            (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
              ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
        (iteratedFDeriv 𝕜 n fun (y : E) ↦ fderiv 𝕜 f y :
          E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
        x)
rw₁ :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) (iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      ((LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F) :
            (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
              ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ E) F)
          (iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x) :
        ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) (iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (iteratedFDeriv 𝕜 (n + 1) f x)
have rw₂ : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) (iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) =
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
    (iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
Tactic: rw [iteratedFDeriv_succ_eq_comp_right, comp_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
m : Fin 1 → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 1 f x : (a : (i : Fin 1) → E) → F) m : F)
    ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F)
have rw : Eq.{uF + 1} (α := F)
  ((((iteratedFDeriv 𝕜 0 (fun (y : E) ↦ fderiv 𝕜 f y) x : (a : (i : Fin 0) → E) → E →L[𝕜] F)
            (init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) m) :
          E →L[𝕜] F) :
        (a : E) → F)
      (m (last 0)) :
    F)
  ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F)
Tactic: rw [iteratedFDeriv_succ_apply_right, iteratedFDeriv_zero_apply, last_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
m : Fin 1 → E
rw :
  Eq.{uF + 1} (α := F)
    ((((iteratedFDeriv 𝕜 0 (fun (y : E) ↦ fderiv 𝕜 f y) x : (a : (i : Fin 0) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) m) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last 0)) :
      F)
    ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F)
⊢ Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 1 f x : (a : (i : Fin 1) → E) → F) m : F)
    ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F)
have rw₁ : Eq.{uF + 1} (α := F) ((fderiv 𝕜 f x : (a : E) → F) (m (last 0)) : F) ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F)
Tactic: rw [iteratedFDeriv_succ_apply_right, iteratedFDeriv_zero_apply, last_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
m : Fin 1 → E
rw :
  Eq.{uF + 1} (α := F)
    ((((iteratedFDeriv 𝕜 0 (fun (y : E) ↦ fderiv 𝕜 f y) x : (a : (i : Fin 0) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) m) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last 0)) :
      F)
    ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F)
rw₁ : Eq.{uF + 1} (α := F) ((fderiv 𝕜 f x : (a : E) → F) (m (last 0)) : F) ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F)
⊢ Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 1 f x : (a : (i : Fin 1) → E) → F) m : F)
    ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F)
have rw₂ : Eq.{uF + 1} (α := F) ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F) ((fderiv 𝕜 f x : (a : E) → F) (m 0) : F)
Tactic: rw [iteratedFDeriv_succ_apply_right, iteratedFDeriv_zero_apply, last_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
f : E → F
⊢ norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 1) ↦ E) F) (iteratedFDeriv 𝕜 1 f x) =
    norm (E := E →L[𝕜] F) (fderiv 𝕜 f x)
have rw : norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 1) ↦ E) F) (iteratedFDerivWithin 𝕜 1 f univ x) =
  norm (E := E →L[𝕜] F) (fderivWithin 𝕜 f univ x)
Tactic: rw [← iteratedFDerivWithin_univ, ← fderivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih :
  ∀ (a : 𝕜),
    iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s a =
      HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
        (iteratedFDerivWithin 𝕜 n f (-s) (-a))
a : 𝕜
⊢ Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s)
    fun (a : 𝕜) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
      (iteratedFDerivWithin 𝕜 n f (-s) (-a))
have h : ∀ (b : 𝕜),
  Eq.{uF + 1} (α := F)
    (((iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s b : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
            (iteratedFDerivWithin 𝕜 n f (-s) (-b)) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
Tactic: ext b
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih :
  ∀ (a : 𝕜),
    iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s a =
      HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
        (iteratedFDerivWithin 𝕜 n f (-s) (-a))
a b : 𝕜
⊢ Eq.{uF + 1} (α := F)
    (((iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s b : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
            (iteratedFDerivWithin 𝕜 n f (-s) (-b)) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
have h : Eq.{uF + 1} (α := F)
  ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
          (iteratedFDerivWithin 𝕜 n f (-s) (-b)) :
        (a : (i : Fin n) → 𝕜) → F)
      fun (x : Fin n) ↦ 1 :
    F)
  ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
          (iteratedFDerivWithin 𝕜 n f (-s) (-b)) :
        (a : (i : Fin n) → 𝕜) → F)
      fun (x : Fin n) ↦ 1 :
    F)
Tactic: rw [ih b]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih :
  ∀ (a : 𝕜),
    iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s a =
      HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
        (iteratedFDerivWithin 𝕜 n f (-s) (-a))
a : 𝕜
⊢ iteratedFDerivWithin 𝕜 (n + 1) (fun (x : 𝕜) ↦ f (-x)) s a =
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) (n + 1))
      (iteratedFDerivWithin 𝕜 (n + 1) f (-s) (-a))
have ih' : Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s)
  fun (a : 𝕜) ↦
  HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
    (iteratedFDerivWithin 𝕜 n f (-s) (-a))
Tactic: have ih' : iteratedFDerivWithin 𝕜 n (fun x => f (-x)) s
        = fun a ↦ (-1 : 𝕜) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a) := by
      ext b
      rw [ih b]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
a : 𝕜
⊢ iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s a =
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
      (iteratedFDerivWithin 𝕜 n f (-s) (-a))
have zero : ∀ (a : 𝕜),
  iteratedFDerivWithin 𝕜 0 (fun (x : 𝕜) ↦ f (-x)) s a =
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (β := ℕ) (-1) 0)
      (iteratedFDerivWithin 𝕜 0 f (-s) (-a))
Tactic: induction n generalizing a with
  | zero => simp [iteratedFDerivWithin]
  | succ n ih =>
    have ih' : iteratedFDerivWithin 𝕜 n (fun x => f (-x)) s
        = fun a ↦ (-1 : 𝕜) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a) := by
      ext b
      rw [ih b]
    set g := fun a ↦ iteratedFDerivWithin 𝕜 n f (-s) a
    rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left,
      Function.comp_apply, Function.comp_apply, ih', ← Pi.smul_def,
      fderivWithin_const_smul_field' ((-1 : 𝕜) ^ n) (f := fun a ↦ g (-a)),
      fderivWithin_comp_neg (f := g), ← neg_one_smul 𝕜 (fderivWithin 𝕜 _ (-s) (-a)),
      ← mul_smul _ (-1), ← pow_succ (-1) n, map_smul]
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
a : 𝕜
zero :
  ∀ (a : 𝕜),
    iteratedFDerivWithin 𝕜 0 (fun (x : 𝕜) ↦ f (-x)) s a =
      HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (β := ℕ) (-1) 0)
        (iteratedFDerivWithin 𝕜 0 f (-s) (-a))
⊢ iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s a =
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
      (iteratedFDerivWithin 𝕜 n f (-s) (-a))
have succ : ∀ (n : ℕ)
  (ih :
    ∀ (a : 𝕜),
      iteratedFDerivWithin 𝕜 n (fun (x : 𝕜) ↦ f (-x)) s a =
        HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
          (iteratedFDerivWithin 𝕜 n f (-s) (-a)))
  (a : 𝕜),
  iteratedFDerivWithin 𝕜 (n + 1) (fun (x : 𝕜) ↦ f (-x)) s a =
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) (n + 1))
      (iteratedFDerivWithin 𝕜 (n + 1) f (-s) (-a))
Tactic: induction n generalizing a with
  | zero => simp [iteratedFDerivWithin]
  | succ n ih =>
    have ih' : iteratedFDerivWithin 𝕜 n (fun x => f (-x)) s
        = fun a ↦ (-1 : 𝕜) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a) := by
      ext b
      rw [ih b]
    set g := fun a ↦ iteratedFDerivWithin 𝕜 n f (-s) a
    rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left,
      Function.comp_apply, Function.comp_apply, ih', ← Pi.smul_def,
      fderivWithin_const_smul_field' ((-1 : 𝕜) ^ n) (f := fun a ↦ g (-a)),
      fderivWithin_comp_neg (f := g), ← neg_one_smul 𝕜 (fderivWithin 𝕜 _ (-s) (-a)),
      ← mul_smul _ (-1), ← pow_succ (-1) n, map_smul]
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
c : 𝕜
⊢ Eq (α := 𝕜 → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F)
    (iteratedFDerivWithin 𝕜 n (fun (z : 𝕜) ↦ f (c - z)) s) fun (x : 𝕜) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
      (iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c - x))
have h : ∀ (a : 𝕜),
  Eq.{uF + 1} (α := F)
    (((iteratedFDerivWithin 𝕜 n (fun (z : 𝕜) ↦ f (c - z)) s a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
            (iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c - a)) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
c a : 𝕜
⊢ Eq.{uF + 1} (α := F)
    (((iteratedFDerivWithin 𝕜 n (fun (z : 𝕜) ↦ f (c - z)) s a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
            (iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c - a)) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
have this : Eq (α := (z : 𝕜) → F) (fun (z : 𝕜) ↦ f (c - z)) fun (z : 𝕜) ↦ (fun (w : 𝕜) ↦ f (c + w)) (-z)
Tactic: have : (fun z : 𝕜 => f (c - z)) = fun z => (fun w => f (c + w)) (-z) := by
    simp only [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
c a : 𝕜
this : Eq (α := (z : 𝕜) → F) (fun (z : 𝕜) ↦ f (c - z)) fun (z : 𝕜) ↦ (fun (w : 𝕜) ↦ f (c + w)) (-z)
⊢ Eq.{uF + 1} (α := F)
    (((iteratedFDerivWithin 𝕜 n (fun (z : 𝕜) ↦ f (c - z)) s a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
            (iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c - a)) :
          (a : (i : Fin n) → 𝕜) → F)
        fun (x : Fin n) ↦ 1 :
      F)
have h : Eq.{uF + 1} (α := F)
  ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
          (iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c + -a)) :
        (a : (i : Fin n) → 𝕜) → F)
      fun (x : Fin n) ↦ 1 :
    F)
  ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) F) (HPow.hPow (α := 𝕜) (-1) n)
          (iteratedFDerivWithin 𝕜 n f (c +ᵥ -s) (c - a)) :
        (a : (i : Fin n) → 𝕜) → F)
      fun (x : Fin n) ↦ 1 :
    F)
Tactic: rw [this, iteratedFDerivWithin_comp_neg (f := fun w => f (c + w)) n a,
    iteratedFDerivWithin_comp_add_left]