awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f t x)

Tactic:
exact fderivWithin_of_mem_nhdsWithin h (hs x hx) (hf.differentiableWithinAt two_ne_zero)

Premises used: fderivWithin_of_mem_nhdsWithin, two_ne_zero, ContDiffWithinAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)
⊢ Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x)

Tactic:
have : fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x := by
    apply Filter.EventuallyEq.fderivWithin_eq A
    exact fderivWithin_of_mem_nhdsWithin h (hs x hx) (hf.differentiableWithinAt two_ne_zero)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)
this : Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x)
rw : Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x)
⊢ Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)
this : Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x)
apply : DifferentiableWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f t) t x
⊢ Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x)

Tactic:
apply fderivWithin_of_mem_nhdsWithin h (hs x hx)

Premises used: fderivWithin_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)
this : Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x)
⊢ DifferentiableWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f t) t x

Tactic:
(hf.fderivWithin_right (m := 1) ht le_rfl
    (mem_of_mem_nhdsWithin hx h)).differentiableWithinAt one_ne_zero

Premises used: le_rfl, mem_of_mem_nhdsWithin, one_ne_zero, ContDiffWithinAt.differentiableWithinAt, ContDiffWithinAt.fderivWithin_right
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
A : ∀ᶠ (y : E) in 𝓝[s] x, Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)
this : Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x)
⊢ DifferentiableWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f t) t x

Tactic:
exact (hf.fderivWithin_right (m := 1) ht le_rfl
    (mem_of_mem_nhdsWithin hx h)).differentiableWithinAt one_ne_zero

Premises used: le_rfl, mem_of_mem_nhdsWithin, one_ne_zero, ContDiffWithinAt.differentiableWithinAt, ContDiffWithinAt.fderivWithin_right
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : s =ᶠ[𝓝 x] t
⊢ Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x)

Tactic:
calc
  fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x
    = fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x :=
      (fderivWithin_eventually_congr_set h).fderivWithin_eq_of_nhds
  _ = fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x := fderivWithin_congr_set h

Premises used: Trans.trans, Filter.EventuallyEq.fderivWithin_eq_of_nhds, fderivWithin_eventually_congr_set, fderivWithin_congr_set
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : s ∈ 𝓝 x
simp :
  Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f univ) univ x)
⊢ Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderiv 𝕜 (fderiv 𝕜 f) x)

Tactic:
simp only [← fderivWithin_univ]

Premises used: fderivWithin_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : s ∈ 𝓝 x
h₁ : s =ᶠ[𝓝 x] univ
⊢ Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f univ) univ x)

Tactic:
apply fderivWithin_fderivWithin_eq_of_eventuallyEq

Premises used: fderivWithin_fderivWithin_eq_of_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ s =ᶠ[𝓝 x] univ

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
⊢ IsSymmSndFDerivWithinAt 𝕜 f univ x ↔ IsSymmSndFDerivAt 𝕜 f x

Tactic:
simp [IsSymmSndFDerivWithinAt, IsSymmSndFDerivAt]

Premises used: IsSymmSndFDerivWithinAt, IsSymmSndFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f t x
hst : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
v w : E
rw :
  Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)
⊢ Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)

Tactic:
rw [fderivWithin_fderivWithin_eq_of_mem_nhdsWithin hst hf hs ht hx]

Premises used: fderivWithin_fderivWithin_eq_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f t x
hst : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
v w : E
⊢ Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)

Tactic:
h v w
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f t x
hst : t ∈ 𝓝[s] x
hf : ContDiffWithinAt 𝕜 2 f t x
hs : UniqueDiffOn 𝕜 s
ht : UniqueDiffOn 𝕜 t
hx : x ∈ s
v w : E
⊢ Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)

Tactic:
exact h v w
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
v w : E
rw :
  Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)
⊢ Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)

Tactic:
rw [fderivWithin_fderivWithin_eq_of_eventuallyEq hst.symm]

Premises used: fderivWithin_fderivWithin_eq_of_eventuallyEq, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
v w : E
⊢ Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)

Tactic:
h v w
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
v w : E
⊢ Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)

Tactic:
exact h v w
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
hst : s =ᶠ[𝓝 x] t
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x ↔ IsSymmSndFDerivWithinAt 𝕜 f t x

Tactic:
⟨fun h ↦ h.congr_set hst, fun h ↦ h.congr_set hst.symm⟩

Premises used: Iff.intro, IsSymmSndFDerivWithinAt.congr_set, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : IsSymmSndFDerivAt 𝕜 f x
hf : ContDiffAt 𝕜 2 f x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ IsSymmSndFDerivWithinAt 𝕜 f univ x

Tactic:
simp only [← isSymmSndFDerivWithinAt_univ, ← contDiffWithinAt_univ] at h hf

Premises used: isSymmSndFDerivWithinAt_univ, contDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : IsSymmSndFDerivAt 𝕜 f x
hf : ContDiffAt 𝕜 2 f x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h₁ : IsSymmSndFDerivWithinAt 𝕜 f univ x
⊢ ContDiffWithinAt 𝕜 2 f univ x

Tactic:
simp only [← isSymmSndFDerivWithinAt_univ, ← contDiffWithinAt_univ] at h hf

Premises used: isSymmSndFDerivWithinAt_univ, contDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : IsSymmSndFDerivWithinAt 𝕜 f univ x
hf : ContDiffWithinAt 𝕜 2 f univ x
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x

Tactic:
h.mono_of_mem_nhdsWithin univ_mem hf hs uniqueDiffOn_univ hx

Premises used: IsSymmSndFDerivWithinAt.mono_of_mem_nhdsWithin, uniqueDiffOn_univ, Filter.univ_mem
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : IsSymmSndFDerivWithinAt 𝕜 f univ x
hf : ContDiffWithinAt 𝕜 2 f univ x
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x

Tactic:
exact h.mono_of_mem_nhdsWithin univ_mem hf hs uniqueDiffOn_univ hx

Premises used: IsSymmSndFDerivWithinAt.mono_of_mem_nhdsWithin, uniqueDiffOn_univ, Filter.univ_mem
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
simp_rw :
  (∀ (v w : E),
      Eq.{u_3 + 1} (α := F)
        ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
        ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)) ↔
    ∀ (a a_1 : E),
      Eq.{u_3 + 1} (α := F)
        ((ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDerivWithin 𝕜 2 f s x) : (a : (i : Fin 2) → E) → F)
            (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ E) a
              (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) a_1
                (finZeroElim (α := fun (i : Fin 0) ↦ E)))) :
          F)
        ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F)
            (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ E) a
              (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) a_1
                (finZeroElim (α := fun (i : Fin 0) ↦ E)))) :
          F)
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x ↔
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin 2) ↦ E) F)
      (ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDerivWithin 𝕜 2 f s x))
      (iteratedFDerivWithin 𝕜 2 f s x)

Tactic:
simp_rw [IsSymmSndFDerivWithinAt, ContinuousMultilinearMap.ext_iff, Fin.forall_fin_succ_pi,
    Fin.forall_fin_zero_pi]

Premises used: IsSymmSndFDerivWithinAt, Fin.forall_fin_succ_pi, Fin.forall_fin_zero_pi, ContinuousMultilinearMap.ext_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ (∀ (v w : E),
      Eq.{u_3 + 1} (α := F)
        ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
        ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)) ↔
    ∀ (a a_1 : E),
      Eq.{u_3 + 1} (α := F)
        ((ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDerivWithin 𝕜 2 f s x) : (a : (i : Fin 2) → E) → F)
            (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ E) a
              (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) a_1
                (finZeroElim (α := fun (i : Fin 0) ↦ E)))) :
          F)
        ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F)
            (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ E) a
              (Fin.cons (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) a_1
                (finZeroElim (α := fun (i : Fin 0) ↦ E)))) :
          F)

Tactic:
simp [iteratedFDerivWithin_two_apply f hs hx, eq_comm]

Premises used: eq_comm, iteratedFDerivWithin_two_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
simp :
  IsSymmSndFDerivWithinAt 𝕜 f univ x ↔
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin 2) ↦ E) F)
      (ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDerivWithin 𝕜 2 f univ x))
      (iteratedFDerivWithin 𝕜 2 f univ x)
⊢ IsSymmSndFDerivAt 𝕜 f x ↔
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin 2) ↦ E) F)
      (ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDeriv 𝕜 2 f x)) (iteratedFDeriv 𝕜 2 f x)

Tactic:
simp only [← isSymmSndFDerivWithinAt_univ, ← iteratedFDerivWithin_univ]

Premises used: isSymmSndFDerivWithinAt_univ, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
⊢ IsSymmSndFDerivWithinAt 𝕜 f univ x ↔
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin 2) ↦ E) F)
      (ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDerivWithin 𝕜 2 f univ x))
      (iteratedFDerivWithin 𝕜 2 f univ x)

Tactic:
isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin uniqueDiffOn_univ (mem_univ _)

Premises used: uniqueDiffOn_univ, Set.mem_univ, isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
⊢ IsSymmSndFDerivWithinAt 𝕜 f univ x ↔
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin 2) ↦ E) F)
      (ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDerivWithin 𝕜 2 f univ x))
      (iteratedFDerivWithin 𝕜 2 f univ x)

Tactic:
exact isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin uniqueDiffOn_univ (mem_univ _)

Premises used: uniqueDiffOn_univ, Set.mem_univ, isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x v w : E
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ ∀ (x_1 : (i : Fin 2) → E),
    Eq.{u_3 + 1} (α := F)
      ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) fun (i : Fin 2) ↦
          x_1 ((Fin.revPerm : (a : Fin 2) → Fin 2) i) :
        F)
      ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) x_1 : F)

Tactic:
simp_rw [isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin hs hx, ContinuousMultilinearMap.ext_iff,
    ContinuousMultilinearMap.domDomCongr_apply] at hf

Premises used: ContinuousMultilinearMap.domDomCongr_apply, isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin, ContinuousMultilinearMap.ext_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x v w : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hf :
  ∀ (x_1 : (i : Fin 2) → E),
    Eq.{u_3 + 1} (α := F)
      ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) fun (i : Fin 2) ↦
          x_1 ((Fin.revPerm : (a : Fin 2) → Fin 2) i) :
        F)
      ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) x_1 : F)
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) fun (i : Fin 2) ↦
        ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) i) :
      F)
    ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) ![w, v] : F)

Tactic:
hf ![w, v]

Premises used: Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x v w : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hf :
  ∀ (x_1 : (i : Fin 2) → E),
    Eq.{u_3 + 1} (α := F)
      ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) fun (i : Fin 2) ↦
          x_1 ((Fin.revPerm : (a : Fin 2) → Fin 2) i) :
        F)
      ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) x_1 : F)
h : ![v, w] = fun (i : Fin 2) ↦ ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) i)
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) ![v, w] : F)
    ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) ![w, v] : F)

Tactic:
convert! hf ![w, v] using 2

Premises used: Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x v w : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hf :
  ∀ (x_1 : (i : Fin 2) → E),
    Eq.{u_3 + 1} (α := F)
      ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) fun (i : Fin 2) ↦
          x_1 ((Fin.revPerm : (a : Fin 2) → Fin 2) i) :
        F)
      ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) x_1 : F)
h : ∀ (i : Fin (Nat.succ 1)), ![v, w] i = ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) i)
⊢ ![v, w] = fun (i : Fin 2) ↦ ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) i)

Tactic:
ext i