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
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)
⊢ HasFPowerSeriesWithinOnBall f p (s ∩ Metric.eball x r) x r

Tactic:
exact h.mono inter_subset_left

Premises used: Set.inter_subset_left, HasFPowerSeriesWithinOnBall.mono
-- 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∞
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' : s ∩ Metric.eball x r ⊆ insert x s ∩ Metric.eball x r
⊢ AnalyticOn 𝕜 f (s ∩ Metric.eball x r)

Tactic:
apply h.analyticOn.mono

Premises used: HasFPowerSeriesWithinOnBall.analyticOn, AnalyticOn.mono
-- 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∞
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' h'₁ : s ∩ Metric.eball x r ⊆ s ∩ Metric.eball x r
⊢ s ∩ Metric.eball x r ⊆ insert x s ∩ Metric.eball x r

Tactic:
rw [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∞
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)
⊢ UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)

Tactic:
hs.inter Metric.isOpen_eball

Premises used: Metric.isOpen_eball, UniqueDiffOn.inter
-- 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∞
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)
⊢ UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)

Tactic:
exact hs.inter Metric.isOpen_eball

Premises used: Metric.isOpen_eball, UniqueDiffOn.inter
-- 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∞
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)
⊢ x ∈ s ∩ Metric.eball x r

Tactic:
⟨hx, Metric.mem_eball_self h.r_pos⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro, HasFPowerSeriesWithinOnBall.r_pos, Metric.mem_eball_self
-- 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∞
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)
⊢ x ∈ s ∩ Metric.eball x r

Tactic:
exact ⟨hx, Metric.mem_eball_self h.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∞
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 ⊆ Metric.eball x r

Tactic:
inter_subset_right

Premises used: Set.inter_subset_right
-- 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∞
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 ⊆ Metric.eball x r

Tactic:
exact inter_subset_right

Premises used: Set.inter_subset_right
-- 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
x : E
r : ℝ≥0∞
inst_5 : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
n : ℕ
v : Fin n → E
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)
⊢ 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)

Tactic:
simp only [← iteratedFDerivWithin_univ, ← hasFPowerSeriesWithinOnBall_univ] at h ⊢

Premises used: hasFPowerSeriesWithinOnBall_univ, iteratedFDerivWithin_univ
-- 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
x : E
r : ℝ≥0∞
inst_5 : CompleteSpace F
n : ℕ
v : Fin n → E
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:
h.iteratedFDerivWithin_eq_sum_of_completeSpace uniqueDiffOn_univ (mem_univ _) v

Premises used: uniqueDiffOn_univ, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_completeSpace, Set.mem_univ
-- 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
x : E
r : ℝ≥0∞
inst_5 : CompleteSpace F
n : ℕ
v : Fin n → E
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:
exact h.iteratedFDerivWithin_eq_sum_of_completeSpace uniqueDiffOn_univ (mem_univ _) v

Premises used: uniqueDiffOn_univ, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_completeSpace, Set.mem_univ
-- 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
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
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)
⊢ 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⟩
-- 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
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
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))
⊢ 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:
rw [hp.iteratedFDerivWithin_eq_sum h hs hx, hp.iteratedFDerivWithin_eq_sum h hs hx]

Premises used: HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum
-- 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
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
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)
| ∑ σ : Perm (Fin n), (p n : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ v ((σ : (a : Fin n) → Fin n) i)

Tactic:
rw [← Equiv.sum_comp (Equiv.mulLeft σ)]

Premises used: Equiv.sum_comp, Equiv.mulLeft
-- 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
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
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))
⊢ 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:
conv_rhs => rw [← Equiv.sum_comp (Equiv.mulLeft σ)]

Premises used: Equiv.sum_comp, Equiv.mulLeft
-- 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
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))
    (∑ 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:
simp only [coe_mulLeft, Perm.coe_mul, Function.comp_apply]

Premises used: Equiv.Perm.coe_mul, Equiv.coe_mulLeft, Function.comp_apply
-- 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
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
σ : Perm (Fin n)
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)
⊢ 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)

Tactic:
ext
-- 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
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
σ : Perm (Fin n)
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:
h.iteratedFDerivWithin_comp_perm hs hx _ _

Premises used: AnalyticOn.iteratedFDerivWithin_comp_perm
-- 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
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
σ : Perm (Fin n)
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:
exact h.iteratedFDerivWithin_comp_perm hs hx _ _

Premises used: AnalyticOn.iteratedFDerivWithin_comp_perm
-- 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
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 (α := ℕ∞ω) ω ∞ → Eq (α := ℕ∞ω) ω ω

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
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
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)
⊢ 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⟩

Premises used: le_rfl, ContDiffWithinAt.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
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)
⊢ ContDiffOn 𝕜 ω f (s ∩ u)

Tactic:
rw [insert_eq_of_mem hx] at hu

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
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 (α := 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
-- 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
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)
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)
⊢ 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:
rw [← this]
-- 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
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 ∩ 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:
AnalyticOn.iteratedFDerivWithin_comp_perm hu.analyticOn (hs.inter u_open) ⟨hx, xu⟩ _ _

Premises used: AnalyticOn.iteratedFDerivWithin_comp_perm, ContDiffOn.analyticOn, And.intro, UniqueDiffOn.inter
-- 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
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 ∩ 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:
exact AnalyticOn.iteratedFDerivWithin_comp_perm hu.analyticOn (hs.inter u_open) ⟨hx, xu⟩ _ _

Premises used: AnalyticOn.iteratedFDerivWithin_comp_perm, ContDiffOn.analyticOn, And.intro, UniqueDiffOn.inter
-- 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
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
σ : Perm (Fin n)
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)
⊢ 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)

Tactic:
ext