calculating multiplicities

Stream: mathlib4

[Julian Berman]

Is there a faster path to:

import Mathlib.RingTheory.Multiplicity

example : emultiplicity 3 18 = 2 := by
  dsimp [emultiplicity]
  simp only [show multiplicity.Finite 3 18 by decide, ↓reduceDIte]
  norm_cast
  simp only [Nat.find_eq_iff, Nat.reduceAdd, Nat.reducePow, Decidable.not_not]
  decide

Probably it's Nat.find's API I need to learn more about?

[Julian Berman]

Ah, or the _mul theorems...

[Jireh Loreaux]

yeah, this works:

import Mathlib.RingTheory.Multiplicity
import Mathlib.Data.Nat.Prime.Defs

example : emultiplicity 3 18 = 2 := by
  rw [show 18 = 2 * 3 ^ 2 from rfl]
  have : Prime 3 := Nat.prime_iff.mp Nat.prime_three
  rw [emultiplicity_mul this, emultiplicity_pow_self_of_prime this, emultiplicity_eq_zero.mpr (by norm_num),
    zero_add, Nat.cast_ofNat]

I'm not sure it qualifies as faster though.

[Daniel Weber]

Can you rewrite with docs#padicValNat_def' and then use rfl/decide?

[Julian Berman]

I can do:

example : emultiplicity 3 18 = 2 := by
  rw [← padicValNat_eq_emultiplicity (by positivity)]

to get ↑(padicValNat 3 18) = 2 but should I consider that progress? Neither rfl nor decide (nor anything else obvious that I tried) make progress from there without doing similar things to Jireh's or my original attempt.

[Julian Berman]

I think Jireh's proof is probably good enough for me if there's nothing else obvious that I should know about.

[Matthew Ballard]

There should be a norm_num extension.

[Julian Berman]

Should be meaning "is" or should be? I tried norm_num initially with import Mathlib and didn't see any progress. I'll try again with this new state.

[Matthew Ballard]

Very much "should be" :rainbow:

[Daniel Weber]

You can do

import Mathlib.RingTheory.Multiplicity

example : emultiplicity 3 18 = 2 := by
  erw [emultiplicity_eq_coe]
  decide

(there's erw due to a missing emultiplicity_eq_ofNat)

[Julian Berman]

Daniel Weber said:

(there's erw due to a missing emultiplicity_eq_ofNat)

#19753, hopefully I've done that right, thanks Daniel. Seems quite easy to forget to add that, I usually lose all understanding when instOfAtLeastTwo shows up.