awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ 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)
have 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)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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)
⊢ 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)
have 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)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 ι
have rw : l + 1 ≠ 0
Tactic: rw [add_comm, Fintype.card_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (hypothesis)
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)
have this : ∀ (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 _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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)
    ((∑' (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)
have 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)
Tactic: simp_rw [Fintype.sum_empty, changeOriginSeries_support _ (this _), zero_apply _, tsum_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 ι
⊢ 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)
have 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)))) sorry :
            (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 [tsum_eq_single (Fintype.card ι - 1), changeOriginSeries]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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)
⊢ 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)
have 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
Tactic: rw [tsum_eq_single (Fintype.card ι - 1), changeOriginSeries]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (hypothesis)
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
⊢ 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
have hm₁ : ¬1 + m = Fintype.card ι
Tactic: rw [Ne, eq_tsub_iff_add_eq_of_le (by exact Fintype.card_pos), add_comm] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 : ¬1 + m = Fintype.card ι
⊢ 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
have 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
Tactic: rw [f.changeOriginSeries_support hm, zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ 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
have h₁ : Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F) 0 0
Tactic: rw [f.changeOriginSeries_support hm, zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 ι
⊢ 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)
have 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)))) sorry :
            (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: rw [sum_apply, ContinuousMultilinearMap.sum_apply, Fin.snoc_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 ι
⊢ 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)))
have 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)))
Tactic: simp_rw [changeOriginSeriesTerm_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 ι
⊢ 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)))
have h : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0)) →
  { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 }
Tactic: refine (Fintype.sum_bijective (?_ ∘ Fintype.equivFinOfCardEq (Nat.add_sub_of_le
    Fintype.card_pos).symm) (.comp ?_ <| Equiv.bijective _) _ _ fun i ↦ ?_).symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 :
  Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0)) →
    { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 }
⊢ 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)))
have h₁ : Function.Bijective (β := { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 })
  fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
  Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ sorry
Tactic: refine (Fintype.sum_bijective (?_ ∘ Fintype.equivFinOfCardEq (Nat.add_sub_of_le
    Fintype.card_pos).symm) (.comp ?_ <| Equiv.bijective _) _ _ fun i ↦ ?_).symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 :
  Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0)) →
    { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 }
h₁ :
  Function.Bijective (β := { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 })
    fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
    Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ ⋯
⊢ 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)))
have h₂ : ∀ (i : ι),
  Eq.{v + 1} (α := F) ((f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
    ((f.toFormalMultilinearSeries (E := E) (1 + (Fintype.card ι - 1)) :
          (a : (i : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) → F)
        (Finset.piecewise (π := fun (i : Fin (1 + (Fintype.card ι - 1))) ↦ (i : ι) → E i)
          (↑(((fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
                    Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ
                      sorry) ∘
                  (⇑(Fintype.equivFinOfCardEq sorry) : (a : ι) → Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))))
                i) :
            Finset (Fin (1 + (Fintype.card ι - 1))))
          (fun (x_1 : Fin (1 + (Fintype.card ι - 1))) ↦ x) fun (x : Fin (1 + (Fintype.card ι - 1))) ↦ y) :
      F)
Tactic: refine (Fintype.sum_bijective (?_ ∘ Fintype.equivFinOfCardEq (Nat.add_sub_of_le
    Fintype.card_pos).symm) (.comp ?_ <| Equiv.bijective _) _ _ fun i ↦ ?_).symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 ι
⊢ Function.Bijective (β := { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 })
    fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
    Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ ⋯
have right : Function.Surjective (β := { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 })
  fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
  Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ sorry
Tactic: use fun _ _ ↦ (singleton_injective <| compl_injective <| Subtype.ext_iff.mp ·)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
⊢ #sᶜ = 1
have rw : Fintype.card (Fin (1 + (Fintype.card ι - 1))) - #s = 1
Tactic: rw [card_compl, hs, Fintype.card_fin, Nat.add_sub_cancel]