awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
zero :
  CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 0) ↦ E) F) (_root_.iteratedFDeriv 𝕜 0 f)
    s
succ :
  ∀ (n : ℕ)
    (IH :
      CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F)
        (_root_.iteratedFDeriv 𝕜 n f) s),
    CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (_root_.iteratedFDeriv 𝕜 (n + 1) f) s
⊢ CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (_root_.iteratedFDeriv 𝕜 n f)
    s

Tactic:
induction n with
  | zero =>
    rw [iteratedFDeriv_zero_eq_comp]
    exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E [×0]→L[𝕜] F).comp_cpolynomialOn h
  | succ n IH =>
    rw [iteratedFDeriv_succ_eq_comp_left]
    convert! ContinuousLinearMap.comp_cpolynomialOn ?g IH.fderiv
    case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm
    simp

Premises used: LinearIsometryEquiv.symm, continuousMultilinearCurryFin0, ContinuousLinearMap.comp_cpolynomialOn, iteratedFDeriv_zero_eq_comp, LinearIsometryEquiv.toContinuousLinearEquiv, continuousMultilinearCurryLeftEquiv, iteratedFDeriv_succ_eq_comp_left, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
h : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (deriv f) s

Tactic:
(ContinuousLinearMap.apply 𝕜 F (1 : 𝕜)).comp_cpolynomialOn h.fderiv

Premises used: deriv, ContinuousLinearMap.apply, ContinuousLinearMap.comp_cpolynomialOn, CPolynomialOn.fderiv, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
h : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (deriv^[0] f) s

Tactic:
h

Premises used: Nat.iterate
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
h : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (deriv^[0] f) s

Tactic:
exact h
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (deriv^[n] f) s
⊢ CPolynomialOn 𝕜 (deriv^[n + 1] f) s

Tactic:
simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

Premises used: Function.iterate_succ', CPolynomialOn.deriv, Function.comp_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
h : CPolynomialOn 𝕜 f s
n : ℕ
zero : CPolynomialOn 𝕜 (deriv^[0] f) s
succ : ∀ (n : ℕ) (IH : CPolynomialOn 𝕜 (deriv^[n] f) s), CPolynomialOn 𝕜 (deriv^[n + 1] f) s
⊢ CPolynomialOn 𝕜 (deriv^[n] f) s

Tactic:
induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

Premises used: Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
k l : ℕ
h : k + l ≠ Fintype.card ι
x : { s : Finset (Fin (k + l)) // s.card = l }
h_1 : Membership.mem (γ := Finset { s : Finset (Fin (k + l)) // s.card = l }) Finset.univ x
simp_rw :
  Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
      (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    ((curryFinFinset 𝕜 ((i : ι) → E i) F ⋯ ⋯ :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin (k + l)) ↦ (i : ι) → E i) F) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
              (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
        (f.toFormalMultilinearSeries (E := E) (k + l)) :
      ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
        (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    (0 :
      ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
        (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
simp_rw₁ :
  Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
      (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    ((curryFinFinset 𝕜 ((i : ι) → E i) F ⋯ ⋯ :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin (k + l)) ↦ (i : ι) → E i) F) →
          ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
            (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
      (if h : Fintype.card ι = k + l then
        domDomCongr (Fintype.equivFinOfCardEq h)
          (f.compContinuousLinearMap (M₁ := fun (i : ι) ↦ (i : ι) → E i) (M₁' := E) (ContinuousLinearMap.proj (φ := E)))
      else 0))
    0
simp_rw₂ :
  Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
      (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    ((curryFinFinset 𝕜 ((i : ι) → E i) F ⋯ ⋯ :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin (k + l)) ↦ (i : ι) → E i) F) →
          ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
            (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
      0)
    0
⊢ Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
      (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    (changeOriginSeriesTerm (f.toFormalMultilinearSeries (E := E)) k l (↑x : Finset (Fin (k + l))) ⋯) 0

Tactic:
simp_rw [FormalMultilinearSeries.changeOriginSeriesTerm,
      toFormalMultilinearSeries, dif_neg h.symm, LinearIsometryEquiv.map_zero]

Premises used: LinearIsometryEquiv.map_zero, Ne.symm, ContinuousMultilinearMap.toFormalMultilinearSeries, dif_neg, FormalMultilinearSeries.changeOriginSeriesTerm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
h :
  ∀ (y : (i : ι) → E i),
    Eq.{v + 1} (α := F)
      ((((continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F :
                  (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F) → ((i : ι) → E i) →L[𝕜] F)
                (changeOrigin (f.toFormalMultilinearSeries (E := E)) x 1) :
              ((i : ι) → E i) →L[𝕜] F) :
            (a : (i : ι) → E i) → F)
          y :
        F)
      ((f.linearDeriv (M₁ := E) x : (a : (i : ι) → E i) → F) y : F)
⊢ (continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F) → ((i : ι) → E i) →L[𝕜] F)
      (changeOrigin (f.toFormalMultilinearSeries (E := E)) x 1) =
    f.linearDeriv (M₁ := E) x

Tactic:
ext y
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h :
  Eq.{v + 1} (α := F)
    ((∑' (n : ℕ),
            (changeOriginSeries (f.toFormalMultilinearSeries (E := E)) 1 n :
                (a : (i : Fin n) → (i : ι) → E i) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
              fun (x_1 : Fin n) ↦ x :
          (a : (i : Fin 1) → (i : ι) → E i) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ (i : ι) → E i) 0 y) :
      F)
    (∑ i : ι, (f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
⊢ Eq.{v + 1} (α := F)
    ((((continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F :
                (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F) → ((i : ι) → E i) →L[𝕜] F)
              (changeOrigin (f.toFormalMultilinearSeries (E := E)) x 1) :
            ((i : ι) → E i) →L[𝕜] F) :
          (a : (i : ι) → E i) → F)
        y :
      F)
    ((f.linearDeriv (M₁ := E) x : (a : (i : ι) → E i) → F) y : F)

Tactic:
rw [continuousMultilinearCurryFin1_apply, linearDeriv_apply,
      changeOrigin, FormalMultilinearSeries.sum]

Premises used: ContinuousMultilinearMap.linearDeriv_apply, FormalMultilinearSeries.changeOrigin, FormalMultilinearSeries.sum, continuousMultilinearCurryFin1_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h :
  IsEmpty ι →
    Eq.{v + 1} (α := F)
      ((∑' (n : ℕ),
              (changeOriginSeries (f.toFormalMultilinearSeries (E := E)) 1 n :
                  (a : (i : Fin n) → (i : ι) → E i) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
                fun (x_1 : Fin n) ↦ x :
            (a : (i : Fin 1) → (i : ι) → E i) → F)
          (Fin.snoc (α := fun (i : Fin 1) ↦ (i : ι) → E i) 0 y) :
        F)
      (∑ i : ι, (f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
h₁ :
  Nonempty ι →
    Eq.{v + 1} (α := F)
      ((∑' (n : ℕ),
              (changeOriginSeries (f.toFormalMultilinearSeries (E := E)) 1 n :
                  (a : (i : Fin n) → (i : ι) → E i) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
                fun (x_1 : Fin n) ↦ x :
            (a : (i : Fin 1) → (i : ι) → E i) → F)
          (Fin.snoc (α := fun (i : Fin 1) ↦ (i : ι) → E i) 0 y) :
        F)
      (∑ i : ι, (f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
⊢ Eq.{v + 1} (α := F)
    ((∑' (n : ℕ),
            (changeOriginSeries (f.toFormalMultilinearSeries (E := E)) 1 n :
                (a : (i : Fin n) → (i : ι) → E i) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
              fun (x_1 : Fin n) ↦ x :
          (a : (i : Fin 1) → (i : ι) → E i) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ (i : ι) → E i) 0 y) :
      F)
    (∑ i : ι, (f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : IsEmpty ι
l : ℕ
rw : l + 1 ≠ 0
⊢ 1 + l ≠ Fintype.card ι

Tactic:
rw [add_comm, Fintype.card_eq_zero]

Premises used: Fintype.card_eq_zero, add_comm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : IsEmpty ι
l : ℕ
⊢ l + 1 ≠ 0

Tactic:
Nat.succ_ne_zero _

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : IsEmpty ι
l : ℕ
⊢ l + 1 ≠ 0

Tactic:
exact Nat.succ_ne_zero _

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : IsEmpty ι
⊢ ∀ (l : ℕ), 1 + l ≠ Fintype.card ι

Tactic:
have (l : _) : 1 + l ≠ Fintype.card ι := by
      rw [add_comm, Fintype.card_eq_zero]; exact Nat.succ_ne_zero _
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h_1 : IsEmpty ι
this : ∀ (l : ℕ), 1 + l ≠ Fintype.card ι
h :
  Eq.{v + 1} (α := F)
    ((0 : (a : (i : Fin 1) → (i : ι) → E i) → F) (Fin.snoc (α := fun (i : Fin 1) ↦ (i : ι) → E i) 0 y) : F) (0 : F)
⊢ Eq.{v + 1} (α := F)
    ((∑' (n : ℕ),
            (changeOriginSeries (f.toFormalMultilinearSeries (E := E)) 1 n :
                (a : (i : Fin n) → (i : ι) → E i) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
              fun (x_1 : Fin n) ↦ x :
          (a : (i : Fin 1) → (i : ι) → E i) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ (i : ι) → E i) 0 y) :
      F)
    (∑ i : ι, (f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)

Tactic:
simp_rw [Fintype.sum_empty, changeOriginSeries_support _ (this _), zero_apply _, tsum_zero]

Premises used: Fintype.sum_empty, tsum_zero, ContinuousMultilinearMap.changeOriginSeries_support, ContinuousMultilinearMap.zero_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : IsEmpty ι
this : ∀ (l : ℕ), 1 + l ≠ Fintype.card ι
⊢ Eq.{v + 1} (α := F)
    ((0 : (a : (i : Fin 1) → (i : ι) → E i) → F) (Fin.snoc (α := fun (i : Fin 1) ↦ (i : ι) → E i) 0 y) : F) (0 : F)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h_1 : Nonempty ι
h :
  Eq.{v + 1} (α := F)
    (((∑ s : { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 },
                changeOriginSeriesTerm (f.toFormalMultilinearSeries (E := E)) 1 (Fintype.card ι - 1)
                  (↑s : Finset (Fin (1 + (Fintype.card ι - 1)))) ⋯ :
              (a : (i : Fin (Fintype.card ι - 1)) → (i : ι) → E i) →
                ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
            fun (x_1 : Fin (Fintype.card ι - 1)) ↦ x :
          (a : (i : Fin 1) → (i : ι) → E i) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ (i : ι) → E i) 0 y) :
      F)
    (∑ i : ι, (f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
h₁ :
  ∀ (b' : ℕ),
    b' ≠ Fintype.card ι - 1 →
      Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
        ((changeOriginSeries (f.toFormalMultilinearSeries (E := E)) 1 b' :
            (a : (i : Fin b') → (i : ι) → E i) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
          fun (x_1 : Fin b') ↦ x)
        0
⊢ Eq.{v + 1} (α := F)
    ((∑' (n : ℕ),
            (changeOriginSeries (f.toFormalMultilinearSeries (E := E)) 1 n :
                (a : (i : Fin n) → (i : ι) → E i) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
              fun (x_1 : Fin n) ↦ x :
          (a : (i : Fin 1) → (i : ι) → E i) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ (i : ι) → E i) 0 y) :
      F)
    (∑ i : ι, (f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)

Tactic:
rw [tsum_eq_single (Fintype.card ι - 1), changeOriginSeries]

Premises used: HSub.hSub, FormalMultilinearSeries.changeOriginSeries, Fintype.card, tsum_eq_single, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
m : ℕ
hm : ¬m = Fintype.card ι - 1
⊢ 1 ≤ Fintype.card ι

Tactic:
Fintype.card_pos

Premises used: Fintype.card_pos, Nat.lt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
m : ℕ
hm : ¬m = Fintype.card ι - 1
⊢ 1 ≤ Fintype.card ι

Tactic:
exact Fintype.card_pos

Premises used: Fintype.card_pos
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
m : ℕ
hm : m ≠ Fintype.card ι - 1
⊢ ¬1 + m = Fintype.card ι

Tactic:
rw [Ne, eq_tsub_iff_add_eq_of_le (by exact Fintype.card_pos), add_comm] at hm

Premises used: Ne, add_comm, eq_tsub_iff_add_eq_of_le
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h_1 : Nonempty ι
m : ℕ
hm : ¬1 + m = Fintype.card ι
h :
  Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
    ((0 : (a : (i : Fin m) → (i : ι) → E i) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
      fun (x_1 : Fin m) ↦ x)
    0
h₁ h₂ : Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F) 0 0
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
    ((changeOriginSeries (f.toFormalMultilinearSeries (E := E)) 1 m :
        (a : (i : Fin m) → (i : ι) → E i) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
      fun (x_1 : Fin m) ↦ x)
    0

Tactic:
rw [f.changeOriginSeries_support hm, zero_apply]

Premises used: ContinuousMultilinearMap.changeOriginSeries_support, ContinuousMultilinearMap.zero_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h_1 : Nonempty ι
h :
  Eq.{v + 1} (α := F)
    (∑ a : { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 },
      ((changeOriginSeriesTerm (f.toFormalMultilinearSeries (E := E)) 1 (Fintype.card ι - 1)
                (↑a : Finset (Fin (1 + (Fintype.card ι - 1)))) ⋯ :
              (a : (i : Fin (Fintype.card ι - 1)) → (i : ι) → E i) →
                ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
            fun (x_1 : Fin (Fintype.card ι - 1)) ↦ x :
          (a : (i : Fin 1) → (i : ι) → E i) → F)
        fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ y)
    (∑ i : ι, (f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)))
⊢ Eq.{v + 1} (α := F)
    (((∑ s : { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 },
                changeOriginSeriesTerm (f.toFormalMultilinearSeries (E := E)) 1 (Fintype.card ι - 1)
                  (↑s : Finset (Fin (1 + (Fintype.card ι - 1)))) ⋯ :
              (a : (i : Fin (Fintype.card ι - 1)) → (i : ι) → E i) →
                ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
            fun (x_1 : Fin (Fintype.card ι - 1)) ↦ x :
          (a : (i : Fin 1) → (i : ι) → E i) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ (i : ι) → E i) 0 y) :
      F)
    (∑ i : ι, (f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)

Tactic:
rw [sum_apply, ContinuousMultilinearMap.sum_apply, Fin.snoc_zero]

Premises used: ContinuousMultilinearMap.sum_apply, Fin.snoc_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h_1 : Nonempty ι
h :
  Eq.{v + 1} (α := F)
    (∑ x_1 : { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 },
      (f.toFormalMultilinearSeries (E := E) (1 + (Fintype.card ι - 1)) :
          (a : (i : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) → F)
        ((↑x_1 : Finset (Fin (1 + (Fintype.card ι - 1)))).piecewise (π := fun (i : Fin (1 + (Fintype.card ι - 1))) ↦
          (i : ι) → E i) (fun (x_2 : Fin (1 + (Fintype.card ι - 1))) ↦ x) fun (x : Fin (1 + (Fintype.card ι - 1))) ↦ y))
    (∑ i : ι, (f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)))
⊢ Eq.{v + 1} (α := F)
    (∑ a : { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 },
      ((changeOriginSeriesTerm (f.toFormalMultilinearSeries (E := E)) 1 (Fintype.card ι - 1)
                (↑a : Finset (Fin (1 + (Fintype.card ι - 1)))) ⋯ :
              (a : (i : Fin (Fintype.card ι - 1)) → (i : ι) → E i) →
                ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
            fun (x_1 : Fin (Fintype.card ι - 1)) ↦ x :
          (a : (i : Fin 1) → (i : ι) → E i) → F)
        fun (x : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ y)
    (∑ i : ι, (f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)))

Tactic:
simp_rw [changeOriginSeriesTerm_apply]

Premises used: FormalMultilinearSeries.changeOriginSeriesTerm_apply