Reducing DFunLike applications

Stream: Is there code for X?

[Vincent Beffara]

I have this MWE:

import Mathlib

open SchwartzMap

example : True := by
  let f : 𝓢(ℝ, ℝ) := ⟨fun x => x, sorry, sorry⟩
  have key (x : ℝ) : f x = x := by
    simp [f]
    sorry
  trivial

After the simp call, the goal looks like

{ toFun := fun x => x, smooth' := ⋯, decay' := ⋯ } x = x

but I was expecting simp to close it (and rfl does, as do change x = x and the like). How do I tell simp to reduce this?

[Vincent Beffara]

Adding this above,

@[simp] lemma toSchwartz_apply (f : ℝ → ℂ) {h1 h2 x} : SchwartzMap.mk f h1 h2 x = f x := rfl

makes it work, but I can't figure if this is filling a hole in the SchwartzMap API or introducing a footgun defeating the point of DFunLike...

[Eric Wieser]

The missing lemma is

@[simp] lemma coe_mk (f : ℝ → ℂ) {h1 h2} : SchwartzMap.mk f h1 h2 = f := rfl

[Yaël Dillies]

([norm_cast]!)

[Vincent Beffara]

Eric Wieser said:

The missing lemma is

@[simp] lemma coe_mk (f : ℝ → ℂ) {h1 h2} : SchwartzMap.mk f h1 h2 = f := rfl

This does not reduce:

import Mathlib

open SchwartzMap

@[simp] lemma coe_mk (f : ℝ → ℂ) {h1 h2} : SchwartzMap.mk f h1 h2 = f := rfl

example : True := by
  let f : 𝓢(ℝ, ℝ) := ⟨fun x => x, sorry, sorry⟩
  have key (x : ℝ) : f x = x := by
    simp [f]
    sorry
  trivial