awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
G : Type x
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
v : (i : Fin 0) → E
h :
  Eq.{x + 1} (α := G) ((p 0 : (a : (i : Fin 0) → F) → G) ((⇑0 : (a : E) → F) ∘ v) : G)
    ((p 0 : (a : (i : Fin 0) → F) → G) ![] : G)
⊢ Eq.{x + 1} (α := G) ((p.compContinuousLinearMap 0 0 : (a : (i : Fin 0) → E) → G) v : G)
    (((constFormalMultilinearSeries 𝕜 E ((p 0 : (a : (i : Fin 0) → F) → G) 0) 0 :
            ContinuousMultilinearMap.{u, 0, v, x} 𝕜 (fun (i : Fin 0) ↦ E) G) :
          (a : (i : Fin 0) → E) → G)
        v :
      G)

Tactic:
simp only [FormalMultilinearSeries.compContinuousLinearMap_apply, Matrix.zero_empty,
      constFormalMultilinearSeries_apply_zero, ContinuousMultilinearMap.uncurry0_apply]

Premises used: constFormalMultilinearSeries_apply_zero, ContinuousMultilinearMap.uncurry0_apply, FormalMultilinearSeries.compContinuousLinearMap_apply, Matrix.zero_empty
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
G : Type x
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
v : (i : Fin 0) → E
h : Eq.{w + 1} (α := (i : Fin 0) → F) ((⇑0 : (a : E) → F) ∘ v) ![]
⊢ Eq.{x + 1} (α := G) ((p 0 : (a : (i : Fin 0) → F) → G) ((⇑0 : (a : E) → F) ∘ v) : G)
    ((p 0 : (a : (i : Fin 0) → F) → G) ![] : G)

Tactic:
congr
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
G : Type x
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
v : (i : Fin 0) → E
⊢ Eq.{w + 1} (α := (i : Fin 0) → F) ((⇑0 : (a : E) → F) ∘ v) ![]

Tactic:
apply Subsingleton.allEq

Premises used: Subsingleton.allEq
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
G : Type x
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
n : ℕ
v : (i : Fin (n + 1)) → E
⊢ Eq.{x + 1} (α := G) ((p.compContinuousLinearMap 0 (n + 1) : (a : (i : Fin (n + 1)) → E) → G) v : G)
    (((constFormalMultilinearSeries 𝕜 E ((p 0 : (a : (i : Fin 0) → F) → G) 0) (n + 1) :
            ContinuousMultilinearMap.{u, 0, v, x} 𝕜 (fun (i : Fin (n + 1)) ↦ E) G) :
          (a : (i : Fin (n + 1)) → E) → G)
        v :
      G)

Tactic:
simp [ContinuousLinearMap.coe_zero']

Premises used: ContinuousLinearMap.coe_zero'
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
G : Type x
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
n : ℕ
v : (i : Fin n) → E
h :
  ∀ (v : (i : Fin 0) → E),
    Eq.{x + 1} (α := G) ((p.compContinuousLinearMap 0 0 : (a : (i : Fin 0) → E) → G) v : G)
      (((constFormalMultilinearSeries 𝕜 E ((p 0 : (a : (i : Fin 0) → F) → G) 0) 0 :
              ContinuousMultilinearMap.{u, 0, v, x} 𝕜 (fun (i : Fin 0) ↦ E) G) :
            (a : (i : Fin 0) → E) → G)
          v :
        G)
h₁ :
  ∀ (n : ℕ) (v : (i : Fin (n + 1)) → E),
    Eq.{x + 1} (α := G) ((p.compContinuousLinearMap 0 (n + 1) : (a : (i : Fin (n + 1)) → E) → G) v : G)
      (((constFormalMultilinearSeries 𝕜 E ((p 0 : (a : (i : Fin 0) → F) → G) 0) (n + 1) :
              ContinuousMultilinearMap.{u, 0, v, x} 𝕜 (fun (i : Fin (n + 1)) ↦ E) G) :
            (a : (i : Fin (n + 1)) → E) → G)
          v :
        G)
⊢ Eq.{x + 1} (α := G) ((p.compContinuousLinearMap 0 n : (a : (i : Fin n) → E) → G) v : G)
    (((constFormalMultilinearSeries 𝕜 E ((p 0 : (a : (i : Fin 0) → F) → G) 0) n :
            ContinuousMultilinearMap.{u, 0, v, x} 𝕜 (fun (i : Fin n) ↦ E) G) :
          (a : (i : Fin n) → E) → G)
        v :
      G)

Tactic:
cases n with
  | zero =>
    simp only [FormalMultilinearSeries.compContinuousLinearMap_apply, Matrix.zero_empty,
      constFormalMultilinearSeries_apply_zero, ContinuousMultilinearMap.uncurry0_apply]
    congr
    apply Subsingleton.allEq
  | succ =>
    simp [ContinuousLinearMap.coe_zero']

Premises used: ContinuousLinearMap.coe_zero', Fin.succ, constFormalMultilinearSeries_apply_zero, Subsingleton.allEq, ContinuousMultilinearMap.uncurry0_apply, FormalMultilinearSeries.compContinuousLinearMap_apply, Matrix.zero_empty
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin 0) ↦ E) F) (f.fpowerSeries x 0)
    (ContinuousMultilinearMap.uncurry0 𝕜 E ((f : (a : E) → F) x))

Tactic:
rfl

Premises used: ContinuousLinearMap.fpowerSeries, rfl
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin 1) ↦ E) F) (f.fpowerSeries x 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      f)

Tactic:
rfl

Premises used: ContinuousLinearMap.fpowerSeries, rfl
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin (n + 2)) ↦ E) F) (f.fpowerSeries x (n + 2)) 0

Tactic:
rfl

Premises used: ContinuousLinearMap.fpowerSeries, rfl
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
f' x : F
s : Set F
⊢ HasGradientWithinAt f f' s x ↔ HasFDerivWithinAt (𝕜 := 𝕜) f ((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F) f') s x

Tactic:
Iff.rfl

Premises used: HasGradientAtFilter, HasGradientWithinAt, Iff.rfl, HasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
x : F
frechet : StrongDual 𝕜 F
s : Set F
rw :
  HasFDerivWithinAt (𝕜 := 𝕜) f frechet s x ↔
    HasFDerivWithinAt (𝕜 := 𝕜) f
      ((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F)
        ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) frechet))
      s x
rw₁ rw₂ : HasFDerivWithinAt (𝕜 := 𝕜) f frechet s x ↔ HasFDerivWithinAt (𝕜 := 𝕜) f frechet s x
⊢ HasFDerivWithinAt (𝕜 := 𝕜) f frechet s x ↔
    HasGradientWithinAt f ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) frechet) s x

Tactic:
rw [hasGradientWithinAt_iff_hasFDerivWithinAt, (toDual 𝕜 F).apply_symm_apply frechet]

Premises used: InnerProductSpace.toDual, LinearIsometryEquiv.apply_symm_apply, hasGradientWithinAt_iff_hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
f' x : F
⊢ HasGradientAt f f' x ↔ HasFDerivAt (𝕜 := 𝕜) f ((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F) f') x

Tactic:
Iff.rfl

Premises used: HasFDerivAt, HasGradientAtFilter, Iff.rfl, HasGradientAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
x : F
frechet : StrongDual 𝕜 F
rw :
  HasFDerivAt (𝕜 := 𝕜) f frechet x ↔
    HasFDerivAt (𝕜 := 𝕜) f
      ((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F)
        ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) frechet))
      x
rw₁ rw₂ : HasFDerivAt (𝕜 := 𝕜) f frechet x ↔ HasFDerivAt (𝕜 := 𝕜) f frechet x
⊢ HasFDerivAt (𝕜 := 𝕜) f frechet x ↔
    HasGradientAt f ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) frechet) x

Tactic:
rw [hasGradientAt_iff_hasFDerivAt, (toDual 𝕜 F).apply_symm_apply frechet]

Premises used: InnerProductSpace.toDual, LinearIsometryEquiv.apply_symm_apply, hasGradientAt_iff_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
x : F
h : ¬DifferentiableAt 𝕜 f x
rw :
  Eq.{u_2 + 1} (α := F)
    ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) (fderiv 𝕜 f x : F →L[𝕜] 𝕜) : F) (0 : F)
rw₁ : Eq.{u_2 + 1} (α := F) ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) 0 : F) (0 : F)
rw₂ rw₃ : Eq.{u_2 + 1} (α := F) 0 0
⊢ ∇ f x = 0

Tactic:
rw [gradient, fderiv_zero_of_not_differentiableAt h, map_zero]

Premises used: gradient, map_zero, fderiv_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
x gradf gradg : F
hf : HasGradientAt f gradf x
hg : HasGradientAt f gradg x
⊢ gradf = gradg

Tactic:
(toDual 𝕜 F).injective (hf.hasFDerivAt.unique hg.hasFDerivAt)

Premises used: InnerProductSpace.toDual, HasGradientAt.hasFDerivAt, LinearIsometryEquiv.injective, HasFDerivAt.unique
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
x : F
h : DifferentiableAt 𝕜 f x
rw : HasFDerivAt f (fderiv 𝕜 f x) x
⊢ HasGradientAt f (∇ f x) x

Tactic:
rw [hasGradientAt_iff_hasFDerivAt, gradient, (toDual 𝕜 F).apply_symm_apply (fderiv 𝕜 f x)]

Premises used: InnerProductSpace.toDual, LinearIsometryEquiv.apply_symm_apply, gradient, fderiv, hasGradientAt_iff_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
x : F
h : DifferentiableAt 𝕜 f x
⊢ HasFDerivAt f (fderiv 𝕜 f x) x

Tactic:
h.hasFDerivAt

Premises used: DifferentiableAt.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
x : F
h : DifferentiableAt 𝕜 f x
⊢ HasFDerivAt f (fderiv 𝕜 f x) x

Tactic:
exact h.hasFDerivAt

Premises used: DifferentiableAt.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
f' x : F
h : HasGradientAt f f' x
⊢ DifferentiableAt 𝕜 f x

Tactic:
h.hasFDerivAt.differentiableAt

Premises used: HasGradientAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
x : F
s : Set F
h : DifferentiableWithinAt 𝕜 f s x
rw : HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x
⊢ HasGradientWithinAt f (gradientWithin f s x) s x

Tactic:
rw [hasGradientWithinAt_iff_hasFDerivWithinAt, gradientWithin,
    (toDual 𝕜 F).apply_symm_apply (fderivWithin 𝕜 f s x)]

Premises used: InnerProductSpace.toDual, LinearIsometryEquiv.apply_symm_apply, hasGradientWithinAt_iff_hasFDerivWithinAt, gradientWithin, fderivWithin
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
x : F
s : Set F
h : DifferentiableWithinAt 𝕜 f s x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x

Tactic:
h.hasFDerivWithinAt

Premises used: DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
x : F
s : Set F
h : DifferentiableWithinAt 𝕜 f s x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x

Tactic:
exact h.hasFDerivWithinAt

Premises used: DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
f' x : F
s : Set F
h : HasGradientWithinAt f f' s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
h.hasFDerivWithinAt.differentiableWithinAt

Premises used: HasFDerivWithinAt.differentiableWithinAt, HasGradientWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
f' x : F
⊢ HasFDerivWithinAt (𝕜 := 𝕜) f ((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F) f') univ x ↔
    HasFDerivAt (𝕜 := 𝕜) f ((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F) f') x

Tactic:
hasFDerivWithinAt_univ

Premises used: hasFDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
f' x : F
⊢ HasFDerivWithinAt (𝕜 := 𝕜) f ((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F) f') univ x ↔
    HasFDerivAt (𝕜 := 𝕜) f ((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F) f') x

Tactic:
exact hasFDerivWithinAt_univ

Premises used: hasFDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
x : F
s : Set F
h : DifferentiableOn 𝕜 f s
hs : s ∈ 𝓝 x
⊢ HasGradientAt f (∇ f x) x

Tactic:
(h.hasFDerivAt hs).hasGradientAt

Premises used: DifferentiableOn.hasFDerivAt, gradient, HasFDerivAt.hasGradientAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
f' x : F
h : HasGradientAt f f' x
⊢ ∇ f x = f'

Tactic:
h.differentiableAt.hasGradientAt.unique h

Premises used: HasGradientAt.unique, DifferentiableAt.hasGradientAt, HasGradientAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
f' : F → F
h : ∀ (x : F), HasGradientAt f (f' x) x
⊢ ∇ f = f'

Tactic:
funext fun x => (h x).gradient

Premises used: funext, HasGradientAt.gradient
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasGradientAtFilter g g' u L'
⊢ HasDerivAtFilter g ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') (SProd.sprod (β := Filter 𝕜) L' (pure u))

Tactic:
h

Premises used: HasGradientAtFilter, LinearMap.mkContinuousOfExistsBound, HasDerivAtFilter, ContinuousLinearMap.toSpanSingleton, LinearMap.smulRight, LinearMap.toSpanSingleton
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasDerivAtFilter g g' (SProd.sprod (β := Filter 𝕜) L' (pure u))
h₁ :
  Eq (α := 𝕜) ((ContinuousLinearMap.smulRight (S := 𝕜) 1 g' : (a : 𝕜) → 𝕜) 1 : 𝕜)
    ((((toDual 𝕜 𝕜 : (a : 𝕜) → StrongDual 𝕜 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') : StrongDual 𝕜 𝕜) : (a : 𝕜) → 𝕜) 1 :
      𝕜)
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜) (ContinuousLinearMap.smulRight (S := 𝕜) 1 g')
    ((toDual 𝕜 𝕜 : (a : 𝕜) → StrongDual 𝕜 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g'))

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasDerivAtFilter g g' (SProd.sprod (β := Filter 𝕜) L' (pure u))
⊢ Eq (α := 𝕜) ((ContinuousLinearMap.smulRight (S := 𝕜) 1 g' : (a : 𝕜) → 𝕜) 1 : 𝕜)
    ((((toDual 𝕜 𝕜 : (a : 𝕜) → StrongDual 𝕜 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') : StrongDual 𝕜 𝕜) : (a : 𝕜) → 𝕜) 1 :
      𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasDerivAtFilter g g' (SProd.sprod (β := Filter 𝕜) L' (pure u))
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜) (ContinuousLinearMap.smulRight (S := 𝕜) 1 g')
    ((toDual 𝕜 𝕜 : (a : 𝕜) → StrongDual 𝕜 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g'))

Tactic:
have : ContinuousLinearMap.smulRight (1 : 𝕜 →L[𝕜] 𝕜) g' = (toDual 𝕜 𝕜) (conj g') := by
    ext; simp
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasDerivAtFilter g g' (SProd.sprod (β := Filter 𝕜) L' (pure u))
this :
  Eq (α := 𝕜 →L[𝕜] 𝕜) (ContinuousLinearMap.smulRight (S := 𝕜) 1 g')
    ((toDual 𝕜 𝕜 : (a : 𝕜) → StrongDual 𝕜 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g'))
rwa :
  HasFDerivAtFilter (𝕜 := 𝕜) g ((toDual 𝕜 𝕜 : (a : 𝕜) → StrongDual 𝕜 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g'))
    (SProd.sprod (β := Filter 𝕜) L' (pure u))
rwa₁ rwa₂ rwa₃ rwa₄ :
  HasFDerivAtFilter (𝕜 := 𝕜) g (ContinuousLinearMap.smulRight (S := 𝕜) 1 g') (SProd.sprod (β := Filter 𝕜) L' (pure u))
⊢ HasGradientAtFilter g ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') u L'

Tactic:
rwa [HasGradientAtFilter, ← this]

Premises used: HasGradientAtFilter
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasGradientAt g g' u
⊢ HasDerivAt g ((((toDual 𝕜 𝕜 : (a : 𝕜) → StrongDual 𝕜 𝕜) g' : StrongDual 𝕜 𝕜) : (a : 𝕜) → 𝕜) 1) u

Tactic:
rw [hasGradientAt_iff_hasFDerivAt, hasFDerivAt_iff_hasDerivAt] at h

Premises used: hasFDerivAt_iff_hasDerivAt, hasGradientAt_iff_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasDerivAt g ((((toDual 𝕜 𝕜 : (a : 𝕜) → StrongDual 𝕜 𝕜) g' : StrongDual 𝕜 𝕜) : (a : 𝕜) → 𝕜) 1) u
⊢ HasDerivAt g ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') u

Tactic:
simpa using h
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasDerivAt g g' u
rw :
  HasDerivAt g
    ((((toDual 𝕜 𝕜 : (a : 𝕜) → StrongDual 𝕜 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') : StrongDual 𝕜 𝕜) : (a : 𝕜) → 𝕜) 1) u
⊢ HasGradientAt g ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') u

Tactic:
rw [hasGradientAt_iff_hasFDerivAt, hasFDerivAt_iff_hasDerivAt]

Premises used: hasFDerivAt_iff_hasDerivAt, hasGradientAt_iff_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasDerivAt g g' u
⊢ HasDerivAt g
    ((((toDual 𝕜 𝕜 : (a : 𝕜) → StrongDual 𝕜 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') : StrongDual 𝕜 𝕜) : (a : 𝕜) → 𝕜) 1) u

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
pos : ∀ (h : DifferentiableAt 𝕜 g u), ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)
neg : ∀ (h : ¬DifferentiableAt 𝕜 g u), ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)
⊢ ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)

Tactic:
by_cases h : DifferentiableAt 𝕜 g u

Premises used: DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : DifferentiableAt 𝕜 g u
pos : ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∇ g u) : 𝕜)
pos₁ pos₂ : ∇ g u = ∇ g u
⊢ ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)

Tactic:
rw [h.hasGradientAt.hasDerivAt.deriv, RCLike.conj_conj]

Premises used: HasDerivAt.deriv, RCLike.conj_conj, DifferentiableAt.hasGradientAt, HasGradientAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : ¬DifferentiableAt 𝕜 g u
neg : Eq (α := 𝕜) (0 : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u) : 𝕜)
neg₁ : Eq (α := 𝕜) (0 : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜)
neg₂ neg₃ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)

Tactic:
rw [gradient_eq_zero_of_not_differentiableAt h, deriv_zero_of_not_differentiableAt h, map_zero]

Premises used: deriv_zero_of_not_differentiableAt, map_zero, gradient_eq_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
g : ℝ → ℝ
g' u : ℝ
L' : Filter ℝ
h : HasGradientAtFilter g g' u L'
⊢ HasDerivAtFilter g g' (SProd.sprod (β := Filter ℝ) L' (pure u))

Tactic:
h.hasDerivAtFilter

Premises used: HasGradientAtFilter.hasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
g : ℝ → ℝ
g' u : ℝ
L' : Filter ℝ
h : HasDerivAtFilter g g' (SProd.sprod (β := Filter ℝ) L' (pure u))
⊢ HasGradientAtFilter g g' u L'

Tactic:
h.hasGradientAtFilter

Premises used: HasDerivAtFilter.hasGradientAtFilter
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
g : ℝ → ℝ
g' u : ℝ
h : HasGradientAt g g' u
⊢ HasDerivAt g g' u

Tactic:
h.hasDerivAt

Premises used: HasGradientAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
g : ℝ → ℝ
g' u : ℝ
h : HasDerivAt g g' u
⊢ HasGradientAt g g' u

Tactic:
h.hasGradientAt

Premises used: HasDerivAt.hasGradientAt
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
g : ℝ → ℝ
u : ℝ
⊢ ∇ g u = deriv g u

Tactic:
gradient_eq_deriv

Premises used: deriv, gradient_eq_deriv
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
f' x : F
L : Filter F
⊢ (Asymptotics.IsLittleO.{u_2, u_1, u_2} (E := 𝕜) (F := F) (SProd.sprod (β := Filter F) L (pure x))
      (fun (p : F × F) ↦
        HSub.hSub (β := 𝕜) (f p.1 - f p.2)
          ((((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F) f' : StrongDual 𝕜 F) : (a : F) → 𝕜) (p.1 - p.2) : 𝕜))
      fun (p : F × F) ↦ p.1 - p.2) ↔
    Asymptotics.IsLittleO.{u_2, u_1, u_2} (E := 𝕜) (F := F) L (fun (x' : F) ↦ f x' - f x - ⟪f', x' - x⟫) fun (x' : F) ↦
      x' - x

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
f' x : F
s : Set F
⊢ HasGradientWithinAt f f' s x ↔
    Asymptotics.IsLittleO.{u_2, u_1, u_2} (E := 𝕜) (F := F) (𝓝[s] x) (fun (x' : F) ↦ f x' - f x - ⟪f', x' - x⟫)
      fun (x' : F) ↦ x' - x

Tactic:
hasGradientAtFilter_iff_isLittleO

Premises used: HasGradientWithinAt, hasGradientAtFilter_iff_isLittleO
-- Module: Mathlib.Analysis.Calculus.Gradient.Basic
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : CompleteSpace F
f : F → 𝕜
f' x : F
s : Set F
⊢ HasGradientWithinAt f f' s x ↔
    Tendsto (β := ℝ) (fun (x' : F) ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - ⟪f', x' - x⟫‖) (𝓝[s] x) (𝓝 0)

Tactic:
hasFDerivWithinAt_iff_tendsto

Premises used: HasGradientAtFilter, HasGradientWithinAt, HasFDerivWithinAt, hasFDerivWithinAt_iff_tendsto