awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) s x)
      (-iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
h : (i : Fin (i + 1)) → E
rw :
  Eq.{uF + 1} (α := F)
    ((((fderivWithin 𝕜 (fun (x : E) ↦ -iteratedFDerivWithin 𝕜 i f s x) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    ((((fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
⊢ Eq.{uF + 1} (α := F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    ((((fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
have rw₁ : Eq.{uF + 1} (α := F)
  ((((fderivWithin 𝕜 (fun (x : E) ↦ -iteratedFDerivWithin 𝕜 i f s x) s x :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
            (h 0) :
          ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
        (a : (i : Fin i) → E) → F)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
    F)
  ((((fderivWithin 𝕜 (fun (i_1 : E) ↦ -iteratedFDerivWithin 𝕜 i f s i_1) s x :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
            (h 0) :
          ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
        (a : (i : Fin i) → E) → F)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
    F)
Tactic: rw [fderivWithin_congr' (@hi) hx, Pi.neg_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) s x)
      (-iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
h : (i : Fin (i + 1)) → E
⊢ Eq.{uF + 1} (α := F)
    ((((fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    (-(((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
                (h 0) :
              ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
            (a : (i : Fin i) → E) → F)
          (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
have rw : Eq.{uF + 1} (α := F)
  ((((-fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x : (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
            (h 0) :
          ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
        (a : (i : Fin i) → E) → F)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
    F)
  (-(((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x : (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
    F)
Tactic: rw [fderivWithin_neg (hu x hx), ContinuousLinearMap.neg_apply,
          ContinuousMultilinearMap.neg_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) s x)
      (-iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
h : (i : Fin (i + 1)) → E
rw :
  Eq.{uF + 1} (α := F)
    ((((-fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    (-(((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
                (h 0) :
              ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
            (a : (i : Fin i) → E) → F)
          (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
⊢ Eq.{uF + 1} (α := F)
    ((((fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    (-(((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
                (h 0) :
              ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
            (a : (i : Fin i) → E) → F)
          (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
have rw₁ : Eq.{uF + 1} (α := F)
  (((-(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x : (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
          ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
        (a : (i : Fin i) → E) → F)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
    F)
  (-(((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x : (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
    F)
Tactic: rw [fderivWithin_neg (hu x hx), ContinuousLinearMap.neg_apply,
          ContinuousMultilinearMap.neg_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) s x)
      (-iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
h : (i : Fin (i + 1)) → E
⊢ Eq.{uF + 1} (α := F)
    (-(((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
                (h 0) :
              ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
            (a : (i : Fin i) → E) → F)
          (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    (-(iteratedFDerivWithin 𝕜 (i + 1) f s x : (a : (i : Fin (i + 1)) → E) → F) h : F)
have rw : Eq.{uF + 1} (α := F)
  (-(((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x : (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
    F)
  (-(((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x : (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
    F)
Tactic: rw [iteratedFDerivWithin_succ_apply_left]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) s x)
      (-iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
h : (i : Fin (i + 1)) → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (i + 1) (-f) s x : (a : (i : Fin (i + 1)) → E) → F) h : F)
    ((-iteratedFDerivWithin 𝕜 (i + 1) f s x : (a : (i : Fin (i + 1)) → E) → F) h : F)
have iteratedFDerivWithin : Eq.{uF + 1} (α := F)
  ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
            (h 0) :
          ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
        (a : (i : Fin i) → E) → F)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
    F)
  ((((fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x : (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
            (h 0) :
          ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
        (a : (i : Fin i) → E) → F)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
    F)
Tactic: calc
      iteratedFDerivWithin 𝕜 (i + 1) (-f) s x h =
          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x (h 0) (Fin.tail h) :=
        iteratedFDerivWithin_succ_apply_left _
      _ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
        rw [fderivWithin_congr' (@hi) hx, Pi.neg_def]
      _ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
        rw [fderivWithin_neg (hu x hx), ContinuousLinearMap.neg_apply,
          ContinuousMultilinearMap.neg_apply]
      _ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := by
        rw [iteratedFDerivWithin_succ_apply_left]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (_root_.iteratedFDerivWithin 𝕜 i (-f) s x) (-_root_.iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
h : (i : Fin (i + 1)) → E
iteratedFDerivWithin :
  Eq.{uF + 1} (α := F)
    ((((fderivWithin 𝕜 (_root_.iteratedFDerivWithin 𝕜 i (-f) s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    ((((fderivWithin 𝕜 (-_root_.iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
⊢ Eq.{uF + 1} (α := F) ((_root_.iteratedFDerivWithin 𝕜 (i + 1) (-f) s x : (a : (i : Fin (i + 1)) → E) → F) h : F)
    ((-_root_.iteratedFDerivWithin 𝕜 (i + 1) f s x : (a : (i : Fin (i + 1)) → E) → F) h : F)
have iteratedFDerivWithin₁ : Eq.{uF + 1} (α := F)
  ((((fderivWithin 𝕜 (-_root_.iteratedFDerivWithin 𝕜 i f s) s x :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
            (h 0) :
          ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
        (a : (i : Fin i) → E) → F)
      (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
    F)
  (-(((fderivWithin 𝕜 (_root_.iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
    F)
Tactic: calc
      iteratedFDerivWithin 𝕜 (i + 1) (-f) s x h =
          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x (h 0) (Fin.tail h) :=
        iteratedFDerivWithin_succ_apply_left _
      _ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
        rw [fderivWithin_congr' (@hi) hx, Pi.neg_def]
      _ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
        rw [fderivWithin_neg (hu x hx), ContinuousLinearMap.neg_apply,
          ContinuousMultilinearMap.neg_apply]
      _ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := by
        rw [iteratedFDerivWithin_succ_apply_left]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
i : ℕ
f : E → F
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) s x)
    (-iteratedFDerivWithin 𝕜 i f s x)
have zero : ∀ {x : E} (hx : x ∈ s),
  Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 (-f) s x)
    (-iteratedFDerivWithin 𝕜 0 f s x)
Tactic: induction i generalizing x with ext h
  | zero => simp
  | succ i hi =>
    calc
      iteratedFDerivWithin 𝕜 (i + 1) (-f) s x h =
          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x (h 0) (Fin.tail h) :=
        iteratedFDerivWithin_succ_apply_left _
      _ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
        rw [fderivWithin_congr' (@hi) hx, Pi.neg_def]
      _ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
        rw [fderivWithin_neg (hu x hx), ContinuousLinearMap.neg_apply,
          ContinuousMultilinearMap.neg_apply]
      _ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := by
        rw [iteratedFDerivWithin_succ_apply_left]
Cleared hypotheses: x, i, hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
i : ℕ
f : E → F
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
zero :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 (-f) s x)
      (-iteratedFDerivWithin 𝕜 0 f s x)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) s x)
    (-iteratedFDerivWithin 𝕜 i f s x)
have zero₁ : ∀ {x : E} (hx : x ∈ s) (h : (i : Fin 0) → E),
  Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 0 (-f) s x : (a : (i : Fin 0) → E) → F) h : F)
    ((-iteratedFDerivWithin 𝕜 0 f s x : (a : (i : Fin 0) → E) → F) h : F)
Tactic: induction i generalizing x with ext h
  | zero => simp
  | succ i hi =>
    calc
      iteratedFDerivWithin 𝕜 (i + 1) (-f) s x h =
          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x (h 0) (Fin.tail h) :=
        iteratedFDerivWithin_succ_apply_left _
      _ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
        rw [fderivWithin_congr' (@hi) hx, Pi.neg_def]
      _ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
        rw [fderivWithin_neg (hu x hx), ContinuousLinearMap.neg_apply,
          ContinuousMultilinearMap.neg_apply]
      _ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := by
        rw [iteratedFDerivWithin_succ_apply_left]
Cleared hypotheses: x, i, hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
i : ℕ
f : E → F
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
zero :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 (-f) s x)
      (-iteratedFDerivWithin 𝕜 0 f s x)
zero₁ :
  ∀ {x : E} (hx : x ∈ s) (h : (i : Fin 0) → E),
    Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 0 (-f) s x : (a : (i : Fin 0) → E) → F) h : F)
      ((-iteratedFDerivWithin 𝕜 0 f s x : (a : (i : Fin 0) → E) → F) h : F)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) s x)
    (-iteratedFDerivWithin 𝕜 i f s x)
have succ : ∀ (i : ℕ)
  (hi :
    ∀ {x : E} (hx : x ∈ s),
      Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) s x)
        (-iteratedFDerivWithin 𝕜 i f s x))
  {x : E} (hx : x ∈ s),
  Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (i + 1) (-f) s x) (-iteratedFDerivWithin 𝕜 (i + 1) f s x)
Tactic: induction i generalizing x with ext h
  | zero => simp
  | succ i hi =>
    calc
      iteratedFDerivWithin 𝕜 (i + 1) (-f) s x h =
          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x (h 0) (Fin.tail h) :=
        iteratedFDerivWithin_succ_apply_left _
      _ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
        rw [fderivWithin_congr' (@hi) hx, Pi.neg_def]
      _ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
        rw [fderivWithin_neg (hu x hx), ContinuousLinearMap.neg_apply,
          ContinuousMultilinearMap.neg_apply]
      _ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := by
        rw [iteratedFDerivWithin_succ_apply_left]
Cleared hypotheses: x, i, hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
i : ℕ
f : E → F
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
zero :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 (-f) s x)
      (-iteratedFDerivWithin 𝕜 0 f s x)
zero₁ :
  ∀ {x : E} (hx : x ∈ s) (h : (i : Fin 0) → E),
    Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 0 (-f) s x : (a : (i : Fin 0) → E) → F) h : F)
      ((-iteratedFDerivWithin 𝕜 0 f s x : (a : (i : Fin 0) → E) → F) h : F)
succ :
  ∀ (i : ℕ)
    (hi :
      ∀ {x : E} (hx : x ∈ s),
        Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
          (iteratedFDerivWithin 𝕜 i (-f) s x) (-iteratedFDerivWithin 𝕜 i f s x))
    {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (i + 1) (-f) s x) (-iteratedFDerivWithin 𝕜 (i + 1) f s x)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) s x)
    (-iteratedFDerivWithin 𝕜 i f s x)
have succ₁ : ∀ (i : ℕ)
  (hi :
    ∀ {x : E} (hx : x ∈ s),
      Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) s x)
        (-iteratedFDerivWithin 𝕜 i f s x))
  {x : E} (hx : x ∈ s) (h : (i : Fin (i + 1)) → E),
  Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (i + 1) (-f) s x : (a : (i : Fin (i + 1)) → E) → F) h : F)
    ((-iteratedFDerivWithin 𝕜 (i + 1) f s x : (a : (i : Fin (i + 1)) → E) → F) h : F)
Tactic: induction i generalizing x with ext h
  | zero => simp
  | succ i hi =>
    calc
      iteratedFDerivWithin 𝕜 (i + 1) (-f) s x h =
          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x (h 0) (Fin.tail h) :=
        iteratedFDerivWithin_succ_apply_left _
      _ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
        rw [fderivWithin_congr' (@hi) hx, Pi.neg_def]
      _ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
        rw [fderivWithin_neg (hu x hx), ContinuousLinearMap.neg_apply,
          ContinuousMultilinearMap.neg_apply]
      _ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := by
        rw [iteratedFDerivWithin_succ_apply_left]
Cleared hypotheses: x, i, hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
i : ℕ
f : E → F
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i (-f) x)
    (-iteratedFDeriv 𝕜 i f x)
have simp_rw : Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) univ x)
  (-iteratedFDerivWithin 𝕜 i f univ x)
Tactic: simp_rw [← iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x
hg : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 i (f - g) s x =
    HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s x) (iteratedFDerivWithin 𝕜 i g s x)
have rw : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (-g) s x
Tactic: rw [sub_eq_add_neg, iteratedFDerivWithin_add_apply hf _ hu hx,
    iteratedFDerivWithin_neg_apply hu hx, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
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
i : ℕ
f g : E → F
hf : ContDiffAt 𝕜 (↑i : ℕ∞ω) f x
hg : ContDiffAt 𝕜 (↑i : ℕ∞ω) g x
⊢ iteratedFDeriv 𝕜 i (f - g) x =
    HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i f x)
      (iteratedFDeriv 𝕜 i g x)
have simp_rw : iteratedFDerivWithin 𝕜 i (f - g) univ x =
  HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i f univ x) (iteratedFDerivWithin 𝕜 i g univ x)
Tactic: simp_rw [← iteratedFDerivWithin_univ]