feat: port NumberTheory.Padics.PadicNumbers !4#3095

Stream: PR reviews

[Jujian Zhang]

I have managed to get padicNumbers.lean compile now. But the linter is complaining on line 840 and 1154. On line 840, the linter timed out with this error message:

simplify fails on left-hand side:

tactic 'simp' failed, nested error:

(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

On 1154, the theorem reads

theorem addValuation.apply {x : ℚ_[p]} (hx : x ≠ 0) :
    Padic.addValuation x = (x.valuation : WithTop ℤ) :=

the linter complains that the left hand side is not in simp normal form while left hand side is exactly what linter thinks should be simplified to.

#check Padic.addValuation.apply /- Left-hand side simplifies from
  ZeroHom.toFun (↑Padic.addValuation.toMonoidWithZeroHom) x
to
  ↑Padic.addValuation x
using
  simp only [@ne_eq, @ZeroHom.toFun_eq_coe, @MonoidWithZeroHom.toZeroHom_coe, @Valuation.toMonoidWithZeroHom_coe_eq_coe]
Try to change the left-hand side to the simplified term!

How do I fix these two linter errors please

[Scott Morrison]

Valuation.toMonoidWithZeroHom_coe_eq_coe sounds suspicious.

[Scott Morrison]

And the discrepancy between the LHS's makes me wonder if you accidentally have two different coercions.

[Jujian Zhang]

I am not sure how to check if I made two coercions, even if I change it to

@[simp]
theorem addValuation.apply {x : ℚ_[p]} (hx : x ≠ 0) :
    (Padic.addValuation : AddValuation ℚ_[p] (WithTop ℤ)) x = (x.valuation : WithTop ℤ) := by

Linter still says the same thing

[Ruben Van de Velde]

Can I start debugging from the current state of the PR?

[Jujian Zhang]

Sure thing, thanks!

[Ruben Van de Velde]

Hrm, maybe the CoeFun on AddValuation isn't set up correctly? The LHS simplifies to FunLike.coe