Proofs when defining structures

Stream: lean4

[Frédéric Dupuis]

In the following bit of code, map_smul' should be ∀ m x, f (m • x) = m • f x, where f is the relevant toFun. However, when trying to provide the proof, f is actually called some inaccessible name like (↑__src✝).toFun. How can I give it a proper name that can be worked with? In the docs it's called self.toFun but that doesn't seem to work either.

import Mathlib.Algebra.Module.LinearMap.Defs

variable {R M : Type*} [Ring R] [AddCommGroup M] [Module R M]

def foo : M →+ M where
  toFun := id
  map_add' := by simp
  map_zero' := by simp

def bar : M →ₗ[R] M :=
  { foo with
    map_smul' := by sorry }

If there's only foo and I'm working on map_add', I can at least work around this by calling f whatever is on the RHS of toFun (i.e. id in this case), but in the second structure I can't even do that.

[Kyle Miller]

One trick here is to do the let lifting that Lean does yourself:

def bar : M →ₗ[R] M :=
  let f := foo
  { f with
    map_smul' := by sorry }

[Kyle Miller]

Or you can use Mathlib's spread notation, which currently has a hack that makes dsimp be able to simplify the inaccessible names. (Edit: I misremembered the purpose of the hack; it's to make it so whatever comes after __ := is also available as an instance. It's not about whether dsimp can unfold it.)

def bar : M →ₗ[R] M where
  __ := foo
  map_smul' := by
    dsimp only
    -- ⊢ ∀ (m : R) (x : M), (↑foo).toFun (m • x) = (RingHom.id R) m • (↑foo).toFun x
    sorry

[Kyle Miller]

Oh, I didn't check before testing the above, it looks like dsimp only simplifies your original case too.

def bar : M →ₗ[R] M :=
  { foo with
    map_smul' := by
      dsimp only
      -- ⊢ ∀ (m : R) (x : M), (↑foo).toFun (m • x) = (RingHom.id R) m • (↑foo).toFun x
      sorry }

[Frédéric Dupuis]

I see, thanks!