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
s : Set E
f : E → F
x : E
n : ℕ
rw :
  norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
        (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
              (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
                ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
        (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s) x)
rw₁ :
  norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
              (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
                ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
              ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
          (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) :
        ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
⊢ norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1) f s x)
have rw₂ : norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) =
  norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x)
Tactic: rw [iteratedFDerivWithin_succ_eq_comp_left, 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
s t : Set E
x : E
f g : E → F
y : E
hsx : UniqueDiffWithinAt 𝕜 s x
hyt : UniqueDiffWithinAt 𝕜 t y
⊢ dist (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 1) ↦ E) F) (iteratedFDerivWithin 𝕜 1 f s x)
      (iteratedFDerivWithin 𝕜 1 g t y) =
    dist (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 g t y)
have simp : dist (α := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    ((↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
            F ≃L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) :
        F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘SL
      fderivWithin 𝕜 f s x)
    ((↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
            F ≃L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) :
        F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘SL
      fderivWithin 𝕜 g t y) =
  dist (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 g t y)
Tactic: simp only [iteratedFDerivWithin_succ_eq_comp_left, comp_apply,
    LinearIsometryEquiv.dist_map, iteratedFDerivWithin_zero_eq_comp,
    LinearIsometryEquiv.comp_fderivWithin, hsx, hyt]
-- 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
s : Set E
x : E
f : E → F
h : UniqueDiffWithinAt 𝕜 s x
⊢ norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 1) ↦ E) F) (iteratedFDerivWithin 𝕜 1 f s x) =
    norm (E := E →L[𝕜] F) (fderivWithin 𝕜 f s x)
have simp : norm (E := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    ((↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
            F ≃L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) :
        F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘SL
      fderivWithin 𝕜 f s x) =
  norm (E := E →L[𝕜] F) (fderivWithin 𝕜 f s x)
Tactic: simp only [← norm_fderivWithin_iteratedFDerivWithin,
    iteratedFDerivWithin_zero_eq_comp, LinearIsometryEquiv.comp_fderivWithin _ h]
-- 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
s : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
m : Fin (HAdd.hAdd (α := ℕ) 0 1) → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (HAdd.hAdd (α := ℕ) 0 1) f s x : (a : (i : Fin (0 + 1)) → E) → F) m : F)
    ((((iteratedFDerivWithin 𝕜 0 (fun (y : E) ↦ fderivWithin 𝕜 f s y) s 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)
have zero : Eq.{uF + 1} (α := F)
  (((((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F) :
                (E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) ≃ₗᵢ[𝕜]
                  ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F) :
              (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) →
                ContinuousMultilinearMap 𝕜 (fun (x : Fin (0 + 1)) ↦ E) F)
            ((↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
                    F ≃L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) :
                F →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘SL
              fderivWithin 𝕜 f s x) :
          ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F) :
        (a : (i : Fin (0 + 1)) → E) → F)
      m :
    F)
  ((fderivWithin 𝕜 f s x : (a : E) → F) (m (last 0)) : F)
Tactic: rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_zero_eq_comp,
      iteratedFDerivWithin_zero_apply, Function.comp_apply,
      LinearIsometryEquiv.comp_fderivWithin _ (hs x hx)]
-- 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
s : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E} (hx : x ∈ s) (m : Fin (n + 1) → E),
    Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1) f s x : (a : (i : Fin (n + 1)) → E) → F) m : F)
      ((((iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s 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)
x : E
hx : x ∈ s
m : Fin (n + 1 + 1) → E
I : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F) ≃ₗᵢ[𝕜]
  ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F :=
  LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F)
y : E
hy : y ∈ s
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) (iteratedFDerivWithin 𝕜 n.succ f s y)
    (comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      ((⇑I :
          (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)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s :
        E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      y)
have H : ∀ (m : (i : Fin n.succ) → E),
  Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 n.succ f s y : (a : (i : Fin n.succ) → E) → F) m : F)
    ((comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            ((⇑I :
                (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)
            (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s :
              E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            y :
          (a : (i : Fin n.succ) → E) → F)
        m :
      F)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (hypothesis)
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
s : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
n : ℕ
IH :
  ∀ {x : E} (hx : x ∈ s) (m : Fin (n + 1) → E),
    Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1) f s x : (a : (i : Fin (n + 1)) → E) → F) m : F)
      ((((iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s 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)
x : E
hx : x ∈ s
m : Fin (n + 1 + 1) → E
I : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F) ≃ₗᵢ[𝕜]
  ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F :=
  LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F)
⊢ Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1 + 1) f s x : (a : (i : Fin (n + 1 + 1)) → E) → F) m : F)
    ((((iteratedFDerivWithin 𝕜 (n + 1) (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x :
                (a : (i : Fin (n + 1)) → E) → E →L[𝕜] F)
              (init (α := fun (i : Fin (n + 1 + 1)) ↦ E) m) :
            E →L[𝕜] F) :
          (a : E) → F)
        (m (last (n + 1))) :
      F)
have A : ∀ y ∈ s,
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F) (iteratedFDerivWithin 𝕜 n.succ f s y)
    (comp (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      ((⇑I :
          (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)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s :
        E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      y)
Tactic: have A : ∀ y ∈ s, iteratedFDerivWithin 𝕜 n.succ f s y =
        (I ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) y := fun y hy ↦ by
      ext m
      simp [IH hy m, I]
-- 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
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1) f s x : (a : (i : Fin (n + 1)) → E) → F) m : F)
    ((((iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s 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)
have zero : ∀ {x : E} (hx : x ∈ s) (m : Fin (HAdd.hAdd (α := ℕ) 0 1) → E),
  Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (HAdd.hAdd (α := ℕ) 0 1) f s x : (a : (i : Fin (0 + 1)) → E) → F) m : F)
    ((((iteratedFDerivWithin 𝕜 0 (fun (y : E) ↦ fderivWithin 𝕜 f s y) s 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)
Tactic: induction n generalizing x with
  | zero =>
    rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_zero_eq_comp,
      iteratedFDerivWithin_zero_apply, Function.comp_apply,
      LinearIsometryEquiv.comp_fderivWithin _ (hs x hx)]
    simp
  | succ n IH =>
    let I := (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm
    have A : ∀ y ∈ s, iteratedFDerivWithin 𝕜 n.succ f s y =
        (I ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) y := fun y hy ↦ by
      ext m
      simp [IH hy m, I]
    calc
      (iteratedFDerivWithin 𝕜 (n + 2) f s x : (Fin (n + 2) → E) → F) m =
          (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n.succ f s) s x : E → E [×n + 1]→L[𝕜] F) (m 0)
            (tail m) := by
        simp [iteratedFDerivWithin_succ_eq_comp_left]
      _ = (fderivWithin 𝕜 (I ∘ iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s) s x :
              E → E [×n + 1]→L[𝕜] F) (m 0) (tail m) := by
        rw [fderivWithin_congr A (A x hx)]
      _ = (I ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s) s x :
              E → E [×n + 1]→L[𝕜] F) (m 0) (tail m) := by
        simp [LinearIsometryEquiv.comp_fderivWithin _ (hs x hx)]
      _ = (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) s x :
              E → E [×n]→L[𝕜] E →L[𝕜] F) (m 0) (init (tail m)) ((tail m) (last n)) := by
        simp [I]
      _ = iteratedFDerivWithin 𝕜 (Nat.succ n) (fun y => fderivWithin 𝕜 f s y) s x (init m)
            (m (last (n + 1))) := by
        rw [iteratedFDerivWithin_succ_apply_left, tail_init_eq_init_tail]
        simp [init, tail]
Cleared hypotheses: x, n, hx, m
-- 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
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) f s x)
    (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)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s :
        E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      x)
have H : ∀ (m : (i : Fin (n + 1)) → E),
  Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (n + 1) f s 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)
            (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s :
              E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
            x :
          (a : (i : Fin (n + 1)) → E) → F)
        m :
      F)
Tactic: ext m
-- 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
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1) f s x)
have rw : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
    (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s 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)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s :
        E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      x)
Tactic: rw [iteratedFDerivWithin_succ_eq_comp_right hs hx, 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
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s 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)
        (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s :
          E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
        x)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1) f s x)
have rw₁ : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
    (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s 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)
        (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x) :
      ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
Tactic: rw [iteratedFDerivWithin_succ_eq_comp_right hs hx, 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
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s 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)
        (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s :
          E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
        x)
rw₁ :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s 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)
          (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x) :
        ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n.succ) ↦ E) F)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
      (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x) =
    norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (n + 1) f s x)
have rw₂ : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
    (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x) =
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
    (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ fderivWithin 𝕜 f s y) s x :
      ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F))
Tactic: rw [iteratedFDerivWithin_succ_eq_comp_right hs hx, 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
s : Set E
f : E → F
z : E
hs : UniqueDiffOn 𝕜 s
hz : z ∈ s
m : Fin 2 → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 2 f s z : (a : (i : Fin 2) → E) → F) m : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z : (a : E) → E →L[𝕜] F) (m 0) : E →L[𝕜] F) : (a : E) → F) (m 1) : F)
have simp : Eq.{uF + 1} (α := F)
  ((((((iteratedFDerivWithin 𝕜 0 (fun (y : E) ↦ fderivWithin 𝕜 (fun (y : E) ↦ fderivWithin 𝕜 f s y) s y) s z :
                    (a : (i : Fin 0) → E) → E →L[𝕜] E →L[𝕜] F)
                  (init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E)
                    (init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ E) m)) :
                E →L[𝕜] E →L[𝕜] F) :
              (a : E) → E →L[𝕜] F)
            (init (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ E) m (last 0)) :
          E →L[𝕜] F) :
        (a : E) → F)
      (m (last 1)) :
    F)
  ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z : (a : E) → E →L[𝕜] F) (m 0) : E →L[𝕜] F) : (a : E) → F) (m 1) : F)
Tactic: simp only [iteratedFDerivWithin_succ_apply_right hs hz]