awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
x : E
i : ℕ
f : E → F
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
zero :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 (-f) s x)
      (-iteratedFDerivWithin 𝕜 0 f s x)
zero₁ :
  ∀ {x : E} (hx : x ∈ s) (h : (i : Fin 0) → E),
    Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 0 (-f) s x : (a : (i : Fin 0) → E) → F) h : F)
      ((-iteratedFDerivWithin 𝕜 0 f s x : (a : (i : Fin 0) → E) → F) h : F)
succ :
  ∀ (i : ℕ)
    (hi :
      ∀ {x : E} (hx : x ∈ s),
        Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
          (iteratedFDerivWithin 𝕜 i (-f) s x) (-iteratedFDerivWithin 𝕜 i f s x))
    {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
      (iteratedFDerivWithin 𝕜 (i + 1) (-f) s x) (-iteratedFDerivWithin 𝕜 (i + 1) f s x)
succ₁ :
  ∀ (i : ℕ)
    (hi :
      ∀ {x : E} (hx : x ∈ s),
        Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
          (iteratedFDerivWithin 𝕜 i (-f) s x) (-iteratedFDerivWithin 𝕜 i f s x))
    {x : E} (hx : x ∈ s) (h : (i : Fin (i + 1)) → E),
    Eq.{uF + 1} (α := F) ((iteratedFDerivWithin 𝕜 (i + 1) (-f) s x : (a : (i : Fin (i + 1)) → E) → F) h : F)
      ((-iteratedFDerivWithin 𝕜 (i + 1) f s x : (a : (i : Fin (i + 1)) → E) → F) h : F)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) s x)
    (-iteratedFDerivWithin 𝕜 i f s x)

Tactic:
induction i generalizing x with ext h
  | zero => simp
  | succ i hi =>
    calc
      iteratedFDerivWithin 𝕜 (i + 1) (-f) s x h =
          fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x (h 0) (Fin.tail h) :=
        iteratedFDerivWithin_succ_apply_left _
      _ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
        rw [fderivWithin_congr' (@hi) hx, Pi.neg_def]
      _ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
        rw [fderivWithin_neg (hu x hx), ContinuousLinearMap.neg_apply,
          ContinuousMultilinearMap.neg_apply]
      _ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := by
        rw [iteratedFDerivWithin_succ_apply_left]

Premises used: Fin.succ, iteratedFDerivWithin_succ_apply_left
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
i : ℕ
f : E → F
simp_rw :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) univ x)
    (-iteratedFDerivWithin 𝕜 i f univ x)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i (-f) x)
    (-iteratedFDeriv 𝕜 i f x)

Tactic:
simp_rw [← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
i : ℕ
f : E → F
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) univ x)
    (-iteratedFDerivWithin 𝕜 i f univ x)

Tactic:
iteratedFDerivWithin_neg_apply uniqueDiffOn_univ (Set.mem_univ _)

Premises used: iteratedFDerivWithin_neg_apply, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
i : ℕ
f : E → F
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin 𝕜 i (-f) univ x)
    (-iteratedFDerivWithin 𝕜 i f univ x)

Tactic:
exact iteratedFDerivWithin_neg_apply uniqueDiffOn_univ (Set.mem_univ _)

Premises used: iteratedFDerivWithin_neg_apply, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
i : ℕ
f : E → F
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i (-f))
    (-iteratedFDeriv 𝕜 i f)

Tactic:
funext fun _ ↦ iteratedFDeriv_neg_apply

Premises used: iteratedFDeriv_neg_apply, funext
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
s : Set E
f g : E → F
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f x - g x) s x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: ContDiffWithinAt.add, sub_eq_add_neg, ContDiffWithinAt.neg
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
f g : E → F
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
⊢ ContDiffAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f x - g x) x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: ContDiffAt.add, sub_eq_add_neg, ContDiffAt.neg
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
s : Set E
f g : E → F
hf : ContDiffOn 𝕜 n f s
hg : ContDiffOn 𝕜 n g s
⊢ ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f x - g x) s

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: ContDiffOn.add, sub_eq_add_neg, ContDiffOn.neg
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
f g : E → F
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
⊢ ContDiff.{u_1, uE, uF} 𝕜 (F := F) n fun (x : E) ↦ f x - g x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: sub_eq_add_neg, ContDiff.add, ContDiff.neg
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x
hg : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
rw : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (-g) s x
⊢ iteratedFDerivWithin 𝕜 i (f - g) s x =
    HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s x) (iteratedFDerivWithin 𝕜 i g s x)

Tactic:
rw [sub_eq_add_neg, iteratedFDerivWithin_add_apply hf _ hu hx,
    iteratedFDerivWithin_neg_apply hu hx, sub_eq_add_neg]

Premises used: iteratedFDerivWithin_neg_apply, sub_eq_add_neg, iteratedFDerivWithin_add_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x
hg : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (-g) s x

Tactic:
hg.neg

Premises used: ContDiffWithinAt.neg
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x
hg : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (-g) s x

Tactic:
exact hg.neg

Premises used: ContDiffWithinAt.neg
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
i : ℕ
f g : E → F
hf : ContDiffAt 𝕜 (↑i : ℕ∞ω) f x
hg : ContDiffAt 𝕜 (↑i : ℕ∞ω) g x
simp_rw :
  iteratedFDerivWithin 𝕜 i (f - g) univ x =
    HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f univ x) (iteratedFDerivWithin 𝕜 i g univ x)
⊢ iteratedFDeriv 𝕜 i (f - g) x =
    HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i f x)
      (iteratedFDeriv 𝕜 i g x)

Tactic:
simp_rw [← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
i : ℕ
f g : E → F
hf : ContDiffAt 𝕜 (↑i : ℕ∞ω) f x
hg : ContDiffAt 𝕜 (↑i : ℕ∞ω) g x
⊢ iteratedFDerivWithin 𝕜 i (f - g) univ x =
    HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f univ x) (iteratedFDerivWithin 𝕜 i g univ x)

Tactic:
iteratedFDerivWithin_sub_apply hf hg uniqueDiffOn_univ (Set.mem_univ _)

Premises used: uniqueDiffOn_univ, Set.mem_univ, iteratedFDerivWithin_sub_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
i : ℕ
f g : E → F
hf : ContDiffAt 𝕜 (↑i : ℕ∞ω) f x
hg : ContDiffAt 𝕜 (↑i : ℕ∞ω) g x
⊢ iteratedFDerivWithin 𝕜 i (f - g) univ x =
    HSub.hSub (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f univ x) (iteratedFDerivWithin 𝕜 i g univ x)

Tactic:
exact iteratedFDerivWithin_sub_apply hf hg uniqueDiffOn_univ (Set.mem_univ _)

Premises used: uniqueDiffOn_univ, Set.mem_univ, iteratedFDerivWithin_sub_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
i : ℕ
f g : E → F
hf : ContDiff 𝕜 (↑i : ℕ∞ω) f
hg : ContDiff 𝕜 (↑i : ℕ∞ω) g
⊢ iteratedFDeriv 𝕜 i (f - g) =
    HSub.hSub (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i f)
      (iteratedFDeriv 𝕜 i g)

Tactic:
funext fun _ ↦ iteratedFDeriv_sub_apply (ContDiff.contDiffAt hf) (ContDiff.contDiffAt hg)

Premises used: funext, iteratedFDeriv_sub_apply, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
t : Set E
x : E
h :
  ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ ∅, f i x) t x

Tactic:
simp [contDiffWithinAt_const]

Premises used: contDiffWithinAt_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
t : Set E
x : E
i : ι
s : Finset ι
is : i ∉ s
IH :
  ∀ (h : ∀ i ∈ s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x),
    ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t x
h : ∀ i_1 ∈ Insert.insert i s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i_1 x) t x
insert : ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x + ∑ i ∈ s, f i x) t x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ Insert.insert i s, f i x) t x

Tactic:
simp only [is, Finset.sum_insert, not_false_iff]

Premises used: Finset.sum_insert, not_false_iff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
t : Set E
x : E
i : ι
s : Finset ι
is : i ∉ s
IH :
  ∀ (h : ∀ i ∈ s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x),
    ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t x
h : ∀ i_1 ∈ insert i s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i_1 x) t x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x + ∑ i ∈ s, f i x) t x

Tactic:
(h _ (Finset.mem_insert_self i s)).add
      (IH fun j hj => h _ (Finset.mem_insert_of_mem hj))

Premises used: ContDiffWithinAt.add, Finset.mem_insert_self, Finset.mem_insert_of_mem
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
t : Set E
x : E
i : ι
s : Finset ι
is : i ∉ s
IH :
  ∀ (h : ∀ i ∈ s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x),
    ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t x
h : ∀ i_1 ∈ insert i s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i_1 x) t x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x + ∑ i ∈ s, f i x) t x

Tactic:
exact (h _ (Finset.mem_insert_self i s)).add
      (IH fun j hj => h _ (Finset.mem_insert_of_mem hj))

Premises used: ContDiffWithinAt.add, Finset.mem_insert_self, Finset.mem_insert_of_mem
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
t : Set E
x : E
h : ∀ i ∈ s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x
empty :
  ∀
    (h :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i → ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x),
    ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ ∅, f i x) t x
insert :
  ∀ (i : ι) (s : Finset ι) (is : i ∉ s)
    (IH :
      ∀ (h : ∀ i ∈ s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x),
        ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t x)
    (h : ∀ i_1 ∈ Insert.insert i s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i_1 x) t x),
    ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ Insert.insert i s, f i x) t x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t x

Tactic:
induction s using Finset.induction_on with
  | empty => simp [contDiffWithinAt_const]
  | insert i s is IH =>
    simp only [is, Finset.sum_insert, not_false_iff]
    exact (h _ (Finset.mem_insert_self i s)).add
      (IH fun j hj => h _ (Finset.mem_insert_of_mem hj))

Premises used: contDiffWithinAt_const, Insert.insert, Finset.sum_insert, not_false_iff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
t : Set E
x : E
h : ∀ i ∈ s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x
empty :
  ∀
    (h :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i → ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x),
    ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ ∅, f i x) t x
insert :
  ∀ (i : ι) (s : Finset ι) (is : i ∉ s)
    (IH :
      ∀ (h : ∀ i ∈ s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t x),
        ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t x)
    (h : ∀ i_1 ∈ Insert.insert i s, ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i_1 x) t x),
    ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ Insert.insert i s, f i x) t x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t x

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp [contDiffWithinAt_const]
  | insert i s is IH =>
    simp only [is, Finset.sum_insert, not_false_iff]
    exact (h _ (Finset.mem_insert_self i s)).add
      (IH fun j hj => h _ (Finset.mem_insert_of_mem hj))

Premises used: contDiffWithinAt_const, Insert.insert, Finset.sum_insert, not_false_iff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
x : E
h : ∀ i ∈ s, ContDiffAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) univ x

Tactic:
ContDiffWithinAt.sum h

Premises used: ContDiffWithinAt.sum
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
x : E
h : ∀ i ∈ s, ContDiffAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) univ x

Tactic:
exact ContDiffWithinAt.sum h

Premises used: ContDiffWithinAt.sum
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
t : Set E
h : ∀ i ∈ s, ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) t
⊢ ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) t

Tactic:
fun x hx =>
  ContDiffWithinAt.sum fun i hi => h i hi x hx

Premises used: ContDiffOn, ContDiffWithinAt.sum
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
h : ∀ i ∈ s, ContDiff.{u_1, uE, uF} 𝕜 (F := F) n fun (x : E) ↦ f i x
simp :
  ∀ (h : ∀ i ∈ s, ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) univ),
    ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) univ
⊢ ContDiff.{u_1, uE, uF} 𝕜 (F := F) n fun (x : E) ↦ ∑ i ∈ s, f i x

Tactic:
simp only [← contDiffOn_univ] at *

Premises used: contDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
h : ∀ i ∈ s, ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) univ
⊢ ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) univ

Tactic:
ContDiffOn.sum h

Premises used: ContDiffOn.sum
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
ι : Type u_3
f : ι → E → F
s : Finset ι
h : ∀ i ∈ s, ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ f i x) univ
⊢ ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ ∑ i ∈ s, f i x) univ

Tactic:
exact ContDiffOn.sum h

Premises used: ContDiffOn.sum
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x
⊢ Eq (α := E → F) (∑ j ∈ u, f j) fun (x : E) ↦ ∑ j ∈ u, f j x

Tactic:
aesop
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x
rw :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (∑ j ∈ u, f j) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)

Tactic:
rw [(by aesop : (∑ j ∈ u, f j) = (fun x ↦ ∑ j ∈ u, f j x))]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ ∅, f j x) s x) (∑ j ∈ ∅, iteratedFDerivWithin 𝕜 i (f j) s x)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  ∀ (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
h : ∀ j ∈ Finset.cons a u ha, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x
⊢ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f a) s x ∧ ∀ a ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f a) s x

Tactic:
simp only [Finset.mem_cons, forall_eq_or_imp] at h

Premises used: forall_eq_or_imp, Finset.mem_cons