awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.RestrictScalars (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜' f x ↔ ∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderiv 𝕜 f x)
have rw : DifferentiableWithinAt 𝕜' f univ x ↔
  ∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderivWithin 𝕜 f univ x)
Tactic: rw [← differentiableWithinAt_univ, ← fderivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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
⊢ ∀ᶠ (y : E) in 𝓝[s] x, Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)
have this : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y
Tactic: have : ∀ᶠ y in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y :=
      nhdsWithin_le_iff.2 h (nhdsWithin_mono _ (subset_insert x t) (hf.eventually (by simp)))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
this : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y
⊢ ∀ᶠ (y : E) in 𝓝[s] x, Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)
have h₁ : ∀ (y : E) (hy : y ∈ s) (h'y : ContDiffWithinAt 𝕜 2 f t y) (h''y : ∀ᶠ (x : E) in 𝓝[s] y, t x),
  Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)
Tactic: filter_upwards [self_mem_nhdsWithin, this, eventually_eventually_nhdsWithin.2 h]
      with y hy h'y h''y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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
⊢ Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x)
have A : ∀ᶠ (y : E) in 𝓝[s] x, Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s y) (fderivWithin 𝕜 f t y)
Tactic: have A : ∀ᶠ y in 𝓝[s] x, fderivWithin 𝕜 f s y = fderivWithin 𝕜 f t y := by
    have : ∀ᶠ y in 𝓝[s] x, ContDiffWithinAt 𝕜 2 f t y :=
      nhdsWithin_le_iff.2 h (nhdsWithin_mono _ (subset_insert x t) (hf.eventually (by simp)))
    filter_upwards [self_mem_nhdsWithin, this, eventually_eventually_nhdsWithin.2 h]
      with y hy h'y h''y
    exact fderivWithin_of_mem_nhdsWithin h''y (hs y hy) (h'y.differentiableWithinAt two_ne_zero)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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)
have apply : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f t x)
Tactic: apply Filter.EventuallyEq.fderivWithin_eq A
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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) t x)
have this : 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)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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)
⊢ Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x)
have rw : Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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)
⊢ Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x)
have apply : DifferentiableWithinAt 𝕜 (F := E →L[𝕜] F) (fderivWithin 𝕜 f t) t x
Tactic: apply fderivWithin_of_mem_nhdsWithin h (hs x hx)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
⊢ Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderiv 𝕜 (fderiv 𝕜 f) x)
have simp : Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f univ) univ x)
Tactic: simp only [← fderivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
⊢ Eq (α := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) (fderivWithin 𝕜 (fderivWithin 𝕜 f univ) univ x)
have h₁ : s =ᶠ[𝓝 x] univ
Tactic: apply fderivWithin_fderivWithin_eq_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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 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)
have 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)
Tactic: rw [fderivWithin_fderivWithin_eq_of_mem_nhdsWithin hst hf hs ht hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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 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)
have 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)
Tactic: rw [fderivWithin_fderivWithin_eq_of_eventuallyEq hst.symm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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 s x
have h₁ : IsSymmSndFDerivWithinAt 𝕜 f univ x
Tactic: simp only [← isSymmSndFDerivWithinAt_univ, ← contDiffWithinAt_univ] at h hf
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x
have hf₁ : ContDiffWithinAt 𝕜 2 f univ x
Tactic: simp only [← isSymmSndFDerivWithinAt_univ, ← contDiffWithinAt_univ] at h hf
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
⊢ 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)
have 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)
Tactic: simp_rw [IsSymmSndFDerivWithinAt, ContinuousMultilinearMap.ext_iff, Fin.forall_fin_succ_pi,
    Fin.forall_fin_zero_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
⊢ 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)
have 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)
Tactic: simp only [← isSymmSndFDerivWithinAt_univ, ← iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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
⊢ 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)
have 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)
Tactic: simp_rw [isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin hs hx, ContinuousMultilinearMap.ext_iff,
    ContinuousMultilinearMap.domDomCongr_apply] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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) ![v, w] : F)
    ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) ![w, v] : F)
have h : ![v, w] = fun (i : Fin 2) ↦ ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) i)
Tactic: convert! hf ![w, v] using 2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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)
⊢ ![v, w] = fun (i : Fin 2) ↦ ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) i)
have h : ∀ (i : Fin (Nat.succ 1)), ![v, w] i = ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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)
i : Fin (Nat.succ 1)
⊢ ![v, w] i = ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) i)
have h : ![v, w] ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 1))) =
  ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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)
i : Fin (Nat.succ 1)
h :
  ![v, w] ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 1))) =
    ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨0, ⋯⟩))
⊢ ![v, w] i = ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) i)
have h₁ : ![v, w] ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 1))) =
  ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨1, sorry⟩))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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 v w : E
hf : IsSymmSndFDerivAt 𝕜 f x
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDeriv 𝕜 2 f x : (a : (i : Fin 2) → E) → F) ![v, w] : F)
    ((iteratedFDeriv 𝕜 2 f x : (a : (i : Fin 2) → E) → F) ![w, v] : F)
have simp : ∀ (hf : IsSymmSndFDerivWithinAt 𝕜 f univ x),
  Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 2 f univ x : (a : (i : Fin 2) → E) → F) ![v, w] : F)
    ((iteratedFDerivWithin 𝕜 2 f univ x : (a : (i : Fin 2) → E) → F) ![w, v] : F)
Tactic: simp only [← isSymmSndFDerivWithinAt_univ, ← iteratedFDerivWithin_univ] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
hf : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x
have rw : 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: rw [isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin hs hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
hf : ContDiffAt 𝕜 ω f x
⊢ IsSymmSndFDerivAt 𝕜 f x
have simp : ∀ (hf : ContDiffWithinAt 𝕜 ω f univ x), IsSymmSndFDerivWithinAt 𝕜 f univ x
Tactic: simp only [← isSymmSndFDerivWithinAt_univ, ← contDiffWithinAt_univ] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • v + h • w) - f (x + h • v) - HSMul.hSMul (β := F) h ((f' x : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2 / 2)
          ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
have refine : ∀ (ε : ℝ) (εpos : 0 < ε),
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    ‖f (x + x_1 • v + x_1 • w) - f (x + x_1 • v) - HSMul.hSMul (β := F) x_1 ((f' x : (a : E) → F) w : F) -
            HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
              ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2 / 2)
            ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)‖ ≤
      ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * HPow.hPow (β := ℕ) x_1 2‖
Tactic: refine IsLittleO.trans_isBigO
    (isLittleO_iff.2 fun ε εpos => ?_) (isBigO_const_mul_self ((‖v‖ + ‖w‖) * ‖w‖) _ _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    ‖f (x + x_1 • v + x_1 • w) - f (x + x_1 • v) - HSMul.hSMul (β := F) x_1 ((f' x : (a : E) → F) w : F) -
            HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
              ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2 / 2)
            ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)‖ ≤
      ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * HPow.hPow (β := ℕ) x_1 2‖
have rw : ∀
  (hx :
    ∀ ⦃c : ℝ⦄,
      0 < c →
        ∀ᶠ (x_1 : E) in 𝓝[interior s] x,
          ‖HSub.hSub (β := E →L[ℝ] F) (f' x_1 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_1 - x) : E →L[ℝ] F)‖ ≤
            c * ‖x_1 - x‖)
  {v w : E} (hv : x + v ∈ interior s) (hw : x + v + w ∈ interior s) (ε : ℝ) (εpos : 0 < ε),
  ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    ‖f (x + x_1 • v + x_1 • w) - f (x + x_1 • v) - HSMul.hSMul (β := F) x_1 ((f' x : (a : E) → F) w : F) -
            HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
              ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2 / 2)
            ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)‖ ≤
      ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * HPow.hPow (β := ℕ) x_1 2‖
Tactic: rw [hasFDerivWithinAt_iff_isLittleO, isLittleO_iff] at hx
Cleared hypotheses: hx, v, w, hv, hw, ε, εpos