awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ↔
    Asymptotics.IsLittleO.{u_2, u_1, u_2} (E := 𝕜) (F := F) (𝓝 x) (fun (x' : F) ↦ f x' - f x - ⟪f', x' - x⟫)
      fun (x' : F) ↦ x' - x

Tactic:
hasGradientAtFilter_iff_isLittleO

Premises used: hasGradientAtFilter_iff_isLittleO, 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
⊢ HasGradientAt f f' x ↔ Tendsto (β := ℝ) (fun (x' : F) ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - ⟪f', x' - x⟫‖) (𝓝 x) (𝓝 0)

Tactic:
hasFDerivAt_iff_tendsto

Premises used: HasFDerivAt, HasGradientAtFilter, hasFDerivAt_iff_tendsto, 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
L : Filter F
h : HasGradientAtFilter f f' x L
⊢ Asymptotics.IsBigO.{u_2, u_1, u_2} (E := 𝕜) (F := F) L (fun (x' : F) ↦ f x' - f x) fun (x' : F) ↦ x' - x

Tactic:
HasFDerivAtFilter.isBigO_sub h |>.comp_tendsto prod_pure.ge

Premises used: Eq.ge, Filter.prod_pure, Asymptotics.IsBigO.comp_tendsto, HasFDerivAtFilter.isBigO_sub
-- 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 t : Set F
y : F
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ HasGradientWithinAt f f' s x ↔ HasGradientWithinAt f f' t x

Tactic:
hasFDerivWithinAt_congr_set' y h

Premises used: HasGradientAtFilter, HasGradientWithinAt, HasFDerivWithinAt, hasFDerivWithinAt_congr_set'
-- 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 t : Set F
h : s =ᶠ[𝓝 x] t
⊢ HasGradientWithinAt f f' s x ↔ HasGradientWithinAt f f' t x

Tactic:
hasFDerivWithinAt_congr_set h

Premises used: HasGradientAtFilter, HasGradientWithinAt, HasFDerivWithinAt, hasFDerivWithinAt_congr_set
-- 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 ↔
    Asymptotics.IsLittleO.{u_2, u_1, u_2} (E := 𝕜) (F := F) (𝓝 0) (fun (h : F) ↦ f (x + h) - f x - ⟪f', h⟫)
      fun (h : F) ↦ h

Tactic:
hasFDerivAt_iff_isLittleO_nhds_zero

Premises used: HasFDerivAt, HasGradientAtFilter, HasGradientAt, hasFDerivAt_iff_isLittleO_nhds_zero
-- 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 y : F
s : Set F
h : HasGradientWithinAt f f' s x
hs : UniqueDiffWithinAt 𝕜 s x
rw : (((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F) f' : StrongDual 𝕜 F) : (a : F) → 𝕜) y = ⟪f', y⟫
rw₁ rw₂ : ⟪f', y⟫ = ⟪f', y⟫
⊢ ((fderivWithin 𝕜 f s x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) y = ⟪f', y⟫

Tactic:
rw [h.hasFDerivWithinAt.fderivWithin hs, toDual_apply_apply]

Premises used: InnerProductSpace.toDual_apply_apply, HasFDerivWithinAt.fderivWithin, 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 y : F
h : HasGradientAt f f' x
rw : (((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F) f' : StrongDual 𝕜 F) : (a : F) → 𝕜) y = ⟪f', y⟫
rw₁ rw₂ : ⟪f', y⟫ = ⟪f', y⟫
⊢ ((fderiv 𝕜 f x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) y = ⟪f', y⟫

Tactic:
rw [h.hasFDerivAt.fderiv, toDual_apply_apply]

Premises used: InnerProductSpace.toDual_apply_apply, HasGradientAt.hasFDerivAt, HasFDerivAt.fderiv
-- 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 y : F
s : Set F
h : DifferentiableWithinAt 𝕜 f s x
hs : UniqueDiffWithinAt 𝕜 s x
rw rw₁ : ⟪gradientWithin f s x, y⟫ = ⟪gradientWithin f s x, y⟫
⊢ ⟪gradientWithin f s x, y⟫ = ((fderivWithin 𝕜 f s x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) y

Tactic:
rw [h.hasGradientWithinAt.fderivWithin_apply hs]

Premises used: HasGradientWithinAt.fderivWithin_apply, DifferentiableWithinAt.hasGradientWithinAt
-- 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 y : F
h : DifferentiableAt 𝕜 f x
rw rw₁ : ⟪∇ f x, y⟫ = ⟪∇ f x, y⟫
⊢ ⟪∇ f x, y⟫ = ((fderiv 𝕜 f x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) y

Tactic:
rw [h.hasGradientAt.fderiv_apply]

Premises used: DifferentiableAt.hasGradientAt, HasGradientAt.fderiv_apply
-- 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 y : F
s : Set F
h : DifferentiableWithinAt 𝕜 f s y
hs : UniqueDiffWithinAt 𝕜 s y
rw :
  Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪gradientWithin f s y, x⟫ : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (((fderivWithin 𝕜 f s y : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜) : 𝕜)
rw₁ rw₂ :
  Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (((fderivWithin 𝕜 f s y : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜) : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (((fderivWithin 𝕜 f s y : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜) : 𝕜)
⊢ ⟪x, gradientWithin f s y⟫ = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (((fderivWithin 𝕜 f s y : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜)

Tactic:
rw [← inner_conj_symm, inner_gradientWithin_left h hs]

Premises used: inner_gradientWithin_left, inner_conj_symm
-- 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 y : F
h : DifferentiableAt 𝕜 f y
rw :
  Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪∇ f y, x⟫ : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (((fderiv 𝕜 f y : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜) : 𝕜)
rw₁ rw₂ : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪∇ f y, x⟫ : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪∇ f y, x⟫ : 𝕜)
⊢ ⟪x, ∇ f y⟫ = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (((fderiv 𝕜 f y : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜)

Tactic:
rw [← inner_conj_symm, h.hasGradientAt.fderiv_apply]

Premises used: DifferentiableAt.hasGradientAt, HasGradientAt.fderiv_apply, inner_conj_symm
-- 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
x : F
L : Filter F
f₀ f₁ : F → 𝕜
f₀' f₁' : F
h₀ : f₀ =ᶠ[L] f₁
hx : f₀ x = f₁ x
h₁ : f₀' = f₁'
⊢ f₀ =ᶠ[pure x] f₁

Tactic:
assumption
-- 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
x : F
L : Filter F
f₀ f₁ : F → 𝕜
f₀' f₁' : F
h₀ : f₀ =ᶠ[L] f₁
hx : f₀ x = f₁ x
h₁ : f₀' = f₁'
⊢ ∀ (x : F),
    Eq.{u_1 + 1} (α := 𝕜) ((((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F) f₀' : StrongDual 𝕜 F) : (a : F) → 𝕜) x : 𝕜)
      ((((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F) f₁' : StrongDual 𝕜 F) : (a : F) → 𝕜) x : 𝕜)

Tactic:
simp [h₁]
-- 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
f₁ : F → 𝕜
h : HasGradientAtFilter f f' x L
hL : f₁ =ᶠ[L] f
hx : f₁ x = f x
rwa rwa₁ rwa₂ rwa₃ : HasGradientAtFilter f f' x L
⊢ HasGradientAtFilter f₁ f' x L

Tactic:
rwa [hL.hasGradientAtFilter_iff hx rfl]

Premises used: Filter.EventuallyEq.hasGradientAtFilter_iff, 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
f₁ : F → 𝕜
t : Set F
h : HasGradientWithinAt f f' s x
ht : ∀ x ∈ t, f₁ x = f x
hx : f₁ x = f x
h₁ : t ⊆ s
⊢ HasGradientWithinAt f₁ f' t x

Tactic:
HasFDerivWithinAt.congr_mono h ht hx h₁

Premises used: HasGradientAtFilter, HasGradientWithinAt, HasFDerivWithinAt, HasFDerivWithinAt.congr_mono
-- 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
f₁ : F → 𝕜
h : HasGradientWithinAt f f' s x
hs : ∀ x ∈ s, f₁ x = f x
hx : f₁ x = f x
tauto tauto₁ tauto₂ : ∀ ⦃a : F⦄, a ∈ s → a ∈ s
⊢ s ⊆ s

Tactic:
tauto
-- 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
f₁ : F → 𝕜
h : HasGradientWithinAt f f' s x
hs : ∀ x ∈ s, f₁ x = f x
hx : x ∈ s
⊢ HasGradientWithinAt f₁ f' s x

Tactic:
h.congr hs (hs _ hx)

Premises used: HasGradientWithinAt.congr
-- 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
f₁ : F → 𝕜
h : HasGradientWithinAt f f' s x
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ HasGradientWithinAt f₁ f' s x

Tactic:
HasGradientAtFilter.congr_of_eventuallyEq h h₁ hx

Premises used: HasGradientWithinAt, HasGradientAtFilter.congr_of_eventuallyEq
-- 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
f₁ : F → 𝕜
h : HasGradientWithinAt f f' s x
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : x ∈ s
⊢ HasGradientWithinAt f₁ f' s x

Tactic:
h.congr_of_eventuallyEq h₁ (h₁.eq_of_nhdsWithin hx)

Premises used: Filter.EventuallyEq.eq_of_nhdsWithin, HasGradientWithinAt.congr_of_eventuallyEq
-- 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
f₁ : F → 𝕜
h : HasGradientAt f f' x
h₁ : f₁ =ᶠ[𝓝 x] f
⊢ HasGradientAt f₁ f' x

Tactic:
HasGradientAtFilter.congr_of_eventuallyEq h h₁ (mem_of_mem_nhds h₁ :)

Premises used: HasGradientAtFilter.congr_of_eventuallyEq, mem_of_mem_nhds, 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
f₁ : F → 𝕜
hL : f₁ =ᶠ[𝓝 x] f
unfold :
  Eq.{u_2 + 1} (α := F)
    ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) (fderiv 𝕜 f₁ x : F →L[𝕜] 𝕜) : F)
    ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) (fderiv 𝕜 f x : F →L[𝕜] 𝕜) : F)
⊢ ∇ f₁ x = ∇ f x

Tactic:
unfold gradient

Premises used: gradient
-- 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
f₁ : F → 𝕜
hL : f₁ =ᶠ[𝓝 x] f
rwa :
  Eq.{u_2 + 1} (α := F)
    ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) (fderiv 𝕜 f x : F →L[𝕜] 𝕜) : F)
    ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) (fderiv 𝕜 f x : F →L[𝕜] 𝕜) : F)
rwa₁ : f₁ =ᶠ[𝓝 x] f
rwa₂ : F → 𝕜
rwa₃ :
  Eq.{u_2 + 1} (α := F)
    ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) (fderiv 𝕜 f x : F →L[𝕜] 𝕜) : F)
    ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) (fderiv 𝕜 f x : F →L[𝕜] 𝕜) : F)
rwa₄ : f₁ =ᶠ[𝓝 x] f
rwa₅ : F → 𝕜
rwa₆ rwa₇ : f₁ =ᶠ[𝓝 x] f
⊢ Eq.{u_2 + 1} (α := F)
    ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) (fderiv 𝕜 f₁ x : F →L[𝕜] 𝕜) : F)
    ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) (fderiv 𝕜 f x : F →L[𝕜] 𝕜) : F)

Tactic:
rwa [Filter.EventuallyEq.fderiv_eq]

Premises used: Filter.EventuallyEq.fderiv_eq
-- 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
f₁ : F → 𝕜
h : f₁ =ᶠ[𝓝 x] f
⊢ ∇ f₁ =ᶠ[𝓝 x] ∇ f

Tactic:
h.eventuallyEq_nhds.mono fun _ h => h.gradient_eq

Premises used: Filter.EventuallyEq, Filter.EventuallyEq.eventuallyEq_nhds, Filter.EventuallyEq.gradient_eq, Filter.Eventually.mono
-- 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
x : F
L : Filter F
c : 𝕜
rw : HasFDerivAtFilter.{u_1, u_2, u_1} (𝕜 := 𝕜) (F := 𝕜) (fun (x : F) ↦ c) 0 (SProd.sprod (β := Filter F) L (pure x))
⊢ HasGradientAtFilter.{u_1, u_2} (𝕜 := 𝕜) (fun (x : F) ↦ c) 0 x L

Tactic:
rw [HasGradientAtFilter, map_zero]

Premises used: HasGradientAtFilter, map_zero
-- 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
x : F
L : Filter F
c : 𝕜
⊢ HasFDerivAtFilter.{u_1, u_2, u_1} (𝕜 := 𝕜) (F := 𝕜) (fun (x : F) ↦ c) 0 (SProd.sprod (β := Filter F) L (pure x))

Tactic:
hasFDerivAtFilter_const c _

Premises used: hasFDerivAtFilter_const
-- 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
x : F
L : Filter F
c : 𝕜
⊢ HasFDerivAtFilter.{u_1, u_2, u_1} (𝕜 := 𝕜) (F := 𝕜) (fun (x : F) ↦ c) 0 (SProd.sprod (β := Filter F) L (pure x))

Tactic:
exact hasFDerivAtFilter_const c _

Premises used: hasFDerivAtFilter_const
-- 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
x : F
s : Set F
c : 𝕜
⊢ HasGradientWithinAt.{u_1, u_2} (𝕜 := 𝕜) (fun (x : F) ↦ c) 0 s x

Tactic:
hasGradientAtFilter_const _ _ _

Premises used: hasGradientAtFilter_const, HasGradientWithinAt
-- 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
x : F
c : 𝕜
⊢ HasGradientAt.{u_1, u_2} (𝕜 := 𝕜) (fun (x : F) ↦ c) 0 x

Tactic:
hasGradientAtFilter_const _ _ _

Premises used: hasGradientAtFilter_const, 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
x : F
c : 𝕜
⊢ gradient.{u_1, u_2} (𝕜 := 𝕜) (fun (x : F) ↦ c) x = 0

Tactic:
simp [gradient]

Premises used: gradient
-- 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
x : F
c : 𝕜
⊢ ∇ (const F c) x = 0

Tactic:
gradient_fun_const x c

Premises used: gradient_fun_const
-- 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
c : 𝕜
⊢ Eq.{u_2 + 1} (α := (x : F) → F) (gradient.{u_1, u_2} (𝕜 := 𝕜) fun (x : F) ↦ c) fun (x : F) ↦ 0

Tactic:
funext fun x => gradient_const x c

Premises used: funext, gradient_const
-- 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
c : 𝕜
⊢ ∇ (const F c) = 0

Tactic:
gradient_fun_const' c

Premises used: gradient_fun_const'
-- 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
hL : L ≤ 𝓝 x
h : HasGradientAtFilter f f' x L
⊢ Tendsto f L (𝓝 (f x))

Tactic:
h.tendsto_nhds hL

Premises used: HasFDerivAtFilter.tendsto_nhds
-- 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
⊢ ContinuousWithinAt f s x

Tactic:
HasGradientAtFilter.tendsto_nhds inf_le_left h

Premises used: ContinuousWithinAt, HasGradientAtFilter.tendsto_nhds, inf_le_left
-- 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
⊢ ContinuousAt f x

Tactic:
HasGradientAtFilter.tendsto_nhds le_rfl h

Premises used: le_rfl, ContinuousAt, HasGradientAtFilter.tendsto_nhds
-- 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 → 𝕜
s : Set F
f' : F → F
h : ∀ x ∈ s, HasGradientAt f (f' x) x
⊢ ContinuousOn f s

Tactic:
fun x hx => (h x hx).continuousAt.continuousWithinAt

Premises used: HasGradientAt.continuousAt, ContinuousAt.continuousWithinAt, ContinuousOn
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
x : E
⊢ φ.prodFun x = (φ.leftFun x, φ.rightFun x)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
⊢ HasStrictFDerivAt (𝕜 := 𝕜) φ.prodFun
    (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) : E →L[𝕜] F × G) φ.pt

Tactic:
φ.hasStrictFDerivAt_leftFun.prodMk φ.hasStrictFDerivAt_rightFun

Premises used: ImplicitFunctionData.hasStrictFDerivAt_leftFun, HasStrictFDerivAt.prodMk, Function.prod, ContinuousLinearMap.prod, LinearMap.prod, ImplicitFunctionData.prodFun, ImplicitFunctionData.hasStrictFDerivAt_rightFun, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
rw : (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) : E →L[𝕜] F × G).IsInvertible
⊢ ContinuousLinearMap.IsInvertible (fderiv 𝕜 φ.prodFun φ.pt)

Tactic:
rw [φ.hasStrictFDerivAt.hasFDerivAt.fderiv]

Premises used: ImplicitFunctionData.hasStrictFDerivAt, HasStrictFDerivAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
⊢ (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) : E →L[𝕜] F × G).IsInvertible

Tactic:
ContinuousLinearMap.isInvertible_equiv

Premises used: ContinuousLinearMap.isInvertible_equiv
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
⊢ (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) : E →L[𝕜] F × G).IsInvertible

Tactic:
exact ContinuousLinearMap.isInvertible_equiv

Premises used: ContinuousLinearMap.isInvertible_equiv
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
⊢ φ.implicitFunction = Function.curry (↑(HasStrictFDerivAt.toOpenPartialHomeomorph φ.prodFun ⋯).symm : F × G → E)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
x : F
y : G
⊢ φ.implicitFunction x y = (↑φ.toOpenPartialHomeomorph.symm : F × G → E) (x, y)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
⊢ (↑φ.toOpenPartialHomeomorph : E → F × G) = φ.prodFun

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
x : E
⊢ (↑φ.toOpenPartialHomeomorph : E → F × G) x = (φ.leftFun x, φ.rightFun x)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.Implicit
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
G : Type u_4
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
⊢ φ.pt ∈ φ.toOpenPartialHomeomorph.source

Tactic:
φ.hasStrictFDerivAt.mem_toOpenPartialHomeomorph_source

Premises used: Set.Mem, HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source, ImplicitFunctionData.hasStrictFDerivAt