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
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
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
h₁ : HasFPowerSeriesWithinOnBall f p (s ∩ Metric.eball x r) x r
h'₁ : AnalyticOn 𝕜 f (s ∩ Metric.eball x r)
hs₁ : UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)
hx₁ : x ∈ s ∩ Metric.eball x r
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) 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 h's : s ∩ Metric.eball x r ⊆ Metric.eball x r
Tactic: apply HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset
-- 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
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
h' : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDeriv 𝕜 n f 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 simp : ∀ (h : HasFPowerSeriesWithinOnBall f p univ x r),
  Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f univ 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)
Tactic: simp only [← iteratedFDerivWithin_univ, ← hasFPowerSeriesWithinOnBall_univ] at h ⊢
Cleared hypotheses: h
-- 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∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
⊢ 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 this : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
  (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
Tactic: have : iteratedFDerivWithin 𝕜 n f s x
      = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x :=
    (iteratedFDerivWithin_inter_open Metric.isOpen_eball (Metric.mem_eball_self h.r_pos)).symm
-- 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∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) 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 rw : Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) 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)
Tactic: rw [this]
-- 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∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) 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 h₁ : HasFPowerSeriesWithinOnBall f p (s ∩ Metric.eball x r) x r
Tactic: apply HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset
-- 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∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
h₁ : HasFPowerSeriesWithinOnBall f p (s ∩ Metric.eball x r) x r
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) 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 h' : AnalyticOn 𝕜 f (s ∩ Metric.eball x r)
Tactic: apply HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset
-- 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∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
h₁ : HasFPowerSeriesWithinOnBall f p (s ∩ Metric.eball x r) x r
h' : AnalyticOn 𝕜 f (s ∩ Metric.eball x r)
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) 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 hs₁ : UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)
Tactic: apply HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset
-- 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∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
h₁ : HasFPowerSeriesWithinOnBall f p (s ∩ Metric.eball x r) x r
h' : AnalyticOn 𝕜 f (s ∩ Metric.eball x r)
hs₁ : UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) 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 hx₁ : x ∈ s ∩ Metric.eball x r
Tactic: apply HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset
-- 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∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
h₁ : HasFPowerSeriesWithinOnBall f p (s ∩ Metric.eball x r) x r
h' : AnalyticOn 𝕜 f (s ∩ Metric.eball x r)
hs₁ : UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)
hx₁ : x ∈ s ∩ Metric.eball x r
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) 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 h's : s ∩ Metric.eball x r ⊆ Metric.eball x r
Tactic: apply HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset
-- 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∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
⊢ AnalyticOn 𝕜 f (s ∩ Metric.eball x r)
have h' : s ∩ Metric.eball x r ⊆ insert x s ∩ Metric.eball x r
Tactic: apply h.analyticOn.mono
-- 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∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
    (iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x)
⊢ s ∩ Metric.eball x r ⊆ insert x s ∩ Metric.eball x r
have h' : s ∩ Metric.eball x r ⊆ s ∩ Metric.eball x r
Tactic: rw [insert_eq_of_mem hx]
-- 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
x : E
r : ℝ≥0∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
n : ℕ
v : Fin n → E
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDeriv 𝕜 n f 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 simp : ∀ (h : HasFPowerSeriesWithinOnBall f p univ x r),
  Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f univ 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)
Tactic: simp only [← iteratedFDerivWithin_univ, ← hasFPowerSeriesWithinOnBall_univ] at h ⊢
Cleared hypotheses: 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
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) v : F)
have rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (r : ℝ≥0∞) (hp : HasFPowerSeriesWithinOnBall f p s x r),
  Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) v : F)
Tactic: rcases h x hx with ⟨p, r, hp⟩
-- 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
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) v : F)
have rw : Eq.{u_3 + 1} (α := F)
  (∑ σ_1 : Perm (Fin n),
    (p n : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦
      Function.comp (α := Fin n) v ((⇑σ : (a : Fin n) → Fin n) : (a : Fin n) → Fin n)
        ((σ_1 : (a : Fin n) → Fin n) i : Fin n))
  (∑ σ : Perm (Fin n), (p n : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ v ((σ : (a : Fin n) → Fin n) i))
Tactic: rw [hp.iteratedFDerivWithin_eq_sum h hs hx, hp.iteratedFDerivWithin_eq_sum h hs hx]
-- 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
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
| ∑ σ : Perm (Fin n), (p n : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ v ((σ : (a : Fin n) → Fin n) i)
have rw : ∑ i : Perm (Fin n),
  (p n : (a : (i : Fin n) → E) → F) fun (i_1 : Fin n) ↦
    v ((((Equiv.mulLeft σ : (a : Perm (Fin n)) → Perm (Fin n)) i : Perm (Fin n)) : (a : Fin n) → Fin n) i_1)
Tactic: rw [← Equiv.sum_comp (Equiv.mulLeft σ)]
-- 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
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ Eq.{u_3 + 1} (α := F)
    (∑ σ_1 : Perm (Fin n),
      (p n : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦
        Function.comp (α := Fin n) v ((⇑σ : (a : Fin n) → Fin n) : (a : Fin n) → Fin n)
          ((σ_1 : (a : Fin n) → Fin n) i : Fin n))
    (∑ σ : Perm (Fin n), (p n : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ v ((σ : (a : Fin n) → Fin n) i))
have conv_rhs : Eq.{u_3 + 1} (α := F)
  (∑ σ_1 : Perm (Fin n),
    (p n : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦
      Function.comp (α := Fin n) v ((⇑σ : (a : Fin n) → Fin n) : (a : Fin n) → Fin n)
        ((σ_1 : (a : Fin n) → Fin n) i : Fin n))
  (∑ i : Perm (Fin n),
    (p n : (a : (i : Fin n) → E) → F) fun (i_1 : Fin n) ↦
      v ((((Equiv.mulLeft σ : (a : Perm (Fin n)) → Perm (Fin n)) i : Perm (Fin n)) : (a : Fin n) → Fin n) i_1))
Tactic: conv_rhs => rw [← Equiv.sum_comp (Equiv.mulLeft σ)]
-- 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
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
σ : Perm (Fin n)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f s x)) (iteratedFDerivWithin 𝕜 n f s x)
have H : ∀ (x_1 : (i : Fin n) → E),
  Eq.{u_3 + 1} (α := F)
    ((ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f s x) : (a : (i : Fin n) → E) → F) x_1 : F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) x_1 : F)
Tactic: ext
-- 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
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) v : F)
have rcases : ∀ (u : Set E) (u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u) (xu : x ∈ u)
  (hu : ContDiffOn 𝕜 ω f (insert x s ∩ u)),
  Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) v : F)
Tactic: rcases h.contDiffOn' le_rfl (by simp) with ⟨u, u_open, xu, hu⟩
-- 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
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 ω f (insert x s ∩ u)
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) v : F)
have hu₁ : ContDiffOn 𝕜 ω f (s ∩ u)
Tactic: rw [insert_eq_of_mem hx] at hu
Cleared hypotheses: hu
-- 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
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 ω f (s ∩ u)
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) v : F)
have this : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f (s ∩ u) x)
  (iteratedFDerivWithin 𝕜 n f s x)
Tactic: have : iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x :=
    iteratedFDerivWithin_inter_open u_open xu
-- 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
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 ω f (s ∩ u)
this :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f (s ∩ u) x)
    (iteratedFDerivWithin 𝕜 n f s x)
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) v : F)
have rw : Eq.{u_3 + 1} (α := F)
  ((iteratedFDerivWithin 𝕜 n f (s ∩ u) x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
  ((iteratedFDerivWithin 𝕜 n f (s ∩ u) x : (a : (i : Fin n) → E) → F) v : F)
Tactic: rw [← this]
-- 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
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
σ : Perm (Fin n)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f s x)) (iteratedFDerivWithin 𝕜 n f s x)
have H : ∀ (x_1 : (i : Fin n) → E),
  Eq.{u_3 + 1} (α := F)
    ((ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f s x) : (a : (i : Fin n) → E) → F) x_1 : F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) x_1 : F)
Tactic: ext
-- 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
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) v : F)
have rw : Eq.{u_3 + 1} (α := F)
  ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
  ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) v : F)
Tactic: rw [← iteratedFDerivWithin_univ]
-- 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
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
σ : Perm (Fin n)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr σ (iteratedFDeriv 𝕜 n f x)) (iteratedFDeriv 𝕜 n f x)
have rw : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
  (ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f univ x)) (iteratedFDerivWithin 𝕜 n f univ x)
Tactic: rw [← iteratedFDerivWithin_univ]
-- 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
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) v : F)
have rw : Eq.{u_3 + 1} (α := F)
  ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
  ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) v : F)
Tactic: rw [← iteratedFDerivWithin_univ]