Defeq abuse with TangentSpace: how to solve?

Stream: mathlib4

[Michael Rothgang]

We may have a defeq abuse problem in differential geometry, for instance around scalar multiplication in tangent spaces. For a concrete example, let's look at #34262 (which proves/generalises mfderiv_const_smul, relating the mfderiv of a • f and f at x (for a scalar a). The proofs are a fair bit more painful than one would like.

Two elementary examples:

import Mathlib.Geometry.Manifold.MFDeriv.Basic

-- Let `M` be a manifold over the pair `(E, H)`, and `F` a normed space.
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  {s : Set M} {x : M} {z : M} {f g : M → F}
open Manifold

@[simp, mfld_simps]
theorem mfderiv_zero : mfderiv I 𝓘(𝕜, F) (0 : M → F) x = 0 :=
  mfderiv_const (c := (0 : F)) -- note that `by simp` does not work

example : mfderiv I 𝓘(𝕜, E') (0 • f) x = 0 := by
  -- `simp` alone does not work; removing the `congr` also breaks the proof
  rw [← mfderiv_zero]
  congr
  simp? says simp only [zero_nsmul]

In the second example, note that the left hand side is a tangent vector at (0 • f) x; I suspect this to create most of the trouble.

For a final challenge, try proving this:
``
example (v : TangentSpace I x) : mfderiv I 𝓘(𝕜, E') (0 • f) x v = 0 := sorry

Note that the previous example does not seem to help; doing

have : (0 : TangentSpace I x → TangentSpace 𝓘(𝕜, E') (f x)) v = 0 := sorry
rw [← this]

makes the goal superficially simpler, but I'm obviously missing a trick here, as I cannot reduce the goal to something not involving `v`. Neither `congr 1` nor `apply congrArg` seems to work.

I don't recall much recent discussion about this: one possible reason could be that we don't have that many results about tangent spaces and scalar multiplication (and for addition, this is less of an issue).

[Michael Rothgang]

Perhaps there's a magic trick here that will make all this disappear. If so, I'd love to be educated!

I suspect, though, that this shows we're also in DTT hell. While I'm able to work around it, a much better outcome would be reducing it. One standard option would be to make the identification explicit: define a new gadget def Foo {x y : M} (h : x = y) : TangentSpace I x ≃L[𝕜] TangentSpace I y, make TangentSpace irreducible and use this gadget to fix all statements. This would probably be fairly painful, but perhaps for similar gain.

What do you think? Do you see a better option?
CC @Yury G. Kudryashov @Heather Macbeth @Patrick Massot @Sébastien Gouëzel @Floris van Doorn

[Michael Rothgang]

@Oliver Nash (of course!)

[Sébastien Gouëzel]

For your question, it works just with

example (v : TangentSpace I x) : mfderiv I 𝓘(𝕜, F) (0 • f) x v = 0 := by
  have : (0 • f) = 0 := by simp
  rw [this]
  simp
  rfl

(and the previous one can also be done with

example : mfderiv I 𝓘(𝕜, F) (0 • f) x = 0 := by
  -- `simp` alone does not work; removing the `congr` also breaks the proof
  have : (0 • f) = 0 := by simp
  rw [this]
  simp

[Sébastien Gouëzel]

I agree with you that we're abusing defeqs everywhere here, but I kind of like that it just works. Especially when working with functions between vector spaces, this would be nightmarish without this possibility. Still, introducing a gadget like the one you mention to do things cleanly when defeq abuse gets stuck, is probably a good idea.

[Yury G. Kudryashov]

I think that reducing defeq abuse is a good idea, but I have much less experience with this part of the library than Sébastien.