awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (hypothesis)
Goal:
ι : Type u_4
inst : DecidableEq ι
n : ℕ
e : Fin (n + 1) ↪ ι
j : Fin (n + 1)
h'k :
  Membership.mem (α := ι) (γ := Set ι)
    (range (ι := Fin n)
      (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
            ((Equiv.embeddingFinSucc n ι :
                (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
              e)) :
        (a : Fin n) → ι))
    ((e : (a : Fin (n + 1)) → ι) j : ι)
hj : j ≠ 0
⊢ Fin.succ
      (((Equiv.symm
              (Function.Embedding.toEquivRange
                (Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                  ((Equiv.embeddingFinSucc n ι :
                      (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                    e))) :
            (↑(range (ι := Fin n)
                    (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                          ((Equiv.embeddingFinSucc n ι :
                              (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                            e)) :
                      (a : Fin n) → ι)) :
                Type u_4) ≃
              Fin n) :
          (a :
              (↑(range
                    (⇑((Equiv.embeddingFinSucc n ι :
                              (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                            e).fst :
                      (a : Fin n) → ι)) :
                Type u_4)) →
            Fin n)
        (Subtype.mk (p := fun (x : ι) ↦
          Membership.mem (γ := Set ι)
            (range (ι := Fin n)
              (⇑(Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
                    ((Equiv.embeddingFinSucc n ι :
                        (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
                      e)) :
                (a : Fin n) → ι))
            x)
          ((e : (a : Fin (n + 1)) → ι) j) h'k)) =
    j
have this : Eq (α := ι) ((e : (a : Fin (n + 1)) → ι) j : ι)
  ((Sigma.fst (β := fun (e : Fin n ↪ ι) ↦ { i : ι // i ∉ range (ι := Fin n) (⇑e : (a : Fin n) → ι) })
          ((Equiv.embeddingFinSucc n ι :
              (a : Fin (n + 1) ↪ ι) → (e : Fin n ↪ ι) × { i : ι // i ∉ range (⇑e : (a : Fin n) → ι) })
            e) :
        (a : Fin n) → ι)
      (j.pred hj) :
    ι)
Tactic: have : e j = (Equiv.embeddingFinSucc n ι e).1 (Fin.pred j hj) := by simp
-- 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
n : ℕ
x : (i : ι) → E i
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ (i : ι) → E i) F)
      (iteratedFDeriv 𝕜 n (⇑f : (a : (i : ι) → E i) → F) x) ≤
    (↑((Fintype.card ι).descFactorial n) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)
have rw : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ (i : ι) → E i) F) (f.iteratedFDeriv (E₁ := E) n x) ≤
  (↑((Fintype.card ι).descFactorial n) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n)
Tactic: rw [f.iteratedFDeriv_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
⊢ ((p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x_1 : Fin n) ↦ x : (a : E) → F) x =
    HSMul.hSMul (β := F) (n + 1) ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_1 : Fin (n + 1)) ↦ x : F)
have simp : ∑ x_1 : { s : Finset (Fin (1 + n)) // s.card = n },
    ((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) sorry :
            (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
          fun (x_2 : Fin n) ↦ x :
        (a : (i : Fin 1) → E) → F)
      (Fin.snoc (α := fun (i : Fin 1) ↦ E) ![] x) =
  HSMul.hSMul (β := F) (n + 1) ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_1 : Fin (n + 1)) ↦ x : F)
Tactic: simp only [derivSeries, compFormalMultilinearSeries_apply, changeOriginSeries,
    compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_coe,
    Function.comp_apply, ContinuousMultilinearMap.sum_apply, map_sum, coe_sum', Finset.sum_apply,
    continuousMultilinearCurryFin1_apply, Matrix.zero_empty]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
⊢ ∑ x_1 : { s : Finset (Fin (1 + n)) // s.card = n },
      ((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
              (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
            fun (x_2 : Fin n) ↦ x :
          (a : (i : Fin 1) → E) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ E) ![] x) =
    HSMul.hSMul (β := F) (n + 1) ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_1 : Fin (n + 1)) ↦ x : F)
have h : ∀ (x_1 : { s : Finset (Fin (1 + n)) // s.card = n }),
  Membership.mem (γ := Finset { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ x_1 →
    Eq.{v + 1} (α := F)
      (((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) sorry :
                (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
              fun (x_2 : Fin n) ↦ x :
            (a : (i : Fin 1) → E) → F)
          (Fin.snoc (α := fun (i : Fin 1) ↦ E) ![] x) :
        F)
      ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
Tactic: convert! Finset.sum_const _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
h :
  ∀ (x_1 : { s : Finset (Fin (1 + n)) // s.card = n }),
    Membership.mem (γ := Finset { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ x_1 →
      Eq.{v + 1} (α := F)
        (((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
                  (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
                fun (x_2 : Fin n) ↦ x :
              (a : (i : Fin 1) → E) → F)
            (Fin.snoc (α := fun (i : Fin 1) ↦ E) ![] x) :
          F)
        ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
⊢ ∑ x_1 : { s : Finset (Fin (1 + n)) // s.card = n },
      ((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
              (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
            fun (x_2 : Fin n) ↦ x :
          (a : (i : Fin 1) → E) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ E) ![] x) =
    HSMul.hSMul (β := F) (n + 1) ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_1 : Fin (n + 1)) ↦ x : F)
have h₁ : n + 1 = Finset.card (α := { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ
Tactic: convert! Finset.sum_const _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
x_1 : { s : Finset (Fin (1 + n)) // s.card = n }
h : Membership.mem (γ := Finset { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ x_1
⊢ Eq.{v + 1} (α := F)
    (((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
              (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
            fun (x_2 : Fin n) ↦ x :
          (a : (i : Fin 1) → E) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ E) ![] x) :
      F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
have h : Eq.{v + 1} (α := F)
  (((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) sorry :
            (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
          fun (x_2 : Fin n) ↦ x :
        (a : (i : Fin 1) → E) → F)
      fun (x_2 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ x :
    F)
  ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
Tactic: rw [Fin.snoc_zero, changeOriginSeriesTerm_apply, Finset.piecewise_same, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
x_1 : { s : Finset (Fin (1 + n)) // s.card = n }
h_1 : Membership.mem (γ := Finset { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ x_1
h :
  Eq.{v + 1} (α := F)
    (((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
              (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
            fun (x_2 : Fin n) ↦ x :
          (a : (i : Fin 1) → E) → F)
        fun (x_2 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ x :
      F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
⊢ Eq.{v + 1} (α := F)
    (((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
              (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
            fun (x_2 : Fin n) ↦ x :
          (a : (i : Fin 1) → E) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ E) ![] x) :
      F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
have h₁ : Eq.{v + 1} (α := F)
  ((p (1 + n) : (a : (i : Fin (1 + n)) → E) → F)
      ((↑x_1 : Finset (Fin (1 + n))).piecewise (π := fun (i : Fin (1 + n)) ↦ E) (fun (x_2 : Fin (1 + n)) ↦ x)
        fun (x_2 : Fin (1 + n)) ↦ x) :
    F)
  ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
Tactic: rw [Fin.snoc_zero, changeOriginSeriesTerm_apply, Finset.piecewise_same, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
x_1 : { s : Finset (Fin (1 + n)) // s.card = n }
h_1 : Membership.mem (γ := Finset { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ x_1
h :
  Eq.{v + 1} (α := F)
    (((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
              (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
            fun (x_2 : Fin n) ↦ x :
          (a : (i : Fin 1) → E) → F)
        fun (x_2 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ x :
      F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
h₁ :
  Eq.{v + 1} (α := F)
    ((p (1 + n) : (a : (i : Fin (1 + n)) → E) → F)
        ((↑x_1 : Finset (Fin (1 + n))).piecewise (π := fun (i : Fin (1 + n)) ↦ E) (fun (x_2 : Fin (1 + n)) ↦ x)
          fun (x_2 : Fin (1 + n)) ↦ x) :
      F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
⊢ Eq.{v + 1} (α := F)
    (((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
              (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
            fun (x_2 : Fin n) ↦ x :
          (a : (i : Fin 1) → E) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ E) ![] x) :
      F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
have h₂ : Eq.{v + 1} (α := F) ((p (1 + n) : (a : (i : Fin (1 + n)) → E) → F) fun (x_2 : Fin (1 + n)) ↦ x : F)
  ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
Tactic: rw [Fin.snoc_zero, changeOriginSeriesTerm_apply, Finset.piecewise_same, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
x_1 : { s : Finset (Fin (1 + n)) // s.card = n }
h_1 : Membership.mem (γ := Finset { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ x_1
h :
  Eq.{v + 1} (α := F)
    (((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
              (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
            fun (x_2 : Fin n) ↦ x :
          (a : (i : Fin 1) → E) → F)
        fun (x_2 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ x :
      F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
h₁ :
  Eq.{v + 1} (α := F)
    ((p (1 + n) : (a : (i : Fin (1 + n)) → E) → F)
        ((↑x_1 : Finset (Fin (1 + n))).piecewise (π := fun (i : Fin (1 + n)) ↦ E) (fun (x_2 : Fin (1 + n)) ↦ x)
          fun (x_2 : Fin (1 + n)) ↦ x) :
      F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
h₂ :
  Eq.{v + 1} (α := F) ((p (1 + n) : (a : (i : Fin (1 + n)) → E) → F) fun (x_2 : Fin (1 + n)) ↦ x : F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
⊢ Eq.{v + 1} (α := F)
    (((p.changeOriginSeriesTerm 1 n (↑x_1 : Finset (Fin (1 + n))) ⋯ :
              (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
            fun (x_2 : Fin n) ↦ x :
          (a : (i : Fin 1) → E) → F)
        (Fin.snoc (α := fun (i : Fin 1) ↦ E) ![] x) :
      F)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
have h₃ : Eq.{v + 1} (α := F) ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
  ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x_2 : Fin (n + 1)) ↦ x : F)
Tactic: rw [Fin.snoc_zero, changeOriginSeriesTerm_apply, Finset.piecewise_same, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
⊢ n + 1 = Finset.card (α := { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ
have h : n + 1 = card { s : Finset (Fin (1 + n)) // s.card = n }
Tactic: rw [← card, card_subtype, ← Finset.powerset_univ, ← Finset.powersetCard_eq_filter,
      Finset.card_powersetCard, ← card, card_fin, eq_comm, add_comm, Nat.choose_succ_self_right]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
h : n + 1 = card { s : Finset (Fin (1 + n)) // s.card = n }
⊢ n + 1 = Finset.card (α := { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ
have h₁ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) {x : Finset (Fin (1 + n)) | x.card = n}
Tactic: rw [← card, card_subtype, ← Finset.powerset_univ, ← Finset.powersetCard_eq_filter,
      Finset.card_powersetCard, ← card, card_fin, eq_comm, add_comm, Nat.choose_succ_self_right]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
h : n + 1 = card { s : Finset (Fin (1 + n)) // s.card = n }
h₁ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) {x : Finset (Fin (1 + n)) | x.card = n}
⊢ n + 1 = Finset.card (α := { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ
have h₂ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) ({x ∈ Finset.powerset Finset.univ | x.card = n})
Tactic: rw [← card, card_subtype, ← Finset.powerset_univ, ← Finset.powersetCard_eq_filter,
      Finset.card_powersetCard, ← card, card_fin, eq_comm, add_comm, Nat.choose_succ_self_right]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
h : n + 1 = card { s : Finset (Fin (1 + n)) // s.card = n }
h₁ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) {x : Finset (Fin (1 + n)) | x.card = n}
h₂ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) ({x ∈ Finset.powerset Finset.univ | x.card = n})
⊢ n + 1 = Finset.card (α := { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ
have h₃ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) (Finset.powersetCard n Finset.univ)
Tactic: rw [← card, card_subtype, ← Finset.powerset_univ, ← Finset.powersetCard_eq_filter,
      Finset.card_powersetCard, ← card, card_fin, eq_comm, add_comm, Nat.choose_succ_self_right]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
h : n + 1 = card { s : Finset (Fin (1 + n)) // s.card = n }
h₁ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) {x : Finset (Fin (1 + n)) | x.card = n}
h₂ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) ({x ∈ Finset.powerset Finset.univ | x.card = n})
h₃ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) (Finset.powersetCard n Finset.univ)
⊢ n + 1 = Finset.card (α := { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ
have h₄ : n + 1 = (Finset.card (α := Fin (1 + n)) Finset.univ).choose n
Tactic: rw [← card, card_subtype, ← Finset.powerset_univ, ← Finset.powersetCard_eq_filter,
      Finset.card_powersetCard, ← card, card_fin, eq_comm, add_comm, Nat.choose_succ_self_right]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
h : n + 1 = card { s : Finset (Fin (1 + n)) // s.card = n }
h₁ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) {x : Finset (Fin (1 + n)) | x.card = n}
h₂ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) ({x ∈ Finset.powerset Finset.univ | x.card = n})
h₃ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) (Finset.powersetCard n Finset.univ)
h₄ : n + 1 = (Finset.card (α := Fin (1 + n)) Finset.univ).choose n
⊢ n + 1 = Finset.card (α := { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ
have h₅ : n + 1 = (card (Fin (1 + n))).choose n
Tactic: rw [← card, card_subtype, ← Finset.powerset_univ, ← Finset.powersetCard_eq_filter,
      Finset.card_powersetCard, ← card, card_fin, eq_comm, add_comm, Nat.choose_succ_self_right]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
h : n + 1 = card { s : Finset (Fin (1 + n)) // s.card = n }
h₁ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) {x : Finset (Fin (1 + n)) | x.card = n}
h₂ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) ({x ∈ Finset.powerset Finset.univ | x.card = n})
h₃ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) (Finset.powersetCard n Finset.univ)
h₄ : n + 1 = (Finset.card (α := Fin (1 + n)) Finset.univ).choose n
h₅ : n + 1 = (card (Fin (1 + n))).choose n
⊢ n + 1 = Finset.card (α := { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ
have h₆ : n + 1 = (1 + n).choose n
Tactic: rw [← card, card_subtype, ← Finset.powerset_univ, ← Finset.powersetCard_eq_filter,
      Finset.card_powersetCard, ← card, card_fin, eq_comm, add_comm, Nat.choose_succ_self_right]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
h : n + 1 = card { s : Finset (Fin (1 + n)) // s.card = n }
h₁ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) {x : Finset (Fin (1 + n)) | x.card = n}
h₂ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) ({x ∈ Finset.powerset Finset.univ | x.card = n})
h₃ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) (Finset.powersetCard n Finset.univ)
h₄ : n + 1 = (Finset.card (α := Fin (1 + n)) Finset.univ).choose n
h₅ : n + 1 = (card (Fin (1 + n))).choose n
h₆ : n + 1 = (1 + n).choose n
⊢ n + 1 = Finset.card (α := { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ
have h₇ : (1 + n).choose n = n + 1
Tactic: rw [← card, card_subtype, ← Finset.powerset_univ, ← Finset.powersetCard_eq_filter,
      Finset.card_powersetCard, ← card, card_fin, eq_comm, add_comm, Nat.choose_succ_self_right]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
h : n + 1 = card { s : Finset (Fin (1 + n)) // s.card = n }
h₁ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) {x : Finset (Fin (1 + n)) | x.card = n}
h₂ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) ({x ∈ Finset.powerset Finset.univ | x.card = n})
h₃ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) (Finset.powersetCard n Finset.univ)
h₄ : n + 1 = (Finset.card (α := Fin (1 + n)) Finset.univ).choose n
h₅ : n + 1 = (card (Fin (1 + n))).choose n
h₆ : n + 1 = (1 + n).choose n
h₇ : (1 + n).choose n = n + 1
⊢ n + 1 = Finset.card (α := { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ
have h₈ : (n + 1).choose n = n + 1
Tactic: rw [← card, card_subtype, ← Finset.powerset_univ, ← Finset.powersetCard_eq_filter,
      Finset.card_powersetCard, ← card, card_fin, eq_comm, add_comm, Nat.choose_succ_self_right]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
h : n + 1 = card { s : Finset (Fin (1 + n)) // s.card = n }
h₁ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) {x : Finset (Fin (1 + n)) | x.card = n}
h₂ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) ({x ∈ Finset.powerset Finset.univ | x.card = n})
h₃ : n + 1 = Finset.card (α := Finset (Fin (1 + n))) (Finset.powersetCard n Finset.univ)
h₄ : n + 1 = (Finset.card (α := Fin (1 + n)) Finset.univ).choose n
h₅ : n + 1 = (card (Fin (1 + n))).choose n
h₆ : n + 1 = (1 + n).choose n
h₇ : (1 + n).choose n = n + 1
h₈ : (n + 1).choose n = n + 1
⊢ n + 1 = Finset.card (α := { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ
have h₉ : n + 1 = n + 1
Tactic: rw [← card, card_subtype, ← Finset.powerset_univ, ← Finset.powersetCard_eq_filter,
      Finset.card_powersetCard, ← card, card_fin, eq_comm, add_comm, Nat.choose_succ_self_right]