0 x = 0

Stream: new members

[VayusElytra]

Hi, this one is a really dumb question, but it's giving me surprising difficulty.
I have this as the current state of a proof:

F : Type
inst✝ : DivisionRing F
m : F
x : ↑(ZeroSubmod F)
0 : AddHom ↑(ZeroSubmod F) ↑(SelfSubmod F)
⊢ 0 (m • x) = m * 0 x

with helper definitions

def ZeroSubmod (F : Type u) [DivisionRing F] : ModuleCat.{u} F where
  carrier := PUnit.{u+1}

def SelfSubmod (F : Type u) [DivisionRing F] : ModuleCat.{u} F where
  carrier := F

All I need to close out this goal is the identity0 x = 0, that is to say that applying the zero morphism to any element yields the 0-element of the ring F. This feels like it should be really trivial, but the usual rw and dsimp are not making progress, and I am having some trouble finding the relevant theorem in the jungle of documentation. How do I do this then?

[Ruben Van de Velde]

I would need a #mwe to verify, but maybe docs#Pi.zero_apply

[VayusElytra]

(deleted)

[Junyan Xu]

Usually 0 x is defeq to 0, so exact (mul_zero m).symm solves the "relevant part".

[VayusElytra]

You are right that this works, thank you very much! I am really confused then why dsimp doesn't simplify 0 x to 0 in that relevant part, and why feeding.
Are there any other ways to refer to 0 objects in Lean? I find it confusing to have 0's everywhere in my code, that are misinterpreted as natural numbers or that aren't the exact 0 I am thinking of a quarter of the time. I've been working with modules for a week and I'm still not sure how to actually properly, unambiguously write down the additive unit