Inconsistent simp lemma loop forever

Stream: mathlib4

[Jz Pan]

Seems that there are some simp lemma in mathlib which will loop forever:

import Mathlib.NumberTheory.Padics.RingHoms

example (p : ℕ) [Fact p.Prime] (x : (ZMod p)ˣ) (h : p ∣ x.1.val * x.2.val) : False := by
  /-
  tactic 'simp' failed, nested error:
  maximum recursion depth has been reached
  use `set_option maxRecDepth <num>` to increase limit
  use `set_option diagnostics true` to get diagnostic information
  -/
  simp at h
  sorry

Any ideas?

[Kenny Lau]

you know, the error tells you exactly how to debug it

[Kenny Lau]

image.png

[Kenny Lau]

and then if you follow it, it tells you that these two lemmas are in conflict, which is weird that the simp linter didn't catch it

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/blob/860d21962a6ace996c34b44e9e9668eee7c61753/Mathlib/Data/ZMod/Basic.lean#L792-L801

[Kenny Lau]

it's also weird that this lemma isn't just proved using the first lemma

[Kenny Lau]

ah i think it's because Inv is always defined for ZMod n, even when n is not prime (so it won't always match the condition of the first lemma which requires a DivisionMonoid)

[Kenny Lau]

now that's a tricky issue

[Jz Pan]

Are there any proposed fix of it?