awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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
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 ⋯)))
            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))
⊢ 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))

Tactic:
rw [← sum_comp (Equiv.embeddingEquivOfFinite (Fin n))]

Premises used: Equiv.sum_comp, Equiv.embeddingEquivOfFinite, Fin
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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
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 ⋯)))
              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)
⊢ 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))

Tactic:
congr with σ
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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
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 ⋯)))
          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)
⊢ 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)

Tactic:
congr with i
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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
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) ⋯)))
          ((σ.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))
⊢ (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)

Tactic:
obtain ⟨y, rfl⟩ := σ.equivOfFiniteSelfEmbedding.surjective i

Premises used: Equiv.surjective, rfl, Function.Embedding.equivOfFiniteSelfEmbedding
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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
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) ⋯)))
        ((σ.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:
simp [Function.Embedding.equivOfFiniteSelfEmbedding, g]

Premises used: Function.Embedding.equivOfFiniteSelfEmbedding
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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
rw : s ∩ Metric.eball x r = s
⊢ insert x s ∩ Metric.eball x r = s

Tactic:
rw [Set.insert_eq_of_mem hx]

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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
⊢ s ∩ Metric.eball x r = s

Tactic:
Set.inter_eq_left.2 h's

Premises used: Set.inter_eq_left, Iff.mpr
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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
⊢ s ∩ Metric.eball x r = s

Tactic:
exact Set.inter_eq_left.2 h's

Premises used: Set.inter_eq_left, Iff.mpr
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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

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
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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
apply : AnalyticOn 𝕜 f s
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f s

Tactic:
apply AnalyticOn.contDiffOn _ hs

Premises used: AnalyticOn.contDiffOn
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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
⊢ AnalyticOn 𝕜 f s

Tactic:
simpa [I] using h'
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f s

Tactic:
have fcont : ContDiffOn 𝕜 (↑n) f s := by
    apply AnalyticOn.contDiffOn _ hs
    simpa [I] using h'
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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
apply : ContDiff 𝕜 (F := (i : Fin n) → E) ω fun (z : E) (x_1 : Fin n) ↦ z - x
⊢ ContDiff 𝕜 ω g

Tactic:
apply (p n).contDiff.comp

Premises used: ContinuousMultilinearMap.contDiff, ContDiff.comp
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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 𝕜 (F := (i : Fin n) → E) ω fun (z : E) (x_1 : Fin n) ↦ z - x

Tactic:
contDiff_pi.2 (fun i ↦ contDiff_id.sub contDiff_const)

Premises used: ContDiff.sub, Iff.mpr, contDiff_id, contDiff_const, contDiff_pi
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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 𝕜 (F := (i : Fin n) → E) ω fun (z : E) (x_1 : Fin n) ↦ z - x

Tactic:
exact contDiff_pi.2 (fun i ↦ contDiff_id.sub contDiff_const)

Premises used: ContDiff.sub, Iff.mpr, contDiff_id, contDiff_const, contDiff_pi
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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

Tactic:
have gcont : ContDiff 𝕜 ω g := by
    apply (p n).contDiff.comp
    exact contDiff_pi.2 (fun i ↦ contDiff_id.sub contDiff_const)
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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)
apply₁ : ∀ (m : ℕ), n + 1 ≤ m → q m = 0
⊢ HasFiniteFPowerSeriesOnBall g q x (n + 1) r

Tactic:
apply HasFiniteFPowerSeriesOnBall.mk' _ h.r_pos

Premises used: HasFiniteFPowerSeriesOnBall.mk', HasFPowerSeriesWithinOnBall.r_pos
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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)
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)
⊢ (∑ i ∈ Finset.range (n + 1), (q i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) = g (x + y)

Tactic:
rw [Finset.sum_eq_single_of_mem n]

Premises used: Finset.sum_eq_single_of_mem
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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
⊢ ((q n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) = g (x + y)

Tactic:
simp [q, g]
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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
⊢ n ∈ Finset.range (n + 1)

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
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 : ℕ
hi : i ∈ Finset.range (n + 1)
h'i : i ≠ n
⊢ Eq.{u_3 + 1} (α := F) ((q i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y : F) (0 : F)

Tactic:
simp [q, h'i.symm]

Premises used: Ne.symm