awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
f : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi (φ := fun (a : Fin n) ↦ E) fun (i : Fin n) ↦ ContinuousLinearMap.id 𝕜 E
⊢ Eq.{u_3 + 1} (α := F)
    (∑ x_1 : Fin n ↪ Fin n,
      (f : (a : (i : Fin n) → E) → F) fun (j : Fin n) ↦
        if h : ∃ (y : Fin n), (x_1 : (a : Fin n) → Fin n) y = j then
          (g : (a : E) → (i : Fin n) → E)
            (v
              ((x_1.toEquivRange.symm : (a : (↑(range (⇑x_1 : (a : Fin n) → Fin n)) : Type)) → Fin n)
                (Subtype.mk (p := fun (x : Fin n) ↦
                  Membership.mem (γ := Set (Fin n)) (range (ι := Fin n) (⇑x_1 : (a : Fin n) → Fin n)) x) j ⋯)))
            j
        else (g : (a : E) → (i : Fin n) → E) x j)
    (∑ i : Perm (Fin n),
      (f : (a : (i : Fin n) → E) → F) fun (i_1 : Fin n) ↦
        v
          ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n)) i : Perm (Fin n)) : (a : Fin n) → Fin n)
            i_1))
have rw : Eq.{u_3 + 1} (α := F)
  (∑ x_1 : Fin n ↪ Fin n,
    (f : (a : (i : Fin n) → E) → F) fun (j : Fin n) ↦
      if h : ∃ (y : Fin n), (x_1 : (a : Fin n) → Fin n) y = j then
        (g : (a : E) → (i : Fin n) → E)
          (v
            ((x_1.toEquivRange.symm : (a : (↑(range (⇑x_1 : (a : Fin n) → Fin n)) : Type)) → Fin n)
              (Subtype.mk (p := fun (x : Fin n) ↦
                Membership.mem (γ := Set (Fin n)) (range (ι := Fin n) (⇑x_1 : (a : Fin n) → Fin n)) x) j sorry)))
          j
      else (g : (a : E) → (i : Fin n) → E) x j)
  (∑ i : Fin n ↪ Fin n,
    (f : (a : (i : Fin n) → E) → F) fun (i_1 : Fin n) ↦
      v
        ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n))
                ((embeddingEquivOfFinite (Fin n) : (a : Fin n ↪ Fin n) → Fin n ≃ Fin n) i : Fin n ≃ Fin n) :
              Perm (Fin n)) :
            (a : Fin n) → Fin n)
          i_1))
Tactic: rw [← sum_comp (Equiv.embeddingEquivOfFinite (Fin n))]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
f : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi (φ := fun (a : Fin n) ↦ E) fun (i : Fin n) ↦ ContinuousLinearMap.id 𝕜 E
⊢ Eq.{u_3 + 1} (α := F)
    (∑ x_1 : Fin n ↪ Fin n,
      (f : (a : (i : Fin n) → E) → F) fun (j : Fin n) ↦
        if h : ∃ (y : Fin n), (x_1 : (a : Fin n) → Fin n) y = j then
          (g : (a : E) → (i : Fin n) → E)
            (v
              ((x_1.toEquivRange.symm : (a : (↑(range (⇑x_1 : (a : Fin n) → Fin n)) : Type)) → Fin n)
                (Subtype.mk (p := fun (x : Fin n) ↦
                  Membership.mem (γ := Set (Fin n)) (range (ι := Fin n) (⇑x_1 : (a : Fin n) → Fin n)) x) j ⋯)))
            j
        else (g : (a : E) → (i : Fin n) → E) x j)
    (∑ i : Fin n ↪ Fin n,
      (f : (a : (i : Fin n) → E) → F) fun (i_1 : Fin n) ↦
        v
          ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n))
                  ((embeddingEquivOfFinite (Fin n) : (a : Fin n ↪ Fin n) → Fin n ≃ Fin n) i : Fin n ≃ Fin n) :
                Perm (Fin n)) :
              (a : Fin n) → Fin n)
            i_1))
have e_f : ∀ (σ : Fin n ↪ Fin n),
  Eq.{u_3 + 1} (α := F)
    ((f : (a : (i : Fin n) → E) → F) fun (j : Fin n) ↦
        if h : ∃ (y : Fin n), (σ : (a : Fin n) → Fin n) y = j then
          (g : (a : E) → (i : Fin n) → E)
            (v
              ((σ.toEquivRange.symm : (a : (↑(range (⇑σ : (a : Fin n) → Fin n)) : Type)) → Fin n)
                (Subtype.mk (p := fun (x : Fin n) ↦
                  Membership.mem (γ := Set (Fin n)) (range (ι := Fin n) (⇑σ : (a : Fin n) → Fin n)) x) j sorry)))
            j
        else (g : (a : E) → (i : Fin n) → E) x j :
      F)
    ((f : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦
        v
          ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n))
                  ((embeddingEquivOfFinite (Fin n) : (a : Fin n ↪ Fin n) → Fin n ≃ Fin n) σ : Fin n ≃ Fin n) :
                Perm (Fin n)) :
              (a : Fin n) → Fin n)
            i) :
      F)
Tactic: congr with σ
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
f : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi (φ := fun (a : Fin n) ↦ E) fun (i : Fin n) ↦ ContinuousLinearMap.id 𝕜 E
σ : Fin n ↪ Fin n
⊢ Eq.{u_3 + 1} (α := F)
    ((f : (a : (i : Fin n) → E) → F) fun (j : Fin n) ↦
        if h : ∃ (y : Fin n), (σ : (a : Fin n) → Fin n) y = j then
          (g : (a : E) → (i : Fin n) → E)
            (v
              ((σ.toEquivRange.symm : (a : (↑(range (⇑σ : (a : Fin n) → Fin n)) : Type)) → Fin n)
                (Subtype.mk (p := fun (x : Fin n) ↦
                  Membership.mem (γ := Set (Fin n)) (range (ι := Fin n) (⇑σ : (a : Fin n) → Fin n)) x) j ⋯)))
            j
        else (g : (a : E) → (i : Fin n) → E) x j :
      F)
    ((f : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦
        v
          ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n))
                  ((embeddingEquivOfFinite (Fin n) : (a : Fin n ↪ Fin n) → Fin n ≃ Fin n) σ : Fin n ≃ Fin n) :
                Perm (Fin n)) :
              (a : Fin n) → Fin n)
            i) :
      F)
have e_f : ∀ (i : Fin n),
  (if h : ∃ (y : Fin n), (σ : (a : Fin n) → Fin n) y = i then
      (g : (a : E) → (i : Fin n) → E)
        (v
          ((σ.toEquivRange.symm : (a : (↑(range (⇑σ : (a : Fin n) → Fin n)) : Type)) → Fin n)
            (Subtype.mk (p := fun (x : Fin n) ↦
              Membership.mem (γ := Set (Fin n)) (range (ι := Fin n) (⇑σ : (a : Fin n) → Fin n)) x) i sorry)))
        i
    else (g : (a : E) → (i : Fin n) → E) x i) =
    v
      ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n))
              ((embeddingEquivOfFinite (Fin n) : (a : Fin n ↪ Fin n) → Fin n ≃ Fin n) σ : Fin n ≃ Fin n) :
            Perm (Fin n)) :
          (a : Fin n) → Fin n)
        i)
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
f : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi (φ := fun (a : Fin n) ↦ E) fun (i : Fin n) ↦ ContinuousLinearMap.id 𝕜 E
σ : Fin n ↪ Fin n
i : Fin n
⊢ (if h : ∃ (y : Fin n), (σ : (a : Fin n) → Fin n) y = i then
      (g : (a : E) → (i : Fin n) → E)
        (v
          ((σ.toEquivRange.symm : (a : (↑(range (⇑σ : (a : Fin n) → Fin n)) : Type)) → Fin n)
            (Subtype.mk (p := fun (x : Fin n) ↦
              Membership.mem (γ := Set (Fin n)) (range (ι := Fin n) (⇑σ : (a : Fin n) → Fin n)) x) i ⋯)))
        i
    else (g : (a : E) → (i : Fin n) → E) x i) =
    v
      ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n))
              ((embeddingEquivOfFinite (Fin n) : (a : Fin n ↪ Fin n) → Fin n ≃ Fin n) σ : Fin n ≃ Fin n) :
            Perm (Fin n)) :
          (a : Fin n) → Fin n)
        i)
have e_f : ∀ (y : Fin n),
  (if h :
        ∃ (y_1 : Fin n),
          Eq (α := Fin n) ((σ : (a : Fin n) → Fin n) y_1 : Fin n)
            ((σ.equivOfFiniteSelfEmbedding : (a : Fin n) → Fin n) y : Fin n) then
      (g : (a : E) → (i : Fin n) → E)
        (v
          ((σ.toEquivRange.symm : (a : (↑(range (⇑σ : (a : Fin n) → Fin n)) : Type)) → Fin n)
            (Subtype.mk (p := fun (x : Fin n) ↦
              Membership.mem (γ := Set (Fin n)) (range (ι := Fin n) (⇑σ : (a : Fin n) → Fin n)) x)
              ((σ.equivOfFiniteSelfEmbedding : (a : Fin n) → Fin n) y) sorry)))
        ((σ.equivOfFiniteSelfEmbedding : (a : Fin n) → Fin n) y)
    else (g : (a : E) → (i : Fin n) → E) x ((σ.equivOfFiniteSelfEmbedding : (a : Fin n) → Fin n) y)) =
    v
      ((((Equiv.inv (Perm (Fin n)) : (a : Perm (Fin n)) → Perm (Fin n))
              ((embeddingEquivOfFinite (Fin n) : (a : Fin n ↪ Fin n) → Fin n ≃ Fin n) σ : Fin n ≃ Fin n) :
            Perm (Fin n)) :
          (a : Fin n) → Fin n)
        ((σ.equivOfFiniteSelfEmbedding : (a : Fin n) → Fin n) y))
Tactic: obtain ⟨y, rfl⟩ := σ.equivOfFiniteSelfEmbedding.surjective i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
⊢ insert x s ∩ Metric.eball x r = s
have rw : s ∩ Metric.eball x r = s
Tactic: rw [Set.insert_eq_of_mem hx]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) v : F)
    (∑ σ : Perm (Fin n), (p n : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ v ((σ : (a : Fin n) → Fin n) i) : F)
have I : insert x s ∩ Metric.eball x r = s
Tactic: have I : insert x s ∩ Metric.eball x r = s := by
    rw [Set.insert_eq_of_mem hx]
    exact Set.inter_eq_left.2 h's
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) v : F)
    (∑ σ : Perm (Fin n), (p n : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ v ((σ : (a : Fin n) → Fin n) i) : F)
have fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
Tactic: have fcont : ContDiffOn 𝕜 (↑n) f s := by
    apply AnalyticOn.contDiffOn _ hs
    simpa [I] using h'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
⊢ ContDiff 𝕜 ω g
have apply : ContDiff 𝕜 (F := (i : Fin n) → E) ω fun (z : E) (x_1 : Fin n) ↦ z - x
Tactic: apply (p n).contDiff.comp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) v : F)
    (∑ σ : Perm (Fin n), (p n : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ v ((σ : (a : Fin n) → Fin n) i) : F)
have gcont : ContDiff 𝕜 ω g
Tactic: have gcont : ContDiff 𝕜 ω g := by
    apply (p n).contDiff.comp
    exact contDiff_pi.2 (fun i ↦ contDiff_id.sub contDiff_const)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
⊢ HasFiniteFPowerSeriesOnBall g q x (n + 1) r
have apply : ∀ (y : E),
  Membership.mem (γ := Set E) (Metric.eball 0 r) y →
    (∑ i ∈ Finset.range (n + 1), (q i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) = g (x + y)
Tactic: apply HasFiniteFPowerSeriesOnBall.mk' _ h.r_pos
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
apply :
  ∀ (y : E),
    Membership.mem (γ := Set E) (Metric.eball 0 r) y →
      (∑ i ∈ Finset.range (n + 1), (q i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) = g (x + y)
⊢ HasFiniteFPowerSeriesOnBall g q x (n + 1) r
have apply₁ : ∀ (m : ℕ), n + 1 ≤ m → q m = 0
Tactic: apply HasFiniteFPowerSeriesOnBall.mk' _ h.r_pos
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ (∑ i ∈ Finset.range (n + 1), (q i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) = g (x + y)
have rw : ((q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) = g (x + y)
Tactic: rw [Finset.sum_eq_single_of_mem n]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
rw : ((q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) = g (x + y)
⊢ (∑ i ∈ Finset.range (n + 1), (q i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) = g (x + y)
have h₁ : n ∈ Finset.range (n + 1)
Tactic: rw [Finset.sum_eq_single_of_mem n]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
rw : ((q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) = g (x + y)
h₁ : n ∈ Finset.range (n + 1)
⊢ (∑ i ∈ Finset.range (n + 1), (q i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) = g (x + y)
have h₀ : ∀ b ∈ Finset.range (n + 1),
  b ≠ n → Eq.{u_3 + 1} (α := F) ((q b : (a : (i : Fin b) → E) → F) fun (x : Fin b) ↦ y : F) (0 : F)
Tactic: rw [Finset.sum_eq_single_of_mem n]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
m : ℕ
hm : n + 1 ≤ m
⊢ q m = 0
have this : n ≠ m
Tactic: have : n ≠ m := by lia
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) v : F)
    (∑ σ : Perm (Fin n), (p n : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ v ((σ : (a : Fin n) → Fin n) i) : F)
have A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
Tactic: have A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r := by
    apply HasFiniteFPowerSeriesOnBall.mk' _ h.r_pos
    · intro y hy
      rw [Finset.sum_eq_single_of_mem n]
      · simp [q, g]
      · simp
      · intro i hi h'i
        simp [q, h'i.symm]
    · intro m hm
      have : n ≠ m := by lia
      simp [q, this]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) v : F)
    (∑ σ : Perm (Fin n), (p n : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ v ((σ : (a : Fin n) → Fin n) i) : F)
have B : HasFPowerSeriesWithinOnBall g q s x r
Tactic: have B : HasFPowerSeriesWithinOnBall g q s x r :=
    A.toHasFPowerSeriesOnBall.hasFPowerSeriesWithinOnBall
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s
g : E → F := fun (z : E) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F :=
  fun (k : ℕ) ↦
    if h : n = k then
      Eq.rec (motive := fun (x : ℕ) (h : n = x) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin x) ↦ E) F)
        (p n) h
    else 0
A : HasFiniteFPowerSeriesOnBall g q x (n + 1) r
B : HasFPowerSeriesWithinOnBall g q s x r
⊢ iteratedFDerivWithin 𝕜 n f s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n g s x) (iteratedFDerivWithin 𝕜 n (f - g) s x)
have this : f = g + (f - g)
Tactic: have : f = g + (f - g) := by abel