Problem converting between PartENat and Nat

Stream: new members

[Tony Ma]

The goal I would like to prove is

import Mathlib
open multiplicity Nat
example : (multiplicity 2 (factorial 16)) % 10 = 5 := by sorry

However, it appears to "fail to synthesize HMod PartENat ℕ PartENat".

My first question is, is there a way to create impicit goal, so I could write something like (multiplicity 2 (factorial 16)).get ?_ % 10 = 5?

And the second question is my unsuccessful conversion between PartENat and Nat. I compromised for the moment to change the goal to multiplicity 2 (factorial 16) = 15 and tried to write the proof as follows:

example : multiplicity 2 (factorial 16) = 15 := by
  have h₁ : multiplicity.Finite 2 (Nat.factorial 16) := by
    refine multiplicity.finite_nat_iff.mpr ⟨show 2 ≠ 1 by norm_num, Nat.factorial_pos 16⟩
  have h₂ : (2 - 1) * (multiplicity 2 (factorial 16)).2 h₁ = 16 - (Nat.digits 2 16).sum := by
    apply Prime.sub_one_mul_multiplicity_factorial
    exact Nat.prime_two
  rw [show (Nat.digits 2 16).sum = 1 by native_decide] at h₂
  ring_nf at h₂

What is the way to prove multiplicity 2 16! = 15 (both sides are of type PartENat) from (multiplicity 2 16!).get h₁ = 15? And what is a better practice to write the proof (I found it a bit weird after writing out).

[Daniel Weber]

What Mathlib version are you in? docs#multiplicity was (somewhat recently) changed to be Nat-valued, so PartENat shouldn't appear here

[Daniel Weber]

import Mathlib
open multiplicity Nat
example : (multiplicity 2 (factorial 16)) % 10 = 5 := by
  rw [← padicValNat_def']
  · rw [padicValNat_factorial (b := 5)]
    · decide
    · apply Nat.log_lt_of_lt_pow <;> decide
  · decide
  · apply factorial_pos

works on the current version

[Tony Ma]

I see. I think I am using a version of Nov, 2024, but I ain't quite sure how to get it. So does Lean supports something like implicit goal (as described in my previous comment)?

[Matt Diamond]

@Tony Ma What would an implicit goal of (multiplicity 2 (factorial 16)).get ?_ % 10 = 5 actually mean as a proposition?

[Daniel Weber]

I strongly recommend upgrading Mathlib, PartENat is a pain to work with

[Tony Ma]

Matt Diamond 发言道：

Tony Ma What would an implicit goal of (multiplicity 2 (factorial 16)).get ?_ % 10 = 5 actually mean as a proposition?

I am considering to do this stuff by

import Mathlib
open multiplicity Nat
lemma lm : multiplicity.Finite 2 (Nat.factorial 16) := by sorry
example : (multiplicity 2 (factorial 16)).get lm % 10 = 5 := by sorry

So I wonder if I could directly have (multiplicity 2 (factorial 16)).get ?_ % 10 = 5 and LEAN help me to figure out this implicit goal.

[Tony Ma]

Daniel Weber 发言道：

I strongly recommend upgrading Mathlib, PartENat is a pain to work with

I see. I have to use this version for this moment for some particular reason. But thanks for your comment! That's also how I think of it.

[Daniel Weber]

You can try using padicValNat_def to get out of PartENat, but I don't recall its old definition