awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
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
⊢ Eq (α := FormalMultilinearSeries 𝕜 E G) (p.compContinuousLinearMap 0)
    (constFormalMultilinearSeries 𝕜 E ((p 0 : (a : (i : Fin 0) → F) → G) 0))
have h : ∀ (n : ℕ) (v : (i : Fin n) → E),
  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: ext n v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
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.{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)
have 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)
Tactic: simp only [FormalMultilinearSeries.compContinuousLinearMap_apply, Matrix.zero_empty,
      constFormalMultilinearSeries_apply_zero, ContinuousMultilinearMap.uncurry0_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
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.{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)
have h : Eq.{w + 1} (α := (i : Fin 0) → F) ((⇑0 : (a : E) → F) ∘ v) ![]
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
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
⊢ 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)
have 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)
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']
Cleared hypotheses: n, v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
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)
⊢ 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)
have 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)
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']
Cleared hypotheses: n, v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ HasFDerivWithinAt (𝕜 := 𝕜) f frechet s x ↔
    HasGradientWithinAt f ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) frechet) s x
have 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
Tactic: rw [hasGradientWithinAt_iff_hasFDerivWithinAt, (toDual 𝕜 F).apply_symm_apply frechet]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ HasFDerivWithinAt (𝕜 := 𝕜) f frechet s x ↔
    HasGradientWithinAt f ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) frechet) s x
have rw₁ : HasFDerivWithinAt (𝕜 := 𝕜) f frechet s x ↔ HasFDerivWithinAt (𝕜 := 𝕜) f frechet s x
Tactic: rw [hasGradientWithinAt_iff_hasFDerivWithinAt, (toDual 𝕜 F).apply_symm_apply frechet]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ HasFDerivAt (𝕜 := 𝕜) f frechet x ↔
    HasGradientAt f ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) frechet) x
have rw : HasFDerivAt (𝕜 := 𝕜) f frechet x ↔
  HasFDerivAt (𝕜 := 𝕜) f
    ((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F)
      ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) frechet))
    x
Tactic: rw [hasGradientAt_iff_hasFDerivAt, (toDual 𝕜 F).apply_symm_apply frechet]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ HasFDerivAt (𝕜 := 𝕜) f frechet x ↔
    HasGradientAt f ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) frechet) x
have rw₁ : HasFDerivAt (𝕜 := 𝕜) f frechet x ↔ HasFDerivAt (𝕜 := 𝕜) f frechet x
Tactic: rw [hasGradientAt_iff_hasFDerivAt, (toDual 𝕜 F).apply_symm_apply frechet]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ ∇ f x = 0
have rw : Eq.{u_2 + 1} (α := F)
  ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) (fderiv 𝕜 f x : F →L[𝕜] 𝕜) : F) (0 : F)
Tactic: rw [gradient, fderiv_zero_of_not_differentiableAt h, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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)
⊢ ∇ f x = 0
have rw₁ : Eq.{u_2 + 1} (α := F) ((LinearIsometryEquiv.symm (toDual 𝕜 F) : (a : StrongDual 𝕜 F) → F) 0 : F) (0 : F)
Tactic: rw [gradient, fderiv_zero_of_not_differentiableAt h, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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)
⊢ ∇ f x = 0
have rw₂ : Eq.{u_2 + 1} (α := F) 0 0
Tactic: rw [gradient, fderiv_zero_of_not_differentiableAt h, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ HasGradientAt f (∇ f x) x
have rw : HasFDerivAt f (fderiv 𝕜 f x) x
Tactic: rw [hasGradientAt_iff_hasFDerivAt, gradient, (toDual 𝕜 F).apply_symm_apply (fderiv 𝕜 f x)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ HasGradientWithinAt f (gradientWithin f s x) s x
have rw : HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x
Tactic: rw [hasGradientWithinAt_iff_hasFDerivWithinAt, gradientWithin,
    (toDual 𝕜 F).apply_symm_apply (fderivWithin 𝕜 f s x)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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'))
have h₁ : Eq (α := 𝕜) ((ContinuousLinearMap.smulRight (S := 𝕜) 1 g' : (a : 𝕜) → 𝕜) 1 : 𝕜)
  ((((toDual 𝕜 𝕜 : (a : 𝕜) → StrongDual 𝕜 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') : StrongDual 𝕜 𝕜) : (a : 𝕜) → 𝕜) 1 : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasDerivAtFilter g g' (SProd.sprod (β := Filter 𝕜) L' (pure u))
⊢ HasGradientAtFilter g ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') u L'
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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'))
⊢ HasGradientAtFilter g ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') u L'
have rwa : HasFDerivAtFilter (𝕜 := 𝕜) g ((toDual 𝕜 𝕜 : (a : 𝕜) → StrongDual 𝕜 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g'))
  (SProd.sprod (β := Filter 𝕜) L' (pure u))
Tactic: rwa [HasGradientAtFilter, ← this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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))
⊢ HasGradientAtFilter g ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') u L'
have rwa₁ : HasFDerivAtFilter (𝕜 := 𝕜) g (ContinuousLinearMap.smulRight (S := 𝕜) 1 g') (SProd.sprod (β := Filter 𝕜) L' (pure u))
Tactic: rwa [HasGradientAtFilter, ← this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasGradientAt g g' u
⊢ HasDerivAt g ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') u
have h₁ : HasDerivAt g ((((toDual 𝕜 𝕜 : (a : 𝕜) → StrongDual 𝕜 𝕜) g' : StrongDual 𝕜 𝕜) : (a : 𝕜) → 𝕜) 1) u
Tactic: rw [hasGradientAt_iff_hasFDerivAt, hasFDerivAt_iff_hasDerivAt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
h : HasDerivAt g g' u
⊢ HasGradientAt g ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') u
have rw : HasDerivAt g
  ((((toDual 𝕜 𝕜 : (a : 𝕜) → StrongDual 𝕜 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) g') : StrongDual 𝕜 𝕜) : (a : 𝕜) → 𝕜) 1) u
Tactic: rw [hasGradientAt_iff_hasFDerivAt, hasFDerivAt_iff_hasDerivAt]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
⊢ ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)
have pos : ∀ (h : DifferentiableAt 𝕜 g u), ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)
Tactic: by_cases h : DifferentiableAt 𝕜 g u
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
pos : ∀ (h : DifferentiableAt 𝕜 g u), ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)
⊢ ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)
have neg : ∀ (h : ¬DifferentiableAt 𝕜 g u), ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)
Tactic: by_cases h : DifferentiableAt 𝕜 g u
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : DifferentiableAt 𝕜 g u
⊢ ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)
have pos : ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∇ g u) : 𝕜)
Tactic: rw [h.hasGradientAt.hasDerivAt.deriv, RCLike.conj_conj]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : DifferentiableAt 𝕜 g u
pos : ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∇ g u) : 𝕜)
⊢ ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)
have pos₁ : ∇ g u = ∇ g u
Tactic: rw [h.hasGradientAt.hasDerivAt.deriv, RCLike.conj_conj]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : ¬DifferentiableAt 𝕜 g u
⊢ ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)
have neg : Eq (α := 𝕜) (0 : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u) : 𝕜)
Tactic: rw [gradient_eq_zero_of_not_differentiableAt h, deriv_zero_of_not_differentiableAt h, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : ¬DifferentiableAt 𝕜 g u
neg : Eq (α := 𝕜) (0 : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u) : 𝕜)
⊢ ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)
have neg₁ : Eq (α := 𝕜) (0 : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜)
Tactic: rw [gradient_eq_zero_of_not_differentiableAt h, deriv_zero_of_not_differentiableAt h, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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 : 𝕜)
⊢ ∇ g u = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (deriv g u)
have neg₂ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [gradient_eq_zero_of_not_differentiableAt h, deriv_zero_of_not_differentiableAt h, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ ((fderivWithin 𝕜 f s x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) y = ⟪f', y⟫
have rw : (((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F) f' : StrongDual 𝕜 F) : (a : F) → 𝕜) y = ⟪f', y⟫
Tactic: rw [h.hasFDerivWithinAt.fderivWithin hs, toDual_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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⟫
⊢ ((fderivWithin 𝕜 f s x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) y = ⟪f', y⟫
have rw₁ : ⟪f', y⟫ = ⟪f', y⟫
Tactic: rw [h.hasFDerivWithinAt.fderivWithin hs, toDual_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ ((fderiv 𝕜 f x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) y = ⟪f', y⟫
have rw : (((toDual 𝕜 F : (a : F) → StrongDual 𝕜 F) f' : StrongDual 𝕜 F) : (a : F) → 𝕜) y = ⟪f', y⟫
Tactic: rw [h.hasFDerivAt.fderiv, toDual_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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⟫
⊢ ((fderiv 𝕜 f x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) y = ⟪f', y⟫
have rw₁ : ⟪f', y⟫ = ⟪f', y⟫
Tactic: rw [h.hasFDerivAt.fderiv, toDual_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ ⟪gradientWithin f s x, y⟫ = ((fderivWithin 𝕜 f s x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) y
have rw : ⟪gradientWithin f s x, y⟫ = ⟪gradientWithin f s x, y⟫
Tactic: rw [h.hasGradientWithinAt.fderivWithin_apply hs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ ⟪∇ f x, y⟫ = ((fderiv 𝕜 f x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) y
have rw : ⟪∇ f x, y⟫ = ⟪∇ f x, y⟫
Tactic: rw [h.hasGradientAt.fderiv_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ ⟪x, gradientWithin f s y⟫ = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (((fderivWithin 𝕜 f s y : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜)
have rw : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪gradientWithin f s y, x⟫ : 𝕜)
  ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (((fderivWithin 𝕜 f s y : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜) : 𝕜)
Tactic: rw [← inner_conj_symm, inner_gradientWithin_left h hs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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 : 𝕜) : 𝕜)
⊢ ⟪x, gradientWithin f s y⟫ = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (((fderivWithin 𝕜 f s y : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜)
have rw₁ : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (((fderivWithin 𝕜 f s y : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜) : 𝕜)
  ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (((fderivWithin 𝕜 f s y : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜) : 𝕜)
Tactic: rw [← inner_conj_symm, inner_gradientWithin_left h hs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ ⟪x, ∇ f y⟫ = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (((fderiv 𝕜 f y : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜)
have rw : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪∇ f y, x⟫ : 𝕜)
  ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (((fderiv 𝕜 f y : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜) : 𝕜)
Tactic: rw [← inner_conj_symm, h.hasGradientAt.fderiv_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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 : 𝕜) : 𝕜)
⊢ ⟪x, ∇ f y⟫ = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (((fderiv 𝕜 f y : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜)
have rw₁ : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪∇ f y, x⟫ : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪∇ f y, x⟫ : 𝕜)
Tactic: rw [← inner_conj_symm, h.hasGradientAt.fderiv_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ s ⊆ s
have tauto : ∀ ⦃a : F⦄, a ∈ s → a ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Gradient.Basic (goal)
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
⊢ ∇ f₁ x = ∇ f x
have 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)
Tactic: unfold gradient