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 g : E → F
hf : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x
hg : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h :
  t ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}
a : E
ha : a ∈ s ∩ t
⊢ a ∈ t ∩ insert x s

Tactic:
simp_all
-- 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
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h :
  t ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}
⊢ ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ t)

Tactic:
have hft : ContDiffOn 𝕜 i f (s ∩ t) := fun a ha ↦ (h (by simp_all)).1.mono inter_subset_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
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
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h :
  t ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}
hft : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ t)
a : E
ha : a ∈ s ∩ t
⊢ a ∈ t ∩ insert x s

Tactic:
simp_all
-- 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
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h :
  t ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}
hft : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ t)
⊢ ContDiffOn 𝕜 (↑i : ℕ∞ω) g (s ∩ t)

Tactic:
have hgt : ContDiffOn 𝕜 i g (s ∩ t) := fun a ha ↦ (h (by simp_all)).2.mono inter_subset_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
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
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h :
  t ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}
hft : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ t)
hgt : ContDiffOn 𝕜 (↑i : ℕ∞ω) g (s ∩ t)
⊢ UniqueDiffOn 𝕜 (s ∩ t)

Tactic:
have hut : UniqueDiffOn 𝕜 (s ∩ t) := hu.inter ht
-- 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
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h :
  t ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}
hft : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ t)
hgt : ContDiffOn 𝕜 (↑i : ℕ∞ω) g (s ∩ t)
hut : UniqueDiffOn 𝕜 (s ∩ t)
⊢ s ∩ t =ᶠ[𝓝 x] s

Tactic:
have H : ↑(s ∩ t) =ᶠ[𝓝 x] s :=
    inter_eventuallyEq_left.mpr (eventually_of_mem (ht.mem_nhds hxt) (fun _ h _ ↦ h))
-- 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
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h :
  t ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}
hft : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ t)
hgt : ContDiffOn 𝕜 (↑i : ℕ∞ω) g (s ∩ t)
hut : UniqueDiffOn 𝕜 (s ∩ t)
H : s ∩ t =ᶠ[𝓝 x] s
rw :
  iteratedFDerivWithin 𝕜 i (f + g) (s ∩ t) x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f (s ∩ t) x) (iteratedFDerivWithin 𝕜 i g (s ∩ t) x)
⊢ iteratedFDerivWithin 𝕜 i (f + g) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f s x) (iteratedFDerivWithin 𝕜 i g s x)

Tactic:
rw [← iteratedFDerivWithin_congr_set H, ← iteratedFDerivWithin_congr_set H,
    ← iteratedFDerivWithin_congr_set H]

Premises used: iteratedFDerivWithin_congr_set
-- 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
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h :
  t ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}
hft : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ t)
hgt : ContDiffOn 𝕜 (↑i : ℕ∞ω) g (s ∩ t)
hut : UniqueDiffOn 𝕜 (s ∩ t)
H : s ∩ t =ᶠ[𝓝 x] s
⊢ iteratedFDerivWithin 𝕜 i (f + g) (s ∩ t) x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f (s ∩ t) x) (iteratedFDerivWithin 𝕜 i g (s ∩ t) x)

Tactic:
.symm (((hft.ftaylorSeriesWithin hut).add
      (hgt.ftaylorSeriesWithin hut)).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl hut ⟨hx, hxt⟩)

Premises used: le_rfl, HasFTaylorSeriesUpToOn.add, And.intro, HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn, Eq.symm, ContDiffOn.ftaylorSeriesWithin
-- 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
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h :
  t ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x ∧ ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) g s x) x}
hft : ContDiffOn 𝕜 (↑i : ℕ∞ω) f (s ∩ t)
hgt : ContDiffOn 𝕜 (↑i : ℕ∞ω) g (s ∩ t)
hut : UniqueDiffOn 𝕜 (s ∩ t)
H : s ∩ t =ᶠ[𝓝 x] s
⊢ iteratedFDerivWithin 𝕜 i (f + g) (s ∩ t) x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f (s ∩ t) x) (iteratedFDerivWithin 𝕜 i g (s ∩ t) x)

Tactic:
exact .symm (((hft.ftaylorSeriesWithin hut).add
      (hgt.ftaylorSeriesWithin hut)).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl hut ⟨hx, hxt⟩)
-- 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 =
    HAdd.hAdd (α := 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 =
    HAdd.hAdd (α := 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 =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i f univ x) (iteratedFDerivWithin 𝕜 i g univ x)

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

Premises used: iteratedFDerivWithin_add_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 g : E → F
hf : ContDiffAt 𝕜 (↑i : ℕ∞ω) f x
hg : ContDiffAt 𝕜 (↑i : ℕ∞ω) g x
⊢ iteratedFDerivWithin 𝕜 i (f + g) univ x =
    HAdd.hAdd (α := 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_add_apply hf hg uniqueDiffOn_univ (Set.mem_univ _)

Premises used: iteratedFDerivWithin_add_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 g : E → F
hf : ContDiff 𝕜 (↑i : ℕ∞ω) f
hg : ContDiff 𝕜 (↑i : ℕ∞ω) g
⊢ iteratedFDeriv 𝕜 i (f + g) =
    HAdd.hAdd (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i f)
      (iteratedFDeriv 𝕜 i g)

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

Premises used: iteratedFDeriv_add_apply, funext, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
⊢ ContDiff 𝕜 (F := F) n fun (p : F) ↦ -p

Tactic:
IsBoundedLinearMap.id.neg.contDiff

Premises used: IsBoundedLinearMap.contDiff, IsBoundedLinearMap.id, IsBoundedLinearMap.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 : ℕ∞ω
s : Set E
f : E → F
hf : ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ -f x) s x

Tactic:
contDiff_neg.contDiffWithinAt.comp x hf subset_preimage_univ

Premises used: ContDiffWithinAt.comp, Set.subset_preimage_univ, contDiff_neg, ContDiff.contDiffWithinAt
-- 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 : E → F
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffWithinAt 𝕜 n f univ x

Tactic:
rw [← contDiffWithinAt_univ] at *

Premises used: contDiffWithinAt_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
n : ℕ∞ω
f : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ -f x) univ x

Tactic:
hf.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
n : ℕ∞ω
f : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ -f x) univ x

Tactic:
exact hf.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
n : ℕ∞ω
f : E → F
hf : ContDiff 𝕜 n f
⊢ ContDiff.{u_1, uE, uF} 𝕜 (F := F) n fun (x : E) ↦ -f x

Tactic:
contDiff_neg.comp hf

Premises used: contDiff_neg, ContDiff.comp
-- 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 : E → F
hf : ContDiffOn 𝕜 n f s
⊢ ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (x : E) ↦ -f x) s

Tactic:
fun x hx => (hf x hx).neg

Premises used: ContDiffOn, 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
f : E → F
hu : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
zero :
  ∀ (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)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDerivWithin 𝕜 0 (-f) s x)
    (-iteratedFDerivWithin 𝕜 0 f s x)

Tactic:
ext h
-- 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
f : E → F
hu : UniqueDiffOn 𝕜 s
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)

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
f : E → F
hu : UniqueDiffOn 𝕜 s
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
succ :
  ∀ (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 + 1)) ↦ E) F)
    (iteratedFDerivWithin 𝕜 (i + 1) (-f) s x) (-iteratedFDerivWithin 𝕜 (i + 1) f s x)

Tactic:
ext h
-- 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
f : E → F
hu : UniqueDiffOn 𝕜 s
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)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)

Tactic:
iteratedFDerivWithin_succ_apply_left _

Premises used: 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
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
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
rw :
  Eq.{uF + 1} (α := F)
    ((((fderivWithin 𝕜 (fun (x : E) ↦ -iteratedFDerivWithin 𝕜 i f s x) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    ((((fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
rw₁ rw₂ :
  Eq.{uF + 1} (α := F)
    ((((fderivWithin 𝕜 (fun (x : E) ↦ -iteratedFDerivWithin 𝕜 i f s x) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    ((((fderivWithin 𝕜 (fun (i_1 : E) ↦ -iteratedFDerivWithin 𝕜 i f s i_1) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
⊢ Eq.{uF + 1} (α := F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (-f) s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    ((((fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              (h 0) :
            ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)

Tactic:
rw [fderivWithin_congr' (@hi) hx, Pi.neg_def]

Premises used: fderivWithin_congr', Pi.neg_def
-- 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
f : E → F
hu : UniqueDiffOn 𝕜 s
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
rw rw₁ :
  Eq.{uF + 1} (α := F)
    (-(((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
                (h 0) :
              ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
            (a : (i : Fin i) → E) → F)
          (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    (-(((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
                (h 0) :
              ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
            (a : (i : Fin i) → E) → F)
          (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
⊢ Eq.{uF + 1} (α := F)
    (-(((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x :
                  (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
                (h 0) :
              ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) :
            (a : (i : Fin i) → E) → F)
          (tail (α := fun (i : Fin (i + 1)) ↦ E) h) :
      F)
    (-(iteratedFDerivWithin 𝕜 (i + 1) f s x : (a : (i : Fin (i + 1)) → E) → F) h : F)

Tactic:
rw [iteratedFDerivWithin_succ_apply_left]

Premises used: iteratedFDerivWithin_succ_apply_left