Avoiding "motive is not type correct" with `PartENat`

Stream: general

[Daniel Weber]

I need to use docs#multiplicity, but whenever I try to rewrite anything I get "motive is not type correct". Am I using it incorrectly? Is there a better alternative?
For instance

import Mathlib

example  {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] [DecidableRel fun (x x_1 : α) => (multiplicity x x_1).Dom]
    {a : α} {b : α} (h : ¬a ∣ b) : (multiplicity a b).getOrElse 0 = 0 := by
  have := multiplicity.multiplicity_eq_zero.mpr h
  rw [this] -- tactic 'rewrite' failed, motive is not type correct
  sorry

[Yaël Dillies]

Hot take: multiplicity is broken, which is why nobody uses it

[Daniel Weber]

For some background, I'm trying to define valuation in a general fraction ring

variable {F K : Type*} [CommRing F] [IsDomain F] [UniqueFactorizationMonoid F] [Field K]
  [Algebra F K] [IsFractionRing F K]
  [DecidableRel fun (a b : F) => a ∣ b] [DecidableRel fun (a b : F) => (multiplicity a b).Dom]

instance AddDecidable (a b : PartENat) [Decidable a.Dom] [Decidable b.Dom] :
    Decidable (a+b).Dom := instDecidableAnd

open IsFractionRing algebraMap

def PartENat.toWTZ (x : PartENat) [Decidable x.Dom] : WithTop ℤ :=
  if h : x.Dom then x.get h else ⊤

noncomputable def vp (p : F) (v : K) :=
  (multiplicity p <| num F v).toWTZ - (multiplicity p <| den F v).getOrElse 0

but it's being really annoying to work with, so I think I'm doing this wrong

[Daniel Weber]

Yaël Dillies said:

Hot take: multiplicity is broken, which is why nobody uses it

So what should I use instead?

[Andrew Yang]

example  {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] [DecidableRel fun (x x_1 : α) => (multiplicity x x_1).Dom]
    {a : α} {b : α} (h : ¬a ∣ b) : (multiplicity a b).getOrElse 0 = 0 := by
  classical
  have := multiplicity.multiplicity_eq_zero.mpr h
  simp_rw [this]
  sorry

This is because docs#Part.getOrElse has an extra Decidable a.Dom field, and lean cannot figure out Decidable 0.Dom.

[Kyle Miller]

Sometimes when there's "motive is not type correct" it's worth reaching for convert/convert_to to try to change the goal into the intended form. Not saying this is the right way to go here, but it's a tool that's worth knowing.

example {α : Type u_1} [Monoid α] [DecidableRel fun (x x_1 : α) => x ∣ x_1] [DecidableRel fun (x x_1 : α) => (multiplicity x x_1).Dom]
    {a : α} {b : α} (h : ¬a ∣ b) : (multiplicity a b).getOrElse 0 = 0 := by
  have := multiplicity.multiplicity_eq_zero.mpr h
  convert_to Part.getOrElse 0 0 = 0 using 2
  · rw [← this]
    infer_instance
  -- ⊢ Part.getOrElse 0 0 = 0
  sorry