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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
m : ℕ
hmn : (↑m : ℕ∞ω) ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ p x m = iteratedFDerivWithin 𝕜 m f s x
have zero : ∀ {x : E} (hmn : (↑0 : ℕ∞ω) ≤ n) (hx : x ∈ s),
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (p x 0) (iteratedFDerivWithin 𝕜 0 f s x)
Tactic: induction m generalizing x with
  | zero => rw [h.zero_eq' hx, iteratedFDerivWithin_zero_eq_comp, comp_apply]
  | succ m IH =>
    have A : m < n := lt_of_lt_of_le (mod_cast lt_add_one m) hmn
    have :
      HasFDerivWithinAt (fun y : E => iteratedFDerivWithin 𝕜 m f s y)
        (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m))) s x :=
      (h.fderivWithin m A x hx).congr (fun y hy => (IH (le_of_lt A) hy).symm)
        (IH (le_of_lt A) hx).symm
    rw [iteratedFDerivWithin_succ_eq_comp_left, Function.comp_apply, this.fderivWithin (hs x hx)]
    exact (ContinuousMultilinearMap.uncurry_curryLeft _).symm
Cleared hypotheses: x, m, hmn, 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
x : E
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
m : ℕ
hmn : (↑m : ℕ∞ω) ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
zero :
  ∀ {x : E} (hmn : (↑0 : ℕ∞ω) ≤ n) (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (p x 0) (iteratedFDerivWithin 𝕜 0 f s x)
⊢ p x m = iteratedFDerivWithin 𝕜 m f s x
have succ : ∀ (m : ℕ) (IH : ∀ {x : E} (hmn : (↑m : ℕ∞ω) ≤ n) (hx : x ∈ s), p x m = iteratedFDerivWithin 𝕜 m f s x) {x : E}
  (hmn : (↑(m + 1) : ℕ∞ω) ≤ n) (hx : x ∈ s),
  Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p x (m + 1))
    (iteratedFDerivWithin 𝕜 (m + 1) f s x)
Tactic: induction m generalizing x with
  | zero => rw [h.zero_eq' hx, iteratedFDerivWithin_zero_eq_comp, comp_apply]
  | succ m IH =>
    have A : m < n := lt_of_lt_of_le (mod_cast lt_add_one m) hmn
    have :
      HasFDerivWithinAt (fun y : E => iteratedFDerivWithin 𝕜 m f s y)
        (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m))) s x :=
      (h.fderivWithin m A x hx).congr (fun y hy => (IH (le_of_lt A) hy).symm)
        (IH (le_of_lt A) hx).symm
    rw [iteratedFDerivWithin_succ_eq_comp_left, Function.comp_apply, this.fderivWithin (hs x hx)]
    exact (ContinuousMultilinearMap.uncurry_curryLeft _).symm
Cleared hypotheses: x, m, hmn, 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
a : E
n : ℕ
IH :
  Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦
    iteratedFDerivWithin 𝕜 (n + 1) f (a +ᵥ s) (a + x)
have succ : ∀ (v : E) (x : (i : Fin (n + 1)) → E),
  Eq.{uF + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 (n + 1) (fun (z : E) ↦ f (a + z)) s v : (a : (i : Fin (n + 1)) → E) → F) x : F)
    ((iteratedFDerivWithin 𝕜 (n + 1) f (a +ᵥ s) (a + v) : (a : (i : Fin (n + 1)) → E) → F) x : F)
Tactic: ext v
-- 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
n : ℕ
a : E
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
have zero : Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
  (iteratedFDerivWithin 𝕜 0 (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦ iteratedFDerivWithin 𝕜 0 f (a +ᵥ s) (a + x)
Tactic: induction n with
  | zero => simp [iteratedFDerivWithin]
  | succ n IH =>
    ext v
    simp [iteratedFDerivWithin_succ_eq_comp_left, IH, fderivWithin_comp_add_left]
Cleared hypotheses: n
-- 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
n : ℕ
a : E
zero :
  Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDerivWithin 𝕜 0 (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦ iteratedFDerivWithin 𝕜 0 f (a +ᵥ s) (a + x)
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
have succ : ∀ (n : ℕ)
  (IH :
    Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)),
  Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (n + 1) (fun (z : E) ↦ f (a + z)) s) fun (x : E) ↦
    iteratedFDerivWithin 𝕜 (n + 1) f (a +ᵥ s) (a + x)
Tactic: induction n with
  | zero => simp [iteratedFDerivWithin]
  | succ n IH =>
    ext v
    simp [iteratedFDerivWithin_succ_eq_comp_left, IH, fderivWithin_comp_add_left]
Cleared hypotheses: n
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
x : E
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (p x 0)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
      (f x))
have rw : Eq (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (p x 0)
  ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
      (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
    (ContinuousMultilinearMap.curry0 (p x 0)))
Tactic: rw [← h.zero_eq x]
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn n f p univ ↔ HasFTaylorSeriesUpTo n f p
have mp : HasFTaylorSeriesUpToOn n f p univ → HasFTaylorSeriesUpTo n f p
Tactic: constructor
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
mp : HasFTaylorSeriesUpToOn n f p univ → HasFTaylorSeriesUpTo n f p
⊢ HasFTaylorSeriesUpToOn n f p univ ↔ HasFTaylorSeriesUpTo n f p
have mpr : HasFTaylorSeriesUpTo n f p → HasFTaylorSeriesUpToOn n f p univ
Tactic: constructor
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn n f p univ → HasFTaylorSeriesUpTo n f p
have mp : ∀ (H : HasFTaylorSeriesUpToOn n f p univ) (m : ℕ),
  (↑m : ℕ∞ω) < n →
    ∀ (x : E),
      HasFDerivAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (y : E) ↦ p y m)
        (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) x
Tactic: refine fun H ↦ ⟨by simpa using H.zero_eq, ?_, by simpa using H.cont⟩
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpTo n f p → HasFTaylorSeriesUpToOn n f p univ
have mpr : ∀ (H : HasFTaylorSeriesUpTo n f p) (m : ℕ),
  (↑m : ℕ∞ω) < n →
    ∀ (x : E),
      Membership.mem (γ := Set E) univ x →
        HasFDerivWithinAt (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) (fun (x : E) ↦ p x m)
          (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p x m.succ)) univ x
Tactic: refine fun H ↦ ⟨by simpa using H.zero_eq, ?_, by simpa using H.cont⟩
-- 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
m n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
hmn : m ≤ n
⊢ HasFTaylorSeriesUpTo m f p
have rw : ∀ (h : HasFTaylorSeriesUpToOn n f p univ) (hmn : m ≤ n), HasFTaylorSeriesUpToOn m f p univ
Tactic: rw [← hasFTaylorSeriesUpToOn_univ_iff] at h ⊢
Cleared hypotheses: h, hmn
-- 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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
have h₁ : HasFTaylorSeriesUpToOn n f p univ
Tactic: rw [← hasFTaylorSeriesUpToOn_univ_iff] at h
Cleared hypotheses: 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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
have rw : ContinuousOn f univ
Tactic: rw [← continuousOn_univ]
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
hn : n ≠ 0
x : E
⊢ HasFDerivAt.{u, uE, uF} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p x 1))
    x
have rw : HasFDerivWithinAt.{u, uE, uF} (𝕜 := 𝕜) f
  ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
    (p x 1))
  univ x
Tactic: rw [← hasFDerivWithinAt_univ]
-- 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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
k m : ℕ
hf : HasFTaylorSeriesUpTo n f p
l : ℕ
h : k.le l
ih :
  ∀ (h2 : (↑l : ℕ∞ω) ≤ n),
    Subset.{uE} (α := Set E)
      (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l) ↦ E) F) fun (x : E) ↦ p x l)
      (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
h2 : (↑l.succ : ℕ∞ω) ≤ n
⊢ Subset.{uE} (α := Set E)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l.succ) ↦ E) F) fun (x : E) ↦ p x l.succ)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
have hl : (↑l : ℕ∞ω) < n
Tactic: have hl : l < n := lt_of_lt_of_le (mod_cast lt_add_one l) h2
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
k m : ℕ
hf : HasFTaylorSeriesUpTo n f p
l : ℕ
h : k.le l
ih :
  ∀ (h2 : (↑l : ℕ∞ω) ≤ n),
    Subset.{uE} (α := Set E)
      (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l) ↦ E) F) fun (x : E) ↦ p x l)
      (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
h2 : (↑l.succ : ℕ∞ω) ≤ n
hl : (↑l : ℕ∞ω) < n
⊢ Subset.{uE} (α := Set E)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l.succ) ↦ E) F) fun (x : E) ↦ p x l.succ)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
have step : Subset.{uE} (α := Set E)
  (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l.succ) ↦ E) F) fun (x : E) ↦ p x l.succ)
  (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l) ↦ E) F) fun (x : E) ↦ p x l)
Tactic: refine subset_trans ?_ (ih hl.le)
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
k m : ℕ
hf : HasFTaylorSeriesUpTo n f p
l : ℕ
h : k.le l
ih :
  ∀ (h2 : (↑l : ℕ∞ω) ≤ n),
    Subset.{uE} (α := Set E)
      (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l) ↦ E) F) fun (x : E) ↦ p x l)
      (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
h2 : (↑l.succ : ℕ∞ω) ≤ n
hl : (↑l : ℕ∞ω) < n
⊢ Subset.{uE} (α := Set E)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l.succ) ↦ E) F) fun (x : E) ↦ p x l.succ)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l) ↦ E) F) fun (x : E) ↦ p x l)
have step : Eq.{uE + 1} (α := Set E)
  (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l.succ) ↦ E) F) fun (x : E) ↦ p x l.succ)
  (tsupport (α := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l) ↦ E) F)
    (fderiv 𝕜 fun (x : E) ↦ p x l))
Tactic: refine Eq.trans_subset ?_ (tsupport_fderiv_subset 𝕜)
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
k m : ℕ
hf : HasFTaylorSeriesUpTo n f p
l : ℕ
h : k.le l
ih :
  ∀ (h2 : (↑l : ℕ∞ω) ≤ n),
    Subset.{uE} (α := Set E)
      (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l) ↦ E) F) fun (x : E) ↦ p x l)
      (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
h2 : (↑l.succ : ℕ∞ω) ≤ n
hl : (↑l : ℕ∞ω) < n
⊢ Eq.{uE + 1} (α := Set E)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l.succ) ↦ E) F) fun (x : E) ↦ p x l.succ)
    (tsupport (α := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l) ↦ E) F)
      (fderiv 𝕜 fun (x : E) ↦ p x l))
have step : Eq.{uE + 1} (α := Set E)
  (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l.succ) ↦ E) F) fun (x : E) ↦ p x l.succ)
  (tsupport (α := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l) ↦ E) F) fun (x : E) ↦
    ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin l.succ) ↦ E) (p x l.succ))
Tactic: rw [funext <| hf.fderiv_eq (mod_cast hl)]
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
k m : ℕ
hf : HasFTaylorSeriesUpTo n f p
l : ℕ
h : k.le l
ih :
  ∀ (h2 : (↑l : ℕ∞ω) ≤ n),
    Subset.{uE} (α := Set E)
      (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l) ↦ E) F) fun (x : E) ↦ p x l)
      (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
h2 : (↑l.succ : ℕ∞ω) ≤ n
hl : (↑l : ℕ∞ω) < n
⊢ Eq.{uE + 1} (α := Set E)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l.succ) ↦ E) F) fun (x : E) ↦ p x l.succ)
    (tsupport (α := E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l) ↦ E) F) fun (x : E) ↦
      ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin l.succ) ↦ E) (p x l.succ))
have step : ∀ {x : ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l.succ) ↦ E) F},
  x.curryLeft (Ei := fun (i : Fin l.succ) ↦ E) = 0 ↔ x = 0
Tactic: refine tsupport_comp_eq (g := ContinuousMultilinearMap.curryLeft) (fun {x} ↦ ?_) _ |>.symm
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
k m : ℕ
h : k ≤ m
h2 : (↑m : ℕ∞ω) ≤ n
hf : HasFTaylorSeriesUpTo n f p
⊢ Subset.{uE} (α := Set E)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦ p x m)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
have refl : ∀ (h2 : (↑k : ℕ∞ω) ≤ n),
  Subset.{uE} (α := Set E)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
Tactic: induction h with
  | refl => rfl
  | @step l h ih =>
    have hl : l < n := lt_of_lt_of_le (mod_cast lt_add_one l) h2
    refine subset_trans ?_ (ih hl.le)
    refine Eq.trans_subset ?_ (tsupport_fderiv_subset 𝕜)
    rw [funext <| hf.fderiv_eq (mod_cast hl)]
    refine tsupport_comp_eq (g := ContinuousMultilinearMap.curryLeft) (fun {x} ↦ ?_) _ |>.symm
    exact (continuousMultilinearCurryLeftEquiv _ _ _).map_eq_zero_iff (x := x)
Cleared hypotheses: h, h2
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
k m : ℕ
h : k ≤ m
h2 : (↑m : ℕ∞ω) ≤ n
hf : HasFTaylorSeriesUpTo n f p
refl :
  ∀ (h2 : (↑k : ℕ∞ω) ≤ n),
    Subset.{uE} (α := Set E)
      (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
      (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
⊢ Subset.{uE} (α := Set E)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦ p x m)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
have step : ∀ {l : ℕ} (h : k.le l)
  (ih :
    ∀ (h2 : (↑l : ℕ∞ω) ≤ n),
      Subset.{uE} (α := Set E)
        (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l) ↦ E) F) fun (x : E) ↦ p x l)
        (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k))
  (h2 : (↑l.succ : ℕ∞ω) ≤ n),
  Subset.{uE} (α := Set E)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin l.succ) ↦ E) F) fun (x : E) ↦ p x l.succ)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin k) ↦ E) F) fun (x : E) ↦ p x k)
Tactic: induction h with
  | refl => rfl
  | @step l h ih =>
    have hl : l < n := lt_of_lt_of_le (mod_cast lt_add_one l) h2
    refine subset_trans ?_ (ih hl.le)
    refine Eq.trans_subset ?_ (tsupport_fderiv_subset 𝕜)
    rw [funext <| hf.fderiv_eq (mod_cast hl)]
    refine tsupport_comp_eq (g := ContinuousMultilinearMap.curryLeft) (fun {x} ↦ ?_) _ |>.symm
    exact (continuousMultilinearCurryLeftEquiv _ _ _).map_eq_zero_iff (x := x)
Cleared hypotheses: h, h2
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
m : ℕ
h : (↑m : ℕ∞ω) ≤ n
hf : HasFTaylorSeriesUpTo n f p
⊢ (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦ p x m) ⊆ tsupport f
have refine : (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) fun (x : E) ↦ p x 0) = tsupport f
Tactic: refine (hf.tsupport_mono zero_le h).trans_eq ?_
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
m : ℕ
h : (↑m : ℕ∞ω) ≤ n
hf : HasFTaylorSeriesUpTo n f p
⊢ (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) fun (x : E) ↦ p x 0) = tsupport f
have rw : Eq.{uE + 1} (α := Set E)
  (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) fun (x : E) ↦ p x 0)
  (tsupport.{uE, uF} (α := F) fun (x : E) ↦ ContinuousMultilinearMap.curry0 (p x 0))
Tactic: rw [← funext hf.zero_eq]
-- 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
m : ℕ
h : (↑m : ℕ∞ω) ≤ n
hf : HasFTaylorSeriesUpTo n f p
⊢ Eq.{uE + 1} (α := Set E)
    (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) fun (x : E) ↦ p x 0)
    (tsupport.{uE, uF} (α := F) fun (x : E) ↦ ContinuousMultilinearMap.curry0 (p x 0))
have refine : ∀ {x : ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin 0) ↦ E) F}, x.curry0 = 0 ↔ x = 0
Tactic: refine tsupport_comp_eq (g := ContinuousMultilinearMap.curry0) (fun {x} ↦ ?_) _ |>.symm