refactor: allow deriv to be used on topological vector spaces (#19108)

Notably, this allows us to _state_ results about derivatives of matrices, without the statement encoding a choice of norm.
For now, it is not possible to prove any of these statements without locally constructing a norm.

This generalizes:

* `HasFDerivAtFilter`
* `HasFDerivWithinAt`
* `HasFDerivAt`
* `HasStrictFDerivAt`
* `DifferentiableWithinAt`
* `DifferentiableAt`
* `fderivWithin`
* `fderiv`
* `DifferentiableOn`
* `Differentiable`
* `HasDerivAtFilter`
* `HasDerivWithinAt`
* `HasDerivAt`
* `HasStrictDerivAt`
* `derivWithin`
* `deriv`

Continues from [this Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/generalizing.20deriv.20to.20TVS/near/482705911).

Mathlib/Analysis/Asymptotics/TVS.lean

@@ -28,6 +28,9 @@ thus reducing the definition to the classical one.
 
 This frees the user from having to chose a canonical norm, at the expense of having to pick a
 specific base ring.
+This is exactly the tradeoff we want in `HasFDerivAtFilter`,
+as there the base ring is already chosen,
+and this removes the choice of norm being part of the statement.
 
 This definition was added to the library in order to migrate Fréchet derivatives
 from normed vector spaces to topological vector spaces.
@@ -50,10 +53,6 @@ until someone will need it (e.g., to prove properties of the Fréchet derivative
 * `isLittleOTVS_iff_tendsto_inv_smul`: the equivalence to convergence of the ratio to zero
   in case of a topological vector space.
 
-## TODO
-
-Use this to redefine `HasFDerivAtFilter`, as the base ring is already chosen there, and this removes
-the choice of norm being part of the statement.
 -/
 
 open Set Filter Asymptotics Metric

Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean

@@ -334,7 +334,8 @@ theorem hasFTaylorSeriesUpToOn_succ_nat_iff_right {n : ℕ} :
         have :
           HasFDerivWithinAt (𝕜 := 𝕜) (continuousMultilinearCurryRightEquiv' 𝕜 m E F ∘ (p · m.succ))
             ((p x).shift m.succ).curryLeft s x := Htaylor.fderivWithin _ A x hx
-        rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff'] at this
+        rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff'
+            (f' := ((p x).shift m.succ).curryLeft)] at this
         convert this
         ext y v
         change

Mathlib/Analysis/Calculus/Deriv/Basic.lean

@@ -95,9 +95,13 @@ open Filter Asymptotics Set
 
 open ContinuousLinearMap (smulRight smulRight_one_eq_iff)
 
+section TVS
+
 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
-variable {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+variable {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
 
+section
+variable [ContinuousSMul 𝕜 F]
 /-- `f` has the derivative `f'` at the point `x` as `x` goes along the filter `L`.
 
 That is, `f x' = f x + (x' - x) • f' + o(x' - x)` where `x'` converges along the filter `L`.
@@ -125,6 +129,7 @@ That is, `f y - f z = (y - z) • f' + o(y - z)` as `y, z → x`. -/
 def HasStrictDerivAt (f : 𝕜 → F) (f' : F) (x : 𝕜) :=
   HasStrictFDerivAt f (smulRight (1 : 𝕜 →L[𝕜] 𝕜) f') x
 
+end
 /-- Derivative of `f` at the point `x` within the set `s`, if it exists.  Zero otherwise.
 
 If the derivative exists (i.e., `∃ f', HasDerivWithinAt f f' s x`), then
@@ -147,6 +152,8 @@ variable {x : 𝕜}
 variable {s t : Set 𝕜}
 variable {L L₁ L₂ : Filter 𝕜}
 
+section
+variable [ContinuousSMul 𝕜 F]
 /-- Expressing `HasFDerivAtFilter f f' x L` in terms of `HasDerivAtFilter` -/
 theorem hasFDerivAtFilter_iff_hasDerivAtFilter {f' : 𝕜 →L[𝕜] F} :
     HasFDerivAtFilter f f' x L ↔ HasDerivAtFilter f (f' 1) x L := by simp [HasDerivAtFilter]
@@ -201,22 +208,34 @@ theorem hasDerivAt_iff_hasFDerivAt {f' : F} :
 
 alias ⟨HasDerivAt.hasFDerivAt, _⟩ := hasDerivAt_iff_hasFDerivAt
 
+end
 theorem derivWithin_zero_of_not_differentiableWithinAt (h : ¬DifferentiableWithinAt 𝕜 f s x) :
     derivWithin f s x = 0 := by
   unfold derivWithin
   rw [fderivWithin_zero_of_not_differentiableWithinAt h]
   simp
 
+theorem differentiableWithinAt_of_derivWithin_ne_zero (h : derivWithin f s x ≠ 0) :
+    DifferentiableWithinAt 𝕜 f s x :=
+  not_imp_comm.1 derivWithin_zero_of_not_differentiableWithinAt h
+
+end TVS
+
+variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
+variable {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+
+variable {f f₀ f₁ : 𝕜 → F}
+variable {f' f₀' f₁' g' : F}
+variable {x : 𝕜}
+variable {s t : Set 𝕜}
+variable {L L₁ L₂ : Filter 𝕜}
+
 theorem derivWithin_zero_of_isolated (h : 𝓝[s \ {x}] x = ⊥) : derivWithin f s x = 0 := by
   rw [derivWithin, fderivWithin_zero_of_isolated h, ContinuousLinearMap.zero_apply]
 
 theorem derivWithin_zero_of_nmem_closure (h : x ∉ closure s) : derivWithin f s x = 0 := by
   rw [derivWithin, fderivWithin_zero_of_nmem_closure h, ContinuousLinearMap.zero_apply]
 
-theorem differentiableWithinAt_of_derivWithin_ne_zero (h : derivWithin f s x ≠ 0) :
-    DifferentiableWithinAt 𝕜 f s x :=
-  not_imp_comm.1 derivWithin_zero_of_not_differentiableWithinAt h
-
 theorem deriv_zero_of_not_differentiableAt (h : ¬DifferentiableAt 𝕜 f x) : deriv f x = 0 := by
   unfold deriv
   rw [fderiv_zero_of_not_differentiableAt h]

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Sébastien Gouëzel, Yury Kudryashov
 -/
 import Mathlib.Analysis.Calculus.TangentCone
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics
+import Mathlib.Analysis.Asymptotics.TVS
 
 /-!
 # The Fréchet derivative
@@ -78,8 +79,10 @@ see `Deriv.lean`.
 
 ## Implementation details
 
-The derivative is defined in terms of the `isLittleO` relation, but also
-characterized in terms of the `Tendsto` relation.
+The derivative is defined in terms of the `IsLittleOTVS` relation to ensure the definition does not
+ingrain a choice of norm, and is then quickly translated to the more convenient `IsLittleO` in the
+subsequent theorems.
+It is also characterized in terms of the `Tendsto` relation.
 
 We also introduce predicates `DifferentiableWithinAt 𝕜 f s x` (where `𝕜` is the base field,
 `f` the function to be differentiated, `x` the point at which the derivative is asserted to exist,
@@ -107,6 +110,10 @@ some boilerplate lemmas, but these can also be useful in their own right.
 Tests for this ability of the simplifier (with more examples) are provided in
 `Tests/Differentiable.lean`.
 
+## TODO
+
+Generalize more results to topological vector spaces.
+
 ## Tags
 
 derivative, differentiable, Fréchet, calculus
@@ -120,20 +127,20 @@ open Topology NNReal Filter Asymptotics ENNReal
 
 noncomputable section
 
-section
-
+section TVS
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+variable {E : Type*} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
+variable {F : Type*} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
 
 /-- A function `f` has the continuous linear map `f'` as derivative along the filter `L` if
 `f x' = f x + f' (x' - x) + o (x' - x)` when `x'` converges along the filter `L`. This definition
 is designed to be specialized for `L = 𝓝 x` (in `HasFDerivAt`), giving rise to the usual notion
 of Fréchet derivative, and for `L = 𝓝[s] x` (in `HasFDerivWithinAt`), giving rise to
 the notion of Fréchet derivative along the set `s`. -/
-@[mk_iff hasFDerivAtFilter_iff_isLittleO]
+@[mk_iff hasFDerivAtFilter_iff_isLittleOTVS]
 structure HasFDerivAtFilter (f : E → F) (f' : E →L[𝕜] F) (x : E) (L : Filter E) : Prop where
-  of_isLittleO :: isLittleO : (fun x' => f x' - f x - f' (x' - x)) =o[L] fun x' => x' - x
+  of_isLittleOTVS ::
+    isLittleOTVS : IsLittleOTVS 𝕜 (fun x' => f x' - f x - f' (x' - x)) (fun x' => x' - x) L
 
 /-- A function `f` has the continuous linear map `f'` as derivative at `x` within a set `s` if
 `f x' = f x + f' (x' - x) + o (x' - x)` when `x'` tends to `x` inside `s`. -/
@@ -151,10 +158,11 @@ def HasFDerivAt (f : E → F) (f' : E →L[𝕜] F) (x : E) :=
 if `f x - f y - f' (x - y) = o(x - y)` as `x, y → a`. This form of differentiability is required,
 e.g., by the inverse function theorem. Any `C^1` function on a vector space over `ℝ` is strictly
 differentiable but this definition works, e.g., for vector spaces over `p`-adic numbers. -/
-@[fun_prop, mk_iff hasStrictFDerivAt_iff_isLittleO]
+@[fun_prop, mk_iff hasStrictFDerivAt_iff_isLittleOTVS]
 structure HasStrictFDerivAt (f : E → F) (f' : E →L[𝕜] F) (x : E) where
-  of_isLittleO :: isLittleO :
-      (fun p : E × E => f p.1 - f p.2 - f' (p.1 - p.2)) =o[𝓝 (x, x)] fun p : E × E => p.1 - p.2
+  of_isLittleOTVS ::
+    isLittleOTVS : IsLittleOTVS 𝕜
+        (fun p : E × E => f p.1 - f p.2 - f' (p.1 - p.2)) (fun p : E × E => p.1 - p.2) (𝓝 (x, x))
 
 variable (𝕜)
 
@@ -210,6 +218,34 @@ theorem fderivWithin_univ : fderivWithin 𝕜 f univ = fderiv 𝕜 f := by
   ext
   rw [fderiv]
 
+end TVS
+
+section
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+
+variable {f f₀ f₁ g : E → F}
+variable {f' f₀' f₁' g' : E →L[𝕜] F}
+variable {x : E}
+variable {s t : Set E}
+variable {L L₁ L₂ : Filter E}
+
+theorem hasFDerivAtFilter_iff_isLittleO :
+    HasFDerivAtFilter f f' x L ↔ (fun x' => f x' - f x - f' (x' - x)) =o[L] fun x' => x' - x :=
+  (hasFDerivAtFilter_iff_isLittleOTVS ..).trans isLittleOTVS_iff_isLittleO
+
+alias ⟨HasFDerivAtFilter.isLittleO, HasFDerivAtFilter.of_isLittleO⟩ :=
+  hasFDerivAtFilter_iff_isLittleO
+
+theorem hasStrictFDerivAt_iff_isLittleO :
+    HasStrictFDerivAt f f' x ↔
+      (fun p : E × E => f p.1 - f p.2 - f' (p.1 - p.2)) =o[𝓝 (x, x)] fun p : E × E => p.1 - p.2 :=
+  (hasStrictFDerivAt_iff_isLittleOTVS ..).trans isLittleOTVS_iff_isLittleO
+
+alias ⟨HasStrictFDerivAt.isLittleO, HasStrictFDerivAt.of_isLittleO⟩ :=
+  hasStrictFDerivAt_iff_isLittleO
+
 section DerivativeUniqueness
 
 /- In this section, we discuss the uniqueness of the derivative.

Mathlib/Analysis/Calculus/FDeriv/Mul.lean

@@ -661,11 +661,14 @@ theorem HasStrictFDerivAt.list_prod' {l : List ι} {x : E}
     HasStrictFDerivAt (fun x ↦ (l.map (f · x)).prod)
       (∑ i : Fin l.length, ((l.take i).map (f · x)).prod •
         smulRight (f' l[i]) ((l.drop (.succ i)).map (f · x)).prod) x := by
-  simp only [← List.finRange_map_get l, List.map_map]
+  simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.finRange_map_get l, List.map_map]
+  -- After #19108, we have to be optimistic with `:)`s; otherwise Lean decides it need to find
+  -- `NormedAddCommGroup (List 𝔸)` which is nonsense.
   refine .congr_fderiv (hasStrictFDerivAt_list_prod_finRange'.comp x
-    (hasStrictFDerivAt_pi.mpr fun i ↦ h l[i] (List.getElem_mem ..))) ?_
+    (hasStrictFDerivAt_pi.mpr fun i ↦ h (l.get i) (List.getElem_mem ..)) :) ?_
   ext m
-  simp [← List.map_map]
+  simp_rw [List.map_take, List.map_drop, List.map_map, comp_apply, sum_apply, smul_apply,
+    smulRight_apply, proj_apply, pi_apply, Function.comp_def]
 
 /--
 Unlike `HasFDerivAt.finset_prod`, supports non-commutative multiply and duplicate elements.
@@ -676,23 +679,25 @@ theorem HasFDerivAt.list_prod' {l : List ι} {x : E}
     HasFDerivAt (fun x ↦ (l.map (f · x)).prod)
       (∑ i : Fin l.length, ((l.take i).map (f · x)).prod •
         smulRight (f' l[i]) ((l.drop (.succ i)).map (f · x)).prod) x := by
-  simp only [← List.finRange_map_get l, List.map_map]
+  simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.finRange_map_get l, List.map_map]
   refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp x
-    (hasFDerivAt_pi.mpr fun i ↦ h l[i] (l.getElem_mem _))) ?_
+    (hasFDerivAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_
   ext m
-  simp [← List.map_map]
+  simp_rw [List.map_take, List.map_drop, List.map_map, comp_apply, sum_apply, smul_apply,
+    smulRight_apply, proj_apply, pi_apply, Function.comp_def]
 
 @[fun_prop]
 theorem HasFDerivWithinAt.list_prod' {l : List ι} {x : E}
     (h : ∀ i ∈ l, HasFDerivWithinAt (f i ·) (f' i) s x) :
     HasFDerivWithinAt (fun x ↦ (l.map (f · x)).prod)
       (∑ i : Fin l.length, ((l.take i).map (f · x)).prod •
         smulRight (f' l[i]) ((l.drop (.succ i)).map (f · x)).prod) s x := by
-  simp only [← List.finRange_map_get l, List.map_map]
+  simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.finRange_map_get l, List.map_map]
   refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp_hasFDerivWithinAt x
-    (hasFDerivWithinAt_pi.mpr fun i ↦ h l[i] (l.getElem_mem _))) ?_
+    (hasFDerivWithinAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_
   ext m
-  simp [← List.map_map]
+  simp_rw [List.map_take, List.map_drop, List.map_map, comp_apply, sum_apply, smul_apply,
+    smulRight_apply, proj_apply, pi_apply, Function.comp_def]
 
 theorem fderiv_list_prod' {l : List ι} {x : E}
     (h : ∀ i ∈ l, DifferentiableAt 𝕜 (f i ·) x) :
@@ -715,7 +720,8 @@ theorem HasStrictFDerivAt.multiset_prod [DecidableEq ι] {u : Multiset ι} {x :
       (u.map fun i ↦ ((u.erase i).map (g · x)).prod • g' i).sum x := by
   simp only [← Multiset.attach_map_val u, Multiset.map_map]
   exact .congr_fderiv
-    (hasStrictFDerivAt_multiset_prod.comp x <| hasStrictFDerivAt_pi.mpr fun i ↦ h i i.prop)
+    (hasStrictFDerivAt_multiset_prod.comp x <|
+      hasStrictFDerivAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
     (by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])
 
 /--
@@ -728,7 +734,7 @@ theorem HasFDerivAt.multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E}
       (u.map fun i ↦ ((u.erase i).map (g · x)).prod • g' i).sum x := by
   simp only [← Multiset.attach_map_val u, Multiset.map_map]
   exact .congr_fderiv
-    (hasFDerivAt_multiset_prod.comp x <| hasFDerivAt_pi.mpr fun i ↦ h i i.prop)
+    (hasFDerivAt_multiset_prod.comp x <| hasFDerivAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
     (by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])
 
 @[fun_prop]
@@ -739,7 +745,7 @@ theorem HasFDerivWithinAt.multiset_prod [DecidableEq ι] {u : Multiset ι} {x :
   simp only [← Multiset.attach_map_val u, Multiset.map_map]
   exact .congr_fderiv
     (hasFDerivAt_multiset_prod.comp_hasFDerivWithinAt x <|
-      hasFDerivWithinAt_pi.mpr fun i ↦ h i i.prop)
+      hasFDerivWithinAt_pi.mpr fun i ↦ h (Subtype.val i) i.prop :)
     (by ext; simp [Finset.sum_multiset_map_count, u.erase_attach_map (g · x)])
 
 theorem fderiv_multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E}
@@ -765,15 +771,15 @@ theorem HasFDerivAt.finset_prod [DecidableEq ι] {x : E}
     (hg : ∀ i ∈ u, HasFDerivAt (g i) (g' i) x) :
     HasFDerivAt (∏ i ∈ u, g i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x := by
   simpa [← Finset.prod_attach u] using .congr_fderiv
-    (hasFDerivAt_finset_prod.comp x <| hasFDerivAt_pi.mpr fun i ↦ hg i i.prop)
+    (hasFDerivAt_finset_prod.comp x <| hasFDerivAt_pi.mpr fun i ↦ hg (Subtype.val i) i.prop :)
     (by ext; simp [Finset.prod_erase_attach (g · x), ← u.sum_attach])
 
 theorem HasFDerivWithinAt.finset_prod [DecidableEq ι] {x : E}
     (hg : ∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x) :
     HasFDerivWithinAt (∏ i ∈ u, g i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) s x := by
   simpa [← Finset.prod_attach u] using .congr_fderiv
     (hasFDerivAt_finset_prod.comp_hasFDerivWithinAt x <|
-      hasFDerivWithinAt_pi.mpr fun i ↦ hg i i.prop)
+      hasFDerivWithinAt_pi.mpr fun i ↦ hg (Subtype.val i) i.prop :)
     (by ext; simp [Finset.prod_erase_attach (g · x), ← u.sum_attach])
 
 theorem fderiv_finset_prod [DecidableEq ι] {x : E} (hg : ∀ i ∈ u, DifferentiableAt 𝕜 (g i) x) :

Mathlib/Analysis/Calculus/FDeriv/WithLp.lean

@@ -67,7 +67,7 @@ theorem hasStrictFDerivAt_equiv_symm (f : PiLp p E) :
 
 nonrec theorem hasStrictFDerivAt_apply (f : PiLp p E) (i : ι) :
     HasStrictFDerivAt (𝕜 := 𝕜) (fun f : PiLp p E => f i) (proj p E i) f :=
-  (hasStrictFDerivAt_apply i f).comp f (hasStrictFDerivAt_equiv p f)
+  (hasStrictFDerivAt_apply i f).comp f (hasStrictFDerivAt_equiv (𝕜 := 𝕜) p f)
 
 theorem hasFDerivAt_equiv (f : PiLp p E) :
     HasFDerivAt (WithLp.equiv p (∀ i, E i))

Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

@@ -542,8 +542,9 @@ theorem fourierIntegral_iteratedFDeriv [FiniteDimensional ℝ V]
     ext w m
     have J : Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ := by
       specialize h'f (n + 1) hn
-      rw [iteratedFDeriv_succ_eq_comp_left] at h'f
-      exact (LinearIsometryEquiv.integrable_comp_iff _).1 h'f
+      rwa [iteratedFDeriv_succ_eq_comp_left, Function.comp_def,
+          LinearIsometryEquiv.integrable_comp_iff (𝕜 := ℝ) (φ := fderiv ℝ (iteratedFDeriv ℝ n f))]
+        at h'f
     suffices H : (fourierIntegral 𝐞 μ L.toLinearMap₂ (fderiv ℝ (iteratedFDeriv ℝ n f)) w)
           (m 0) (Fin.tail m) =
         (-(2 * π * I)) ^ (n + 1) • (∏ x : Fin (n + 1), -L (m x) w) • ∫ v, 𝐞 (-L v w) • f v ∂μ by

Mathlib/Analysis/InnerProductSpace/Calculus.lean

@@ -111,12 +111,11 @@ theorem HasDerivAt.inner {f g : ℝ → E} {f' g' : E} {x : ℝ} :
 
 theorem DifferentiableWithinAt.inner (hf : DifferentiableWithinAt ℝ f s x)
     (hg : DifferentiableWithinAt ℝ g s x) : DifferentiableWithinAt ℝ (fun x => ⟪f x, g x⟫) s x :=
-  ((differentiable_inner _).hasFDerivAt.comp_hasFDerivWithinAt x
-      (hf.prod hg).hasFDerivWithinAt).differentiableWithinAt
+  (hf.hasFDerivWithinAt.inner 𝕜 hg.hasFDerivWithinAt).differentiableWithinAt
 
 theorem DifferentiableAt.inner (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) :
     DifferentiableAt ℝ (fun x => ⟪f x, g x⟫) x :=
-  (differentiable_inner _).comp x (hf.prod hg)
+  (hf.hasFDerivAt.inner 𝕜 hg.hasFDerivAt).differentiableAt
 
 theorem DifferentiableOn.inner (hf : DifferentiableOn ℝ f s) (hg : DifferentiableOn ℝ g s) :
     DifferentiableOn ℝ (fun x => ⟪f x, g x⟫) s := fun x hx => (hf x hx).inner 𝕜 (hg x hx)

Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean

@@ -49,7 +49,7 @@ theorem hasStrictDerivAt_const_cpow {x y : ℂ} (h : x ≠ 0 ∨ y ≠ 0) :
   rcases em (x = 0) with (rfl | hx)
   · replace h := h.neg_resolve_left rfl
     rw [log_zero, mul_zero]
-    refine (hasStrictDerivAt_const _ 0).congr_of_eventuallyEq ?_
+    refine (hasStrictDerivAt_const y 0).congr_of_eventuallyEq ?_
     exact (isOpen_ne.eventually_mem h).mono fun y hy => (zero_cpow hy).symm
   · simpa only [cpow_def_of_ne_zero hx, mul_one] using
       ((hasStrictDerivAt_id y).const_mul (log x)).cexp
@@ -307,7 +307,7 @@ theorem hasStrictDerivAt_rpow_const_of_ne {x : ℝ} (hx : x ≠ 0) (p : ℝ) :
     HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x := by
   cases' hx.lt_or_lt with hx hx
   · have := (hasStrictFDerivAt_rpow_of_neg (x, p) hx).comp_hasStrictDerivAt x
-      ((hasStrictDerivAt_id x).prod (hasStrictDerivAt_const _ _))
+      ((hasStrictDerivAt_id x).prod (hasStrictDerivAt_const x p))
     convert this using 1; simp
   · simpa using (hasStrictDerivAt_id x).rpow (hasStrictDerivAt_const x p) hx
 

Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean

@@ -28,7 +28,7 @@ theorem deriv_arcsin_aux {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :
     rw [sqrt_eq_zero'.2 this.le, div_zero]
     have : arcsin =ᶠ[𝓝 x] fun _ => -(π / 2) :=
       (gt_mem_nhds h₁).mono fun y hy => arcsin_of_le_neg_one hy.le
-    exact ⟨(hasStrictDerivAt_const _ _).congr_of_eventuallyEq this.symm,
+    exact ⟨(hasStrictDerivAt_const x _).congr_of_eventuallyEq this.symm,
       contDiffAt_const.congr_of_eventuallyEq this⟩
   cases' h₂.lt_or_lt with h₂ h₂
   · have : 0 < √(1 - x ^ 2) := sqrt_pos.2 (by nlinarith [h₁, h₂])
@@ -39,7 +39,7 @@ theorem deriv_arcsin_aux {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :
   · have : 1 - x ^ 2 < 0 := by nlinarith [h₂]
     rw [sqrt_eq_zero'.2 this.le, div_zero]
     have : arcsin =ᶠ[𝓝 x] fun _ => π / 2 := (lt_mem_nhds h₂).mono fun y hy => arcsin_of_one_le hy.le
-    exact ⟨(hasStrictDerivAt_const _ _).congr_of_eventuallyEq this.symm,
+    exact ⟨(hasStrictDerivAt_const x _).congr_of_eventuallyEq this.symm,
       contDiffAt_const.congr_of_eventuallyEq this⟩
 
 theorem hasStrictDerivAt_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :

Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean

@@ -326,7 +326,7 @@ lemma continuousAt_jacobiTheta₂ (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) :
 /-- Differentiability of `Θ z τ` in `z`, for fixed `τ`. -/
 lemma differentiableAt_jacobiTheta₂_fst (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) :
     DifferentiableAt ℂ (jacobiTheta₂ · τ) z :=
- ((hasFDerivAt_jacobiTheta₂ z hτ).comp z (hasFDerivAt_prod_mk_left z τ)).differentiableAt
+ ((hasFDerivAt_jacobiTheta₂ z hτ).comp (𝕜 := ℂ) z (hasFDerivAt_prod_mk_left z τ) :).differentiableAt
 
 /-- Differentiability of `Θ z τ` in `τ`, for fixed `z`. -/
 lemma differentiableAt_jacobiTheta₂_snd (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) :