awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
⊢ (↑l : ℕ∞ω) < n

Tactic:
have hl : l < n := lt_of_lt_of_le (mod_cast lt_add_one l) h2
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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)

Tactic:
subset_trans ?_ (ih hl.le)

Premises used: subset_trans, LT.lt.le
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
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)
⊢ 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:
refine subset_trans ?_ (ih hl.le)

Premises used: subset_trans, LT.lt.le
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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)

Tactic:
Eq.trans_subset ?_ (tsupport_fderiv_subset 𝕜)

Premises used: tsupport_fderiv_subset, Eq.trans_subset
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
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))
⊢ 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 Eq.trans_subset ?_ (tsupport_fderiv_subset 𝕜)

Premises used: tsupport_fderiv_subset, Eq.trans_subset
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
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))
⊢ 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:
rw [funext <| hf.fderiv_eq (mod_cast hl)]

Premises used: HasFTaylorSeriesUpTo.fderiv_eq, funext
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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))

Tactic:
tsupport_comp_eq (g := ContinuousMultilinearMap.curryLeft) (fun {x} ↦ ?_) _ |>.symm

Premises used: tsupport_comp_eq, ContinuousMultilinearMap.curryLeft, Eq.symm, MultilinearMap.mkContinuousLinear, LinearMap.mkContinuous
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
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
⊢ 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:
refine tsupport_comp_eq (g := ContinuousMultilinearMap.curryLeft) (fun {x} ↦ ?_) _ |>.symm

Premises used: tsupport_comp_eq, Eq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
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:
(continuousMultilinearCurryLeftEquiv _ _ _).map_eq_zero_iff (x := x)

Premises used: ContinuousMultilinearMap.curryLeft, LinearIsometryEquiv.map_eq_zero_iff, continuousMultilinearCurryLeftEquiv, MultilinearMap.mkContinuousLinear, LinearMap.mkContinuous
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
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:
exact (continuousMultilinearCurryLeftEquiv _ _ _).map_eq_zero_iff (x := x)

Premises used: LinearIsometryEquiv.map_eq_zero_iff, continuousMultilinearCurryLeftEquiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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)
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)
⊢ 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)

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)

Premises used: HasFTaylorSeriesUpTo.fderiv_eq, tsupport_comp_eq, funext, tsupport_fderiv_subset, Eq.symm, refl, Eq.trans_subset
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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

Tactic:
(hf.tsupport_mono zero_le h).trans_eq ?_

Premises used: zero_le, LE.le.trans_eq, HasFTaylorSeriesUpTo.tsupport_mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
refine :
  (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) fun (x : E) ↦ p x 0) = tsupport f
⊢ (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦ p x m) ⊆ tsupport f

Tactic:
refine (hf.tsupport_mono zero_le h).trans_eq ?_

Premises used: zero_le, LE.le.trans_eq, HasFTaylorSeriesUpTo.tsupport_mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
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))
⊢ (tsupport (α := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) fun (x : E) ↦ p x 0) = tsupport f

Tactic:
rw [← funext hf.zero_eq]

Premises used: HasFTaylorSeriesUpTo.zero_eq, funext
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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))

Tactic:
tsupport_comp_eq (g := ContinuousMultilinearMap.curry0) (fun {x} ↦ ?_) _ |>.symm

Premises used: tsupport_comp_eq, Eq.symm, ContinuousMultilinearMap.curry0
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
refine : ∀ {x : ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin 0) ↦ E) F}, x.curry0 = 0 ↔ x = 0
⊢ 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:
refine tsupport_comp_eq (g := ContinuousMultilinearMap.curry0) (fun {x} ↦ ?_) _ |>.symm

Premises used: tsupport_comp_eq, Eq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
x : ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin 0) ↦ E) F
⊢ x.curry0 = 0 ↔ x = 0

Tactic:
(continuousMultilinearCurryFin0 _ _ _).map_eq_zero_iff (x := x)

Premises used: continuousMultilinearCurryFin0, LinearIsometryEquiv.map_eq_zero_iff, ContinuousMultilinearMap.curry0
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
x : ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin 0) ↦ E) F
⊢ x.curry0 = 0 ↔ x = 0

Tactic:
exact (continuousMultilinearCurryFin0 _ _ _).map_eq_zero_iff (x := x)

Premises used: continuousMultilinearCurryFin0, LinearIsometryEquiv.map_eq_zero_iff
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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 0 → E
⊢ (iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) m = f x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 f)
    ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
      f)

Tactic:
rfl

Premises used: ContinuousMultilinearMap.constOfIsEmpty, iteratedFDeriv, ContinuousMultilinearMap.uncurry0, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
rw :
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
          f)
        x) =
    ‖f x‖
rw₁ :
  norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
          (f x) :
        ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) =
    ‖f x‖
rw₂ rw₃ : ‖f x‖ = ‖f x‖
⊢ norm (E := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 f x) = ‖f x‖

Tactic:
rw [iteratedFDeriv_zero_eq_comp, comp_apply, LinearIsometryEquiv.norm_map]

Premises used: LinearIsometryEquiv.norm_map, iteratedFDeriv_zero_eq_comp, Function.comp_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 f s)
    (iteratedFDeriv 𝕜 0 f)

Tactic:
rfl

Premises used: iteratedFDeriv, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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 : Fin (n + 1) → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) m : F)
    ((((fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x : (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) (m 0) :
            ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) :
          (a : (i : Fin n) → E) → F)
        (tail (α := fun (i : Fin (n + 1)) ↦ E) m) :
      F)

Tactic:
rfl

Premises used: iteratedFDeriv, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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 : ℕ
⊢ Eq (α := E → ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (iteratedFDeriv 𝕜 (n + 1) 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)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f)))

Tactic:
rfl

Premises used: ContinuousLinearMap.uncurryLeft, MultilinearMap.mkContinuous, iteratedFDeriv, rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
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 : ℕ
⊢ Eq (α := (x : E) → E →L[𝕜] ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (fderiv 𝕜 (iteratedFDeriv 𝕜 n f))
    (comp (β := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
      (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) →
          E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv 𝕜 (n + 1) f))

Tactic:
rfl

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, ContinuousMultilinearMap.curryLeft, MultilinearMap.mkContinuous, Fin.induction, MultilinearMap.mk', Fin.cases, iteratedFDeriv, MultilinearMap.mkContinuousLinear, Fin.tail, LinearMap.mkContinuous, rfl